Skip to Content

TU Wien Fakultät für Informatik DBAI Database and Artificial Intelligence Group
Top-level Navigation: Current-level Navigation:

Path: DBAI > Research > Projects > Decodyn > dynQBF

Tools: Print

A dynamic programming-based QBF solver


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.



The latest releases (including source code) are available at: Github .

Old releases:

Current evaulation instances:

Old evaluation instances:



  1. Günther Charwat and Stefan Woltran 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  ]
  2. Günther Charwat and Stefan Woltran 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,, 2016.
    [ Abstract | BibTeX | pdf  ]
Last updated: 2017-07-03 16:06

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. / Disclaimer.