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
Last updated: 2017-07-03 16:06