{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiazwnqzxen6ixxpq3fjo3giv23uclwaz64pcpqakvacipn2nsip5u",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mlqndww6cdl2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2605.12073v1",
  "publishedAt": "2026-05-13T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Leif Eriksson",
    "Victor Lagerkvist",
    "Sebastian Ordyniak",
    "George Osipov",
    "Fahad Panolan",
    "Mateusz Rychlicki"
  ],
  "textContent": "**Authors:** Leif Eriksson, Victor Lagerkvist, Sebastian Ordyniak, George Osipov, Fahad Panolan, Mateusz Rychlicki\n\nDetermining 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"
}