Article ID Journal Published Year Pages File Type
430227 Journal of Computer and System Sciences 2014 15 Pages PDF
Abstract

•We solve an open problem on the complexity of bounded tree-width QBF.•We show that the bounded tree-width QBF problem is PSPACE-complete.•We present a family of formulas with bounded tree-width with short refutations.

Tree-width and path-width are two well-studied parameters of structures that measure their similarity to a tree and a path, respectively. We show that QBF on instances with constant path-width, and hence constant tree-width, remains PSPACE-complete. This answers a question by Vardi. We also show that on instances with constant path-width and a very slow-growing number of quantifier alternations (roughly inverse-Ackermann many in the number of variables), the problem remains NP-hard. Additionally, we introduce a family of formulas with bounded tree-width that do have short refutations in Q-resolution, the natural generalization of resolution for quantified Boolean formulas.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, ,