2026/01/01 by Andreas Grigorjew, Michael Lampis · 1 voice
Computer Science · #Advanced Graph Theory Research #Complexity and Algorithms in Graphs #Formal Methods in Verification
paper · pdf · doi:10.4230/lipics.sat.2026.18
openalex publication_date 2026/01/01 · openalex created_date 2026/07/17 · openalex updated_date 2026/07/28
Quantified Boolean Formula (QBF) is a notoriously hard generalization of SAT, especially from the point of view of parameterized complexity, where the problem remains intractable for most standard parameters. A recent work by Eriksson et al. [IJCAI 24] addressed this by considering the case where the propositional part of the formula is in CNF and we parameterize by the number k of existentially quantified variables. One of their main results was that this natural (but so far overlooked) parameter does lead to fixed-parameter tractability, if we also bound the maximum arity d of the clauses of the given CNF. Unfortunately, their algorithm has a double-exponential dependence on k (22k), even when d is an absolute constant. Since the work of Eriksson et al. only complemented this with a SETH-based lower bound implying that a 2O(k) dependence is impossible, this left a large gap as an open question. Our main result in this paper is to close this gap by showing that the double-exponential dependence is optimal, assuming the ETH: even for CNFs of arity 4, QBF with k existential variables cannot be solved in time 22o(k) |φ|O(1). Complementing this, we also consider the further restricted case of QBF with only two quantifier blocks (∀∃-QBF). We show that in this case the situation improves dramatically: for each d ≥ 3 we show an algorithm with running time kOd(kd-1) |φ|O(1) (where the notation Od hides factors depending on d) and a lower bound under the ETH showing our algorithm is almost optimal.