Bounded-width QBF is PSPACE-complete

被引:19
作者
Atserias, Albert [1 ]
Oliva, Sergi [1 ]
机构
[1] Univ Politecn Cataluna, Barcelona 08034, Spain
关键词
Tree-width; Path-width; Quantified Boolean formulas; PSPACE-complete; CONSTRAINT-SATISFACTION; ALGORITHM;
D O I
10.1016/j.jcss.2014.04.014
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
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. (C) 2014 Elsevier Inc. All rights reserved.
引用
收藏
页码:1415 / 1429
页数:15
相关论文
共 20 条
[1]  
Alekhnovich M, 2002, ANN IEEE SYMP FOUND, P593, DOI 10.1109/SFCS.2002.1181983
[2]   COMPLEXITY OF FINDING EMBEDDINGS IN A K-TREE [J].
ARNBORG, S ;
CORNEIL, DG ;
PROSKUROWSKI, A .
SIAM JOURNAL ON ALGEBRAIC AND DISCRETE METHODS, 1987, 8 (02) :277-284
[3]   LINEAR-TIME ALGORITHM FOR TESTING THE TRUTH OF CERTAIN QUANTIFIED BOOLEAN FORMULAS [J].
ASPVALL, B ;
PLASS, MF ;
TARJAN, RE .
INFORMATION PROCESSING LETTERS, 1979, 8 (03) :121-123
[4]   RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS [J].
BUNING, HK ;
KARPINSKI, M ;
FLOGEL, A .
INFORMATION AND COMPUTATION, 1995, 117 (01) :12-18
[5]   Multi-resolution on compressed sets of clauses [J].
Chatalic, P ;
Simon, L .
12TH IEEE INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2000, :2-10
[6]  
Chen H, 2004, FRONT ARTIF INTEL AP, V110, P161
[7]  
Chen HB, 2005, LECT NOTES COMPUT SC, V3634, P232, DOI 10.1007/11538363_17
[8]   Decomposing Quantified Conjunctive (or Disjunctive) Formulas [J].
Chen, Hubie ;
Dalmau, Victor .
2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, :205-214
[9]  
Clarke EM, 1999, MODEL CHECKING, P1
[10]  
Dalmau V., 2006, LNCS, P223