Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach

TL;DR

This paper introduces a new parameter called clause covering backdoor for QBF, analyzing its fixed-parameter tractability across different base classes and establishing complexity results.

Contribution

It defines clause covering backdoors for QBF and provides complexity classifications, including FPT algorithms for some classes and hardness results for others.

Findings

FPT algorithms for 2-CNF and linear equations QBF cases

W[1]-hardness for Horn QBF case

Partial dichotomy in the complexity landscape of QBF backdoors

Abstract

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.