Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Eiben, Eduard; Ganian, Robert; Ordyniak, Sebastian http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-85135
URL:

; ;

Small Resolution Proofs for QBF using Dependency Treewidth

pdf-format:


Abstract

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.

BibTeX - Entry

@InProceedings{eiben_et_al:LIPIcs:2018:8513,
  author =	{Eduard Eiben and Robert Ganian and Sebastian Ordyniak},
  title =	{{Small Resolution Proofs for QBF using Dependency Treewidth}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Rolf Niedermeier and Brigitte Vall{\'e}e},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8513},
  URN =		{urn:nbn:de:0030-drops-85135},
  doi =		{10.4230/LIPIcs.STACS.2018.28},
  annote =	{Keywords: QBF, treewidth, fixed parameter tractability, dependency schemes}
}

Keywords: QBF, treewidth, fixed parameter tractability, dependency schemes
Seminar: 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)
Issue date: 2018
Date of publication: 2018


DROPS-Home | Fulltext Search | Imprint Published by LZI