License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2019.18
URN: urn:nbn:de:0030-drops-102571
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10257/
Go to the corresponding LIPIcs Volume Portal

Capelli, Florent ; Mengel, Stefan

Tractable QBF by Knowledge Compilation

pdf-format:
LIPIcs-STACS-2019-18.pdf (0.6 MB)

Abstract

We generalize several tractability results concerning the tractability of Quantified Boolean Formulas (QBF) with restricted underlying structure. To this end, we introduce a notion of width for structured DNNF which are a class of Boolean circuits heavily studied in knowledge compilation, a subarea of artificial intelligence. We then show that structured DNNF allow quantifier elimination with a size blow-up depending only on the width of the DNNF and not its size. Using known algorithms transforming restricted CNF-formulas into deterministic DNNF, we apply this result to generalize several results for counting and decision on QBF. We also complement these results with lower bounds that show that our definitions and results are essentially optimal in several senses.

BibTeX - Entry

@InProceedings{capelli_et_al:LIPIcs:2019:10257,
  author =	{Florent Capelli and Stefan Mengel},
  title =	{{Tractable QBF by Knowledge Compilation}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Rolf Niedermeier and Christophe Paul},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10257},
  doi =		{10.4230/LIPIcs.STACS.2019.18},
  annote =	{Keywords: QBF, knowledge compilation, parameterized algorithms}
}

Keywords: QBF, knowledge compilation, parameterized algorithms
Collection: 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)
Issue Date: 2019
Date of publication: 12.03.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI