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)}}|φ|^{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})}|φ|^{O(1)}$ and a lower bound under the ETH showing our algorithm is almost optimal.
翻译:量化布尔公式(QBF)是\textsc{SAT}问题一个著名的困难推广,尤其从参数化复杂度的视角来看,该问题对于大多数标准参数仍然是难解的。Eriksson等人近期的工作[IJCAI 24]通过考虑公式的命题部分为CNF且以存在量化变量的数量$k$作为参数的情形来应对这一挑战。他们的主要结果之一是,如果我们同时限定给定CNF子句的最大元数$d$,那么这个自然(但此前被忽视)的参数确实能导出固定参数可解性。遗憾的是,他们的算法对$k$(即使$d$为绝对常数时)存在\emph{双指数}依赖关系($2^{2^k}$)。由于Eriksson等人的工作仅辅以一个基于SETH的下界,表明$2^{O(k)}$的依赖关系不可能实现,这为开放问题留下了巨大的间隙。本文的主要结果是通过证明在假设ETH成立的情况下,双指数依赖关系是最优的,从而填补这一间隙:即使对于元数为$4$的CNF,具有$k$个存在变量的QBF问题也无法在时间$2^{2^{o(k)}}|φ|^{O(1)}$内求解。作为补充,我们还考虑了仅有两个量词块的QBF进一步受限情况($\forall\exists$-QBF)。我们证明在此情形下情况显著改善:对于每个$d\ge 3$,我们给出了一个运行时间为$k^{O_d(k ^{d-1})}|φ|^{O(1)}$的算法,并基于ETH给出了下界,表明我们的算法几乎是最优的。