D-QBF with Few Existential Variables Revisited

Abstract

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 (2^{2^k}), 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 2^{O(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^{2^o(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^O_d(k^{d-1}) |φ|^O(1) (where the notation O_d hides factors depending on d) and a lower bound under the ETH showing our algorithm is almost optimal.