Expansion-based QBF Solving on Tree Decompositions

Abstract

In recent years various approaches for quantified Boolean formula (QBF) solving have been developed, including methods based on expansion, skolemization and search. Here, we present a novel expansion-based solving technique that is motivated by concepts from the area of parameterized complexity. Our approach relies on dynamic programming over the tree decomposition of QBFs in prenex conjunctive normal form (PCNF). Hereby, binary decision diagrams (BDDs) are used for compactly storing partial solutions. Towards efficiency in practice, we integrate dependency schemes and develop dedicated heuristic strategies. Our experimental evaluation reveals that our implementation is competitive to state-of-the-art solvers on instances with one quantifier alternation. Furthermore, it performs particularly well on instances up to a treewidth of approximately 80, even for more quantifier alternations. Results indicate that our approach is orthogonal to existing techniques, with a large number of uniquely solved instances.