d-QBF with Few Existential Variables Revisited

TL;DR

This paper establishes tight bounds on the complexity of solving QBF with few existential variables, showing the double-exponential dependence is optimal under ETH and providing efficient algorithms for special cases.

Contribution

It proves the optimality of the double-exponential dependence on existential variables in QBF solving under ETH and offers improved algorithms for the orallxist case with bounded clause arity.

Findings

Double-exponential dependence on k is optimal under ETH.

New algorithms for orallxist QBF with bounded clause arity.

Lower bounds matching the algorithms' complexity.

Abstract

Quantified Boolean Formula (QBF) is a notoriously hard generalization of \textsc{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 \emph{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)}}|\phi|^{O(1)}$. Complementing this, we also consider the further restricted case of QBF with only two quantifier blocks ($\forall\exists$-QBF). We show that in this case the situation improves dramatically: for each $d\ge 3$ we show an algorithm with running time $k^{O_d(k ^{d-1})}|\phi|^{O(1)}$ and a lower bound under the ETH showing our algorithm is almost optimal.