Solving Quantified Boolean Formulas with Few Existential Variables

TL;DR

This work identifies a natural, previously overlooked parameter for QBFSAT: the number $k$ of existential variables. It develops an unconditionally FPT algorithm for $d$-CNF QBFs with bounded clause size by combining quantifier-elimination to Or-CNF Tautology with a sunflower-based kernel that reduces to Clause-Graph Independent Set, achieving running time $2^{\mathcal{O}(k 2^k)} \cdot |\phi|$. The results extend to the finite-domain QCSP, via a Boolean-domain encoding that preserves parameterized tractability under the joint parameter $k+d$ (existential variables plus domain/arity). Complementary lower bounds show W[1]-hardness for unbounded clause size and ETH/SETH-based limits, clarifying the boundary between tractable and intractable regimes and guiding future solver design for PSPACE-complete problems.

Abstract

The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters} guaranteeing fixed-parameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.

Figures (1)

• Figure 1: Let $X=\{x_1,x_2,\ldots,x_6\}$ be a set of variables. Let $\phi_1=(x_1\vee x_2 \vee x_3)\wedge (\overline{x}_1\vee x_2 \vee x_4)\wedge (\overline{x}_1\vee x_5 \vee \overline{x}_6) \wedge (\overline{x}_3\vee x_2 \vee x_5)$, $\phi_2=(x_2 \vee \overline{x}_3 \vee \overline{x}_6)\wedge (\overline{x}_4\vee \overline{x}_5 \vee x_6)\wedge (\overline{x}_2\vee x_3 \vee \overline{x}_6)$, $\phi_3=(\overline{x}_2 \vee {x}_3 \vee {x}_4)\wedge (\overline{x}_2\vee \overline{x}_4 \vee x_5)\wedge ({x}_3\vee x_4 \vee \overline{x}_5)$, and $\phi_4=(x_1\vee \overline{x}_2 \vee x_5)\wedge (\overline{x}_3\vee x_4 \vee x_6)\wedge (x_3\vee x_4 \vee \overline{x}_6) \wedge (\overline{x}_4\vee \overline{x}_5 \vee x_6)$. The vertices $u_1,\ldots,u_4$ corresponds to the first, second, third, and fourth clauses of $\phi_1$, respectively. Similarly, the vertices $v_1,v_2,v_3$ corresponds to the first second, and third clauses of $\phi_2$, respectively. Analogously, we have drawn vertices for clauses in $\phi_3$ and $\phi_4$. All the edges incident on $u_1$ are drawn in the figure. The set $\{u_3,v_3,w_1,z_3\}$ is an independent set the graph and the assignment $\alpha(x_1)=\alpha(x_2)=\alpha(x_6)=1$ and $\alpha(x_3)=\alpha(x_4)=\alpha(x_5)=0$ implies that $\bigvee_{i=1}^4\phi_i$ is not a tautology.

Theorems & Definitions (30)

• Lemma 1
• proof
• Lemma 2
• proof
• Theorem 3
• proof
• Lemma 4: Erdos60
• Lemma 5
• proof
• Theorem 6