pith. sign in

arxiv: 2605.12073 · v1 · submitted 2026-05-12 · 💻 cs.CC · cs.AI

Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach

Leif Eriksson , Victor Lagerkvist , Sebastian Ordyniak , George Osipov , Fahad Panolan , Mateusz Rychlicki This is my paper

Pith reviewed 2026-05-13 04:06 UTC · model grok-4.3

classification 💻 cs.CC cs.AI
keywords QBFparameterized complexitybackdoorsHorn2-CNFlinear equationsW[1]-hardnessFPT
0
0 comments X

The pith

QBF becomes fixed-parameter tractable after deleting clauses that cover a small number of variables to reach 2-CNF or linear equations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies quantified Boolean formula validity using a new parameter: the size of a clausal deletion backdoor that reduces the input to one of three classical tractable classes. It proves that the problem is fixed-parameter tractable for backdoors to 2-CNF and to linear equations, but W[1]-hard for backdoors to Horn. The algorithms rely on propagation in one case and Gaussian elimination in the other. This classification is nearly complete, missing only one algebraic case for a full dichotomy.

Core claim

We establish W[1]-hardness for the Horn base class but prove FPT for 2-CNF and linear equations under the clausal deletion backdoor parameterization, showing that QBF solving is FPT when a backdoor of size k is given and using propagation or Gaussian elimination respectively, while only one further algebraic case remains open for a complete dichotomy.

What carries the argument

The clause covering (CC) backdoor: a set of clauses whose removal leaves a formula in the chosen base class, with the parameter being the number of distinct variables appearing in those clauses.

Load-bearing premise

The backdoor of size k is supplied as input and the base classes remain tractable once the selected clauses are deleted.

What would settle it

A reduction from a W[1]-hard problem to QBF instances that admit a size-k clausal deletion backdoor to 2-CNF would falsify the fixed-parameter tractability claim for that case.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces clausal deletion backdoors (also called clause covering or CC-backdoors) as a new parameter k for QBF: the number of variables whose incident clauses must be deleted to reach a tractable base class. It proves W[1]-hardness when the base class is Horn QBF, FPT algorithms when the base class is 2-CNF or linear equations (via propagation and Gaussian elimination, respectively), and an algebraic near-dichotomy showing that only one further base class remains to be classified for a complete picture.

Significance. If the results hold, the work is significant because it supplies the first non-trivial FPT results for QBF under a backdoor parameter that does not restrict quantifier alternations. The explicit use of propagation and Gaussian elimination for the FPT cases, together with the algebraic characterization of the dichotomy, strengthens the theoretical toolkit for QBF and may guide the design of practical solvers that exploit small backdoors.

minor comments (3)
  1. The abstract and introduction use both 'clausal deletion backdoor' and 'clause covering (CC) backdoor' without an explicit early definition of the precise deletion operation on quantified clauses; a short formal definition with a small example would improve readability.
  2. The claim that the base classes 'remain tractable under the QBF semantics after deletion' is stated but not illustrated; a one-paragraph reminder of why Horn, 2-CNF, and linear-equation QBF stay polynomial-time solvable would help readers unfamiliar with the QBF literature.
  3. The algebraic sense in which 'only one important case' is missing for a full dichotomy is mentioned in the abstract but not previewed; a brief statement of the algebraic criterion used would make the dichotomy result easier to locate.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our paper, the recognition of its significance for QBF parameterized complexity, and the recommendation of minor revision. We are pleased that the contributions on clausal deletion backdoors, the FPT results via propagation and Gaussian elimination, the W[1]-hardness for Horn, and the algebraic near-dichotomy were viewed favorably.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper establishes W[1]-hardness for Horn and FPT for 2-CNF and linear equations under clausal deletion backdoors for QBF, using standard parameterized reductions and algorithms based on propagation and Gaussian elimination. These results rely on the classical tractability of the base classes under QBF semantics, which is external to the paper. No equations, parameters, or claims reduce by construction to fitted inputs or self-referential definitions. No load-bearing self-citations or uniqueness theorems imported from prior author work create circularity. The near-dichotomy claim is algebraic and independent. This is a normal non-finding for a theoretical complexity paper with explicit algorithmic and hardness proofs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The results rest on standard background facts about QBF complexity and the tractability of the three base classes; no free parameters or invented entities are introduced.

axioms (2)
  • standard math Validity of QBF is PSPACE-complete
    Used as the starting point for why parameterization is needed.
  • domain assumption Horn, 2-CNF, and linear-equation QBF are tractable when the quantifier prefix is unrestricted
    The paper treats these as the target tractable classes after deletion.

pith-pipeline@v0.9.0 · 5519 in / 1362 out tokens · 66691 ms · 2026-05-13T04:06:55.615061+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages

  1. [1]

    Abrahamsen, L

    M. Abrahamsen, L. Kleist, and T. Miltzow. Training neural networks is er-complete. In M. Ranzato, A. Beygelzimer, Y. Dauphin, P. Liang, and J. W. Vaughan, editors,Advances in Neural Information Processing Systems, volume 34, pages 18293–18306. Curran Associates, Inc., 2021

    work page 2021

  2. [2]

    Atserias and S

    A. Atserias and S. Oliva. Bounded-width QBF is PSPACE-complete.Journal of Computer and System Sciences, 80(7):1415–1429, 2014

    work page 2014

  3. [3]

    Biere, M

    A. Biere, M. Heule, and H. v. van Maaren.Handbook of Satisfiability: Second Edition. Frontiers in Artificial Intelligence and Applications. IOS Press, 2021

    work page 2021

  4. [4]

    B¨ ohler, N

    E. B¨ ohler, N. Creignou, S. Reith, and H. Vollmer. Playing with Boolean blocks, part I: Post’s lattice with applications to complexity theory.SIGACT News, 34, 01 2003

    work page 2003

  5. [5]

    Calabro, R

    C. Calabro, R. Impagliazzo, and R. Paturi. The complexity of satisfiability of small depth circuits. In J. Chen and F. V. Fomin, editors,Parameterized and Exact Computation, volume 5917 ofLecture Notes in Computer Science, pages 75–85. Springer Berlin Heidelberg, 2009

    work page 2009

  6. [6]

    Calabro, R

    C. Calabro, R. Impagliazzo, and R. Paturi. On the exact complexity of evaluating quantifiedk-CNF.Algorithmica, 65(4):817–827, 2013

    work page 2013

  7. [7]

    H. Chen. Quantified constraint satisfaction and 2-semilattice polymorphisms. In M. Wallace, editor,Principles and Practice of Constraint Programming - CP 2004, 10th International Conference, CP 2004, Toronto, Canada, Septem- ber 27 - October 1, 2004, Proceedings, volume 3258 ofLecture Notes in Computer Science, pages 168–181. Springer, 2004

    work page 2004

  8. [8]

    H. Chen. A rendezvous of logic, complexity, and algebra.ACM SIGACT News, 37(4):85–114, 2006. 22

    work page 2006

  9. [9]

    M. C. Cooper, D. A. Cohen, and P. Jeavons. Characterising tractable constraints.Artificial Intelligence, 65(2):347–361, 1994

    work page 1994

  10. [10]

    Creignou, P

    N. Creignou, P. Kolaitis, and B. Zanuttini. Structure identification of boolean relations and plain bases for co-clones.Journal of Computer and System Sciences, 74(7):1103–1115, 2008

    work page 2008

  11. [11]

    Cygan, F

    M. Cygan, F. V. Fomin, L. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh.Parameterized Algorithms. Springer Publishing Company, Incorporated, 1st edition, 2015

    work page 2015

  12. [12]

    Dell and D

    H. Dell and D. Van Melkebeek. Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses.Journal of the ACM, 61(4), July 2014

    work page 2014

  13. [13]

    R. G. Downey, M. R. Fellows, et al.Fundamentals of parameterized complexity, volume 4. Springer, 2013

    work page 2013

  14. [14]

    Eriksson, V

    L. Eriksson, V. Lagerkvist, S. Ordyniak, G. Osipov, F. Panolan, and M. Rych- licki. Solving quantified Boolean formulas with few existential variables. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-2024), pages 1889–1897. ijcai.org, 2024

    work page 2024

  15. [15]

    J. K. Fichte, R. Ganian, M. Hecher, F. Slivovsky, and S. Ordyniak. Structure- aware lower bounds and broadening the horizon of tractability for QBF. In Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS-2023), pages 1–14, 2023

    work page 2023

  16. [16]

    F. V. Fomin, D. Lokshtanov, S. Saurabh, and M. Zehavi.Kernelization: theory of parameterized preprocessing. Cambridge University Press, 2019

    work page 2019

  17. [17]

    P. Nunn, M. S¨ alzer, F. Schwarzentruber, and N. Troquard. A logic for reasoning about aggregate-combine graph neural networks. InProceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI ’24, 2024

    work page 2024

  18. [18]

    Samer and S

    M. Samer and S. Szeider. Backdoor sets of quantified Boolean formulas. Journal of Automated Reasoning, 42(1):77–97, 2009

    work page 2009

  19. [19]

    Schaefer

    T. Schaefer. The complexity of satisfiability problems. InProceedings of the 10th Annual ACM Symposium on Theory Of Computing (STOC-1978), pages 216–226. ACM Press, 1978

    work page 1978

  20. [20]

    S¨ alzer, F

    M. S¨ alzer, F. Schwarzentruber, and N. Troquard. Verifying quantized graph neural networks is PSPACE-complete. In J. Kwok, editor,Proceedings of 23 the Thirty-Fourth International Joint Conference on Artificial Intelligence (IJCAI-2025), pages 4660–4668. International Joint Conferences on Artificial Intelligence Organization, 8 2025. Main Track

    work page 2025

  21. [21]

    D. Zhuk. Q 2p vs PSpace dichotomy for the quantified constraint satisfaction problem. InProceedings of the 65th IEEE Annual Symposium on Foundations of Computer Science (FOCS-2024), pages 560–572. IEEE, 2024. 24

    work page 2024