Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach
For researchers in parameterized complexity and QBF solving, it provides the first FPT results for QBF with backdoors beyond bounded quantifier alternations.
The paper introduces a new parameter for QBF—the size of a clause covering backdoor—and shows fixed-parameter tractability for 2-CNF and linear equations base classes, while proving W[1]-hardness for Horn, establishing a near-complete dichotomy.
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.