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.

翻译：量化布尔公式（QBF）的可满足性判定是PSPACE完全问题，具有丰富的表达能力。尽管高效求解器备受关注，但与NP中的问题相比，其正面理论结果较为匮乏；在参数化复杂度框架下，通常需要限制量词前缀（如交替次数有界）才能获得固定参数可解性（FPT）。本文提出一个新参数：在达到可处理类之前需从子句中删除的变量数量（即子句覆盖（CC）后门）。我们关注在给定规模为$k$的CC后门时，如何在FPT时间内求解QBF。以QBF的三个经典可处理类为基础类：Horn公式、2-CNF公式和线性方程。我们证明了Horn情况的W[1]-难性，但给出了其他情况的FPT算法，并指出在精确的代数意义下，仅欠缺一种关键情况即可实现完整二分性。我们的算法分别基于传播法和高斯消元法，具有非平凡性，且此类方法在QBF领域尚少有探索。