Expansion-based QBF Solving on Tree Decompositions*
Issue title: Special issue of the 24th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion”
Guest editors: Marco Maratea, Ivan Serina and Paolo Torroni
Affiliations: Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Vienna, Austria. [email protected], [email protected]
Correspondence:
[†]
Address for correspondence: Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Vienna, Austria.
Note: [*] This work was supported by the Austrian Science Fund (FWF): Y698.
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.
