Small Resolution Proofs for QBF using Dependency Treewidth

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

EIBEN Eduard GANIAN Robert ORDYNIAK Sebastian

Year of publication 2018
Type Article in Proceedings
Conference STACS 2018
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.4230/LIPIcs.STACS.2018.28
Keywords QBF; treewidth; fixed parameter tractability; dependency schemes
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.