Talks and Poster Presentations (with Proceedings-Entry):
G. Charwat, S. Woltran:
"Expansion-based (QBF) Solving on Tree Decompositions";
Talk: 24th International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA@AI*IA 2017),
- 2017-11-15; in: "Proceedings of the 24th International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA@AI*IA 2017)",
M. Maratea, I. Serina (ed.);
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 expansionbased 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, BDDs are used for compactly storing partial solutions. Towards efficiency in practice, we integrate dependency schemes and 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. Results indicate that our approach is orthogonal to existing techniques, with a large number of uniquely solved instances.
Electronic version of the publication:
Project Head Stefan Woltran:
Created from the Publication Database of the Vienna University of Technology.