2026/03/09 by Andreas Grigorjew, Michael Lampis · 1 voice
Computer Science · #cs.CC
paper · pdf · doi:10.48550/arxiv.2603.08826
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 2^2o(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 k^Od(k d-1)|φ|O(1) and a lower bound under the ETH showing our algorithm is almost optimal.