[Back]

G. Charwat, S. Woltran:
"Dynamic Programming-based QBF Solving";
Talk: 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France; 2016-07-04; in: "Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016)", F. Lonsing, M. Seidl (ed.); CEUR-WS.org, 1719 (2016), 14 pages.

Solving Quantified Boolean Formulas (QBFs) is a challenging problem due to its high complexity. Many successful methods have been proposed, including extensions of DPLL/CDCL procedures and expansion-based approaches. In this paper, we present a novel method that is inspired by concepts from the field of parameterized complexity. More specifically, we develop a dynamic programming algorithm that traverses a tree decomposition of the QBF instance. We implemented our method using Binary Decision Diagrams as key ingredient to compactly represent the partial solutions computed during dynamic programming. Experiments indicate that our prototype shows promising results for instances with few quantifier alternations and where the treewidth of the propositional formula does not exceed 50. In fact, treewidth can be understood as a measurement of structure within the formula, and to the best of our knowledge has not been used explicitly in QBF solvers yet.

Project Head Stefan Woltran:
Answer-Set Programming Erweiterungen für Problemlösungen auf Zerlegungen

Project Head Stefan Woltran:
START