Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909036131123200 |
|---|---|
| author | Eriksson, Leif Lagerkvist, Victor Ordyniak, Sebastian Osipov, George Panolan, Fahad Rychlicki, Mateusz |
| author_facet | Eriksson, Leif Lagerkvist, Victor Ordyniak, Sebastian Osipov, George Panolan, Fahad Rychlicki, Mateusz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_12073 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach Eriksson, Leif Lagerkvist, Victor Ordyniak, Sebastian Osipov, George Panolan, Fahad Rychlicki, Mateusz Computational Complexity Artificial Intelligence 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. |
| title | Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach |
| topic | Computational Complexity Artificial Intelligence |
| url | https://arxiv.org/abs/2605.12073 |