Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
G. Charwat, S. Woltran:
"Expansion-based (QBF) Solving on Tree Decompositions";
Vortrag: 24th International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA@AI*IA 2017),
Bari, Italien;
14.11.2017
- 15.11.2017; 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 (Hrg.);
CEUR-WS.org,
2011
(2017),
S. 16
- 26.
Kurzfassung englisch:
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.
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_264830.pdf
Zugeordnete Projekte:
Projektleitung Stefan Woltran:
START
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.