Paper: Fixed-Parameter Hierarchies inside PSPACE (at LICS 2006)

Authors: Guoqiang Pan Moshe Y. Vardi

Abstract

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.

BibTeX

  @InProceedings{PanVardi-FixedParameterHiera,
    author = 	 {Guoqiang Pan and Moshe Y. Vardi},
    title = 	 {Fixed-Parameter Hierarchies inside PSPACE},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {27--36},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }