dynQBF
A dynamic programming-based QBF solver
About
dynQBF is an expansion-based QBF solver for instances in prenex CNF form. First, the CNF matix is split into subproblems by constructing a tree decomposition. The QBF is then solved by dynamic programming over the tree decomposition. While the structure of the CNF is reflected by the tree decomposition, structure within the prefix is considered by integrating dependency schemes in the solving process. Furthermore, dynQBF uses nested sets of binary decision diagrams (BDDs) to efficiently store intermediate results.
Downloads
Releases:
The latest releases (including source code) are available at: Github .
Old releases:
- dynQBF 0.2: dynqbf-0.2.zip (GNU/Linux x86-64, statically linked)
- dynQBF 0.1-beta: dynqbf-0.1-beta.zip (GNU/Linux x86-64, statically linked)
Current evaulation instances:
- QBF Evaluation 2016 (QBFEval'16):
Prenex CNF (Dataset 1)
Prenex CNF 2-QBFs (Dataset 3)
Old evaluation instances:
- 2-QBF instances: http://www.qbflib.org/TS2010/2QBF.tar.gz
preprocessed with DepQBF: 2qbf-preprocessed.zip - Eval-2012 instances: http://qbf.satisfiability.org/gallery/eval2012r2.tgz
preprocessed with DepQBF: eval2012r2-preprocessed.zip
References
2019
- Expansion-based QBF Solving on Tree Decompositions In Sumbitted to Fundamenta Informaticae, 2019.
[ Abstract | BibTeX | pdf ]
2017
- Expansion-based QBF Solving on Tree Decompositions In Proc. of the 24th International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA@AI*IA 2017), Volume 2011 of CEUR Workshop Proceedings, pages 16-26, CEUR-WS.org, 2017.
[ BibTeX | pdf ] - BDD-based Dynamic Programming on Tree Decompositions - Towards an Alternative Approach for Efficient QBF Solving Ph.D. Thesis, Fakultät für Informatik an der Technischen Universität Wien, 2017.
Stefan Woltran advisor.
[ Abstract | BibTeX ]
2016
- BDD-based Dynamic Programming on Tree Decompositions Technical Report DBAI-TR-2016-95, DBAI, Fakultät für Informatik an der Technischen Universität Wien, 2016.
[ Abstract | BibTeX | pdf ] - Dynamic Programming-based QBF Solving In Proc. of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Volume 1719 of CEUR Workshop Proceedings, pages 27-40, CEUR-WS.org, 2016.
[ Abstract | BibTeX | pdf ]
Last updated: 2017-07-03 16:06