[Zurück]

E. Eiben, R. Ganian, S. Ordyniak:
"Small Resolution Proofs for QBF using Dependency Treewidth";
in: "Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France", 35th Symposium on Theoretical Aspects of Computer Science, Caen, 2018, ISBN: 978-3-95977-062-0, S. 1 - 14.

In spite of the close connection between the evaluation of quantified Boolean formulas (QBF) and
propositional satisfiability (SAT), tools and techniques which exploit structural properties of SAT
instances are known to fail for QBF. This is especially true for the structural parameter treewidth,
which has allowed the design of successful algorithms for SAT but cannot be straightforwardly
applied to QBF since it does not take into account the interdependencies between quantified
variables.
In this work we introduce and develop dependency treewidth, a new structural parameter
based on treewidth which allows the efficient solution of QBF instances. Dependency treewidth
pushes the frontiers of tractability for QBF by overcoming the limitations of previously introduced
variants of treewidth for QBF. We augment our results by developing algorithms for computing
the decompositions that are required to use the parameter.

https://publik.tuwien.ac.at/files/publik_276179.pdf