提出新参数化方法，高效求解量子布尔公式。
Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach
- 以可删除子句数为参数，构建可处理的回溯门
- 对2-CNF和线性方程类实现固定参数可解
- 算法依赖传播与高斯消元，适合理论研究者
判定量化布尔公式的有效性是PSPACE完全问题，表达能力强但相比NP类问题缺乏积极的理论结果。在参数化复杂度框架下，通常需限制量词前缀（如控制交替次数）才能获得固定参数可解性（FPT）。本文提出新参数：需删除的变量所在子句数量，使其进入可处理类（即子句覆盖回溯门，CC-backdoor）。研究在给定大小为k的CC回溯门时，能否在FPT时间内求解QBF。考虑三种经典可解的QBF基类：Horn、2-CNF和线性方程。证明Horn类为W[1]-hard，而其余两类为FPT；并从代数角度表明，仅缺一个关键情况即可达成完整二分定理。算法非平凡，分别依赖于传播机制和高斯消元，且在QBF中尚未被充分探索。
原文摘要 · Abstract (English)
Determining the validity of a quantified Boolean formula (QBF) is a PSPACE-complete problem with rich expressive power. Despite interest in efficient solvers, there is, compared to problems in NP, a lack of positive theoretical results, and in the parameterized complexity setting one often has to restrict the quantifier prefix (e.g., bounding alternations) to obtain fixed parameter tractability (FPT). We propose a new parameter: the number of variables in clauses that has to be removed before reaching a tractable class (a clause covering (CC) backdoor). We are then interested in solving QBF in FPT time given a CC-backdoor of size $k$. We consider the three classical, tractable cases of QBF as base classes: Horn, 2-CNF, and linear equations. We establish W[1]-hardness for Horn but prove FPT for the others, and prove that in a precise, algebraic sense, we are only missing one important case for a full dichotomy. Our algorithms are non-trivial and depend on propagation, and Gaussian elimination, respectively, and are comparably unexplored for QBF.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。