Fixed-Parameter Hierarchies inside PSPACE

Treewidth measures the ”tree-likeness” of structures. Many NP-complete problems, e.g., propositional satisfiability, are tractable on bounded-treewidth structures. In this work, we study the impact of treewidth bounds on QBF, a canonical PSPACE-complete problem. This problem is known to be fixed-parameter tractable if both the treewidth and alternation depth are taken as parameters. We show here that the function bounding the complexity in the parameters is provably nonelementary (assuming P is different than NP). This yields a strict hierarchy of fixed-parameter tractability inside PSPACE. As a tool for proving this result, we first prove a similar hierarchy for model checking QPTL, quantified propositional temporal logic. Finally, we show that QBF, restricted to instances with a slowly increasing (log∗ ) treewidth, is still PSPACE-complete.

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: Guoqiang Pan, Moshe Y. Vardi
• Keywords: Canonical Pspace-complete Problem, Computer Science, LICS 2006, Many NP-complete Problems, Propositional Temporal Logic