Tree-width is a well-studied parameter of structures that measures their similarity to a tree. Many important NP-complete problems, such as Boolean satisfiability (SAT), are tractable on bounded tree-width instances. In this paper we focus on the canonical PSPACE-complete problem QBF, the fully-quantified version of SAT. It was shown by Pan and Vardi [LICS 2006] that this problem is PSPACE-complete even for formulas whose tree-width grows extremely slowly. Vardi also posed the question of whether the problem is tractable when restricted to instances of bounded tree-width. We answer this question by showing that QBF on instances with constant tree-width is PSPACE-complete.
@InProceedings{atserias_et_al:LIPIcs.STACS.2013.44, author = {Atserias, Albert and Oliva, Sergi}, title = {{Bounded-width QBF is PSPACE-complete}}, booktitle = {30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)}, pages = {44--54}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-50-7}, ISSN = {1868-8969}, year = {2013}, volume = {20}, editor = {Portier, Natacha and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.44}, URN = {urn:nbn:de:0030-drops-39217}, doi = {10.4230/LIPIcs.STACS.2013.44}, annote = {Keywords: Tree-width, QBF, PSPACE-complete} }
Feedback for Dagstuhl Publishing