The QSAT problem, which asks to evaluate a quantified Boolean formula (QBF), is of fundamental interest in approximation, counting, decision, and probabilistic complexity and is also considered the prototypical PSPACEcomplete problem. As such, it has previously been studied under various structural restrictions (parameters), most notably parameterizations of the primal graph representation of instances. Indeed, it is known that QSAT remains PSPACE-complete even when restricted to instances with constant treewidth of the primal graph, but the problem admits a double-exponential fixed-parameter algorithm parameterized by the vertex cover number (primal graph). However, prior works have left a gap in our understanding of the complexity of QSAT when viewed from the perspective of other natural representations of instances, most notably via incidence graphs. In this paper, we develop structure-aware reductions which allow us to obtain essentially tight lower bounds for highly restricted instances of QSAT, including instances whose incidence graphs have bounded treedepth or feedback vertex number. We complement these lower bounds with novel algorithms for QSAT which establish a nearly-complete picture of the problem's complexity under standard graph-theoretic parameterizations. We also show implications for other natural graph representations, and obtain novel upper as well as lower bounds for QSAT under more fine-grained parameterizations of the primal graph.
翻译:QSAT问题(即评估量化布尔公式(QBF)的真值)在近似、计数、决策与概率复杂度等领域具有基础性意义,并被视作典型的PSPACE完全问题。因此,先前研究已从多种结构约束(参数)角度对其展开探索,尤其关注实例主图表示的参数化。事实上,已知即使将实例限制为主图树宽为常数的情况,QSAT仍保持PSPACE完全性,但该问题存在一个以顶点覆盖数(主图)为参数的双指数固定参数算法。然而,先前工作在研究当以其他自然表示(尤其通过关联图)观察QSAT复杂度时留下了认知空白。本文开发了结构感知的归约方法,使我们能够对高度受限的QSAT实例(包括关联图具有有界树深度或反馈顶点数的实例)获得本质紧的下界。我们通过QSAT的新型算法对这些下界进行补充,从而构建了该问题在标准图论参数化下近乎完整的复杂度图景。我们还展示了该结果对其他自然图表示的含义,并针对主图更细粒度的参数化获得了QSAT的上界与下界。