paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF

QBF 的结构感知下界与可处理性视野的拓宽
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 该论文研究 QBF/QSAT 在关联图等结构参数下的参数化复杂性与 FPT 算法,属于纯理论计算复杂性方向,与用户关注的静态分析、LLM/Agent 程序分析、浮点程序分析、贝叶斯程序分析等核心方向几乎没有直接交集。虽然 QBF 与形式化验证有间接关联,但论文本身不涉及程序分析工具、工业落地、LLM 或 benchmark。引用 11 inbox
Johannes K. Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:为 QSAT 在关联图等结构参数下建立紧下界并给出新 FPT 算法,基本补齐其参数化复杂度图景。

本文研究量化布尔公式求值问题 QSAT 的结构参数化复杂度。已有工作表明,即使原图树宽为常数,QSAT 仍是 PSPACE 完全问题,但以顶点覆盖数为参数存在双指数 FPT 算法;然而关联图等其他自然表示下的复杂度尚不清楚。作者提出结构感知归约,对关联图有界 treedepth 或 feedback vertex number 等高度受限实例给出本质紧的下界,并设计新的 QSAT 算法作为补充。这些结果在标准图论参数化下勾画出近乎完整的复杂度图景,还给出其他图表示的推论,并获得原图更细粒度参数化下的新上界与下界。

问题
QSAT 是典型 PSPACE 完全问题,但其在不同结构表示(尤其是关联图)和标准图参数下的参数化复杂度仍存在空白:常数原图树宽仍不可处理,而顶点覆盖数等参数上的上界已知,其他表示的下界与上界不明。
方法
作者发展结构感知归约来构造高度受限实例的紧下界,并针对相关图参数设计新的 QSAT 参数化算法,结合上界与下界分析。
评估
通过理论证明给出关联图有界 treedepth、feedback vertex number 等参数下的本质紧下界与新算法,并推导其他图表示及原图细粒度参数化下的复杂度结论,形成近乎完整的参数化复杂度刻画。
原文摘要(Abstract)

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 PSPACE-complete 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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{abs-2304-13896,
  title = {Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF},
  author = {Johannes K. Fichte and Robert Ganian and Markus Hecher and Friedrich Slivovsky and Sebastian Ordyniak},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175675}
}