# Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach

arXiv: https://arxiv.org/abs/2605.12073 · HTML: https://mlsanity.com/paper/2605.12073/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 28 references that are in the map.
- First posted on arXiv 12 May 2026.

## Builds on (most cited first, 4 of 4)

- [A Logic for Reasoning About Aggregate-Combine Graph Neural Networks](https://mlsanity.com/paper/2405.00205/) (2024)
- [Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF](https://mlsanity.com/paper/2304.13896/) (2023)
- [Solving Quantified Boolean Formulas with Few Existential Variables](https://mlsanity.com/paper/2405.06485/) (2024)
- [Verifying Quantized Graph Neural Networks is PSPACE-complete](https://mlsanity.com/paper/2502.16244/) (2025)

## Abstract (arXiv)

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.