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


The software tool dynQBF is a structure-aware QBF solver. It handles QBF instances in prenex CNF format, and supports QSAT (deciding satisfiability of QBFs) as well as enumerating solutions (partial certificates for the outermost quantifier block). In a nutshell, dynQBF splits the QBF instance into subproblems by constructing a so-called tree decomposition. The QBF is then solved by dynamic programming over the tree decomposition. As key ingredient, dynQBF uses Binary Decision Diagrams 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-01-09 16:57

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist das Institut für Informationssysteme 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.