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/
Capelli, Florent ;
Mengel, Stefan
Tractable QBF by Knowledge Compilation
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 |