Solving Quantified Boolean Formulas with Few Existential Variables

1 Introduction

The quantified Boolean formula (QBF) problem is the decision problem of verifying a formula Q1x1 . . .Qnxn.φ(x1, . . . , xn), where φ(x1, . . . , xn) is a propositional formula and Qi ∈ {∀, ∃} for each i. Throughout, we write QBFSAT (respectively QBF-DNF) for the subproblem restricted to formulas in conjunctive normal form (respectively disjunctive normal form), and d-QBFSAT for the problem where clauses have maximum size d ≥ 1. From a theoretical angle, the QBF problem serves as a foundational example of PSPACE-completeness, and by restricting the quantifier alternations, we get examples of complete problems for any class in the polynomial hierarchy. From a more practical point of view, the field of applied QBF solving has developed on the shoulders of SAT solving, which has seen tremendous advances in the last decade [Fichte et al., 2023a]. Arguably, the raison d'etre behind SAT solving is not only to solve a specific NP-complete problem faster than exhaustive search, but to provide a combinatorial framework applicable to any problem which can be reduced to SAT. This naturally includes any problem in NP but if one considers stronger reductions than Karp reductions (e.g., by allowing a superpolynomial running time or by viewing the SAT solver as an oracle) more problems fall under the umbrella of SAT. However, this approach is not always optimal, and for many problems of importance in artificial intelligence, e.g., planning, model checking, and non-monotonic reasoning [Shukla et al., 2019], this approach is not ideal since the best reductions in the literature incur an exponential overhead. These problems are instead more naturally formulated via QBF. However, this comes with the downside that QBF solvers, despite steady advances, are not nearly as advanced as their SAT brethren. For more information about applied QBF solving we refer the reader to the handbook by Biere et al. [2021].

To bridge the gap between SAT and QBF solving we need algorithmic breakthroughs for the latter. In this paper we analyze QBF from a theoretical perspective and are therefore interested in obtaining unconditionally improved algorithms. To analyze the complexity of QBF we use the influential paradigm of parameterized complexity where the goal is to identify structural properties of instances, represented by natural numbers called parameters, such that one can effectively solve instances with bounded parameter size. More formally, for every instance I of a computational problem we associate a parameter k ∈ N with it and then we are primarily interested in algorithms with a running time bounded by f(k) · poly(|I|) for a computable function f : N → N depends on k and a polynomial function poly depends on the length |I| of the input I. Such algorithms are said to be fixedparameter tractable (FPT). Thus, while f is generally going to be superpolynomial, an FPT algorithm may still be very competitive in practice if the parameter is sufficiently small. For problems in NP there exists a wealth of results [Cygan et al., 2015], but for PSPACE-complete problems the landscape is rather scarce in comparison since there are fewer natural parameters to choose from. For example, the go-to parameter for NP problems is tree-width, which measures how close a graph is to being a tree, and which is typically sufficient to produce an FPT algorithm. But this fails for QBF where it is even known that QBF is PSPACE-complete for constant primal tree-width [Atserias and Oliva, 2014]. Here, the situation becomes more manageable if one simultaneously bounds e.g. the number of quantifier alternations [Chen, 2004] but for the general QBF problem the few FPT results that exists are primarily with respect to more exotic parameters such as prefix pathwidth [Eiben et al., 2020] and respectful treewidth [Atserias and Oliva, 2014] which takes the ordering of the quantifiers into account. Two interesting counter examples are (1) the FPT algorithm parameterized by primal vertex cover number by [Eiben et al., 2020], further optimized and simplified by [Lampis and Mitsou, 2018], and (2) the backdoor approach in [Samer and Szeider, 2009] which generalizes the classical tractable fragments of QBF in an FPT setting. Moreover, very recently, tractability has been shown for two parameters that fall between vertex cover number and treewidth [Fichte et al., 2023b]. Thus, while FPT results for QBF and related problems exist, they are comparably few in number and generally defined with respect to more complicated structural properties. Do simple parameters not exist, or have we been investigating the wrong ones?

In this paper we demonstrate that a natural (and previously overlooked) parameter does exist: the number of existentially quantified variables. Thus, we bound the number of existentially quantified variables but otherwise make no restrictions on the prefix. While quantifier elimination techniques have been an important tool ever since the early days of QBF solving [Ayari and Basin, 2002; Biere, 2004] (see also Janota & Marques-Silva [2015] for a more recent discussion and a comparison to Q-resolution) the predominant focus has been to expand universal quantifiers since the removal of universal quantifiers produces instances that can be solved with classical SAT techniques (however, methods for expanding existential quantifiers have also been tried in practice [Bloem et al., 2021]). This is, for example, made explicit by Szeider & de Haan [2014] who prove that QBF-DNF parameterized by the number of universally quantified variables is FPT-reducible to SAT (parameterized by the number of all variables). However, they only prove para-NP-completeness of the problem which in the world of parameterized complexity is a far cry away from FPT. Conversely, we show that concentrating on existential variable elimination is much more lucrative since in this case one can construct an FPT algorithm once all existential variables have been removed. Let us also remark that if a QBFSAT instance contains k existential variables and n-k universal variables, then the combination n is not a relevant parameter: it makes the problem technically FPT but there are very few applications where one would expect the total number of variables to be bounded. Moreover, while QBFSAT for arbitrary but constant quantifier depth admits a moderately improved algorithm with a running time of the form 2n-nΩ(1) [Santhanam and Williams, 2013], not even 3QBFSAT restricted to universal followed by existential quantifiers admits an exponentially improved 2εn · poly(|ϕ|) algorithm for ε < 1 under the so-called strong exponential-time hypothesis [Calabro et al., 2013].

After having defined the basic notions (Section 2), we obtain our major results in Section 3 as follows. First, given an instance Q1x1 . . . ∃xi . . .Qnxnϕ(x1, . . . , xn) we can remove the existential quantifier for xi by creating a disjunction of the two subinstances (with fresh variables) obtained by fixing xi to 0 or 1. This extends to a quantifier elimination preprocessing scheme which reduces to the problem of checking whether a disjunction of k formulas in d-CNF is a tautology or not. We call this problem OR-CNF TAUTOLOGY and then construct an FPT algorithm by converting it to the problem of finding an independent set in a certain well-structured graph (CLAUSE-GRAPH INDEPENDENT SET). The latter problem has a strong combinatorial flair and we manage to construct a kernel with at most kd!((k - 1)d + 1)d vertices via the sunflower lemma of Erd¨os & Rado [1960]. Put together, this results in an FPT algorithm with a running time of 2O(k2k ) · |ϕ| for QBFSAT with constant clause size when parameterized by the number of existentially quantified variables. At a first glance, this might not look terribly impressive compared to the naive 2n · |ϕ| algorithm obtained by branching on n - k universal and k existential quantifiers, but we stress that the FPT algorithm is suitable for applications where the total number of existentially quantified variables is kept relatively small. Under this constraint our algorithm shows that one can effectively ignore the cost of universally quantified variables and solve the instance in polynomial time. Via an FPT reduction we also demonstrate (in Section 4) that our FPT result straightforwardly can be extended to the more general problem quantified constraint satisfaction where variables take values in arbitrary finite domains.

In Section 5 we show that the clause size dependency in our FPT algorithm is necessary under the conjecture that FPT ̸= W[1], which is widely believed conjecture in parameterized complexity. Specifically we show that QBFSAT, when parameterized by the number of existentially quantified variables (but not the arity), is W[1]-hard by reducing from the MULTIPARTITE INDEPENDENT SET problem. Moreover, under the Exponential Time Hypothesis (ETH), the same reduction rules out algorithms with running time f(k) · 2o(2k ) for every computable function f : N → N. We then proceed to establish a sharper lower bound under the (Strong) ETH for the specific case of clause size 3. First, we have an easy 2o(k) lower bound for 3-QBFSAT (under the exponential-time hypothesis) since 3-SAT can be viewed as a special case of 3-QBFSAT. However, under the strong exponential-time hypothesis we prove a markedly stronger bound: there is no constant c such that 3-QBFSAT (even for only two quantifier blocks) is solvable in ck time, i.e. the problem is not solvable in 2O(k) time. Thus, while our 2O(k2k ) algorithm likely can be improved to some extent, we should not hope to obtain a 2O(k) algorithm. This proof is based on an interesting observation: any instance with comparably few number of universally quantified variables can be solved by enumerating all possible assignments to the universal variables and then solving the remaining part with a 3-SAT algorithm. Thus, as also remarked by Calabro et al. [2013], instances with few existential variables are in a certain sense harder, which makes our FPT algorithm in Section 3 all the more surprising.

We close the paper with a discussion in Section 6. Most importantly, our FPT algorithm shows tractability of new classes of previously hard QBFs, and it would be interesting to investigate whether similar parameters could be used to study other hard problems outside NP. A promising candidate is the NEXPTIME-complete problem obtained by extending Boolean formulas with Henkin quantifiers, resulting in the depedency QBF (DQBF) formalism.

Statements whose full proofs are omitted due to space constraints are marked with ⋆.

2 Preliminaries

In this section we briefly cover the necessary background on parameterized complexity and quantified Boolean formulas. We assume familiarity with the basics of graph theory, cf. [Diestel, 2016]. We use the notation [n] for the set {1, . . . , n} for every n ∈ N.

Computational Complexity. We follow [Downey et al., 2013] and [Fomin et al., 2019] in our presentation. Let Σ be a finite alphabet. A parameterized problem L is a subset of Σ∗ ×N. The problem L is fixed-parameter tractable (or, in FPT) if there is an algorithm deciding whether an instance (I, k) ∈ Σ∗ ×N is in L in time f(k) · |I|c , where f is some computable function and c is a constant independent of (I, k).

Let L,L′ ⊆ Σ∗ × N be two parameterized problems. A mapping P : Σ∗ × N → Σ∗ × N is a fixed-parameter (FPT) reduction from L to L′ if there exist computable functions f, p : N → N and a constant c such that the following conditions hold:

• (I, k) ∈ L if and only if P(I, k) = (I ′ , k′ ) ∈ L′ ,
• k′ ≤ p(k), and
• P(I, k) can be computed in f(k) · |I|c time.

Let L ⊆ Σ∗ ×N be a parameterized problem. A kernelization (algorithm) for L is an algorithm that takes (I, k) ∈ Σ∗ × N as input and in time polynomial in |(I, k)|, outputs (I ′ , k′ ) ∈ Σ∗ ×N such that: (I, k) ∈ L if and only if (I ′ , k′ ) ∈ L, and |I ′ |, k′ ≤ h(k) for some computable function h. The output (I ′ , k′ ) of the kernelization algorithm is called a kernel. Clearly, if L is decidable and admits a kernel, L is in FPT, and the converse also holds (see e.g. [Fomin et al., 2019, Theorem 4]).

The class W[1] contains all problems that admit FPT reductions from INDEPENDENT SET parameterized by the solution size, i.e. the number of vertices in the independent set. Under the standard assumption that FPT ̸= W[1], we can show that a problem is not fixed-parameter tractable by proving its W[1]-hardness, i.e. by providing an FPT reduction from INDEPENDENT SET to the problem. The class XP contains all parameterized problems that can be solved in time nf(k) for instances with input size n, parameter k and some computable function f.

For sharper lower bounds, stronger assumptions are sometimes necessary. Here, we will primarily consider the exponential-time hypothesis which states that the 3-SAT problem is not solvable in subexponential time when parameterized by the number of variables n or the number of clauses m. To make this more precise, for d ≥ 3 let cd denote the infimum of all constants c such that d-SAT is solvable in 2cn time by a deterministic algorithm; then the ETH states that c3 > 0. The strong exponential-time hypothesis (SETH) additionally conjectures that the limit of the sequence c3, c4, . . . tends to 1, which in particular is known to imply that the satisfiability problem for clauses of arbitrary length (CNF-SAT) is not solvable in 2cn time for any c < 1 [Calabro et al., 2009].

Quantified Boolean Formulas. Boolean expressions, formulas, variables, literals, conjunctive normal form (CNF) and clauses are defined in the standard way (cf. [Biere et al., 2021]). We treat 1 and 0 as the truth-values "true" and "false", respectively, and clauses in CNF as sets of literals. We will assume that no clause contains a literal twice or a literal and its negation, and no clause is repeated in any formula. A quantified Boolean formula is of the form Q.ϕ, where Q = Q1x1 . . .Qnxn with Qi ∈ {∀, ∃} for all 1 ≤ i ≤ n is the (quantifier) prefix, x1, . . . , xn are variables, and ϕ is a propositional Boolean formula ϕ on these variables called the matrix. If Qi = ∀, we say that xi is a universal variable, and if Qi = ∃, we say that xi is an existential variable.

For a Boolean formula ϕ, a variable x and value b ∈ {0, 1}, define ϕ[x = b] to be the formulas obtained from ϕ by replacing every occurrence of x with b. The truth value of a formula Q.ϕ is defined recursively. Let Q = Q1x1 . . . Qnxn and Q′ = Q2x2 . . . Qnxn. Then Q.ϕ is true if

• n = 0 and ϕ is a true Boolean expression, or
• Q1 = ∃ and Q′ .ϕ[x1 = 0] or Q′ .ϕ[x1 = 1] is true, or
• Q1 = ∀ and Q′ .ϕ[x1 = 0] and Q′ .ϕ[x1 = 1] are true.

Otherwise, Q.ϕ is false.

A formula Q.ϕ is a QCNF if ϕ is in CNF, and a Qd-CNF if ϕ is in d-CNF, i.e. a CNF where every clause has size at most d. For a clause C in a QCNF, we use C ∃ and C ∀ to denote the restriction of C to existential and universal variables, respectively. If ϕ is in CNF, then ϕ[x = 0] can be simplified by removing every clause containing literal x, and removing literal x from the remaining clauses. Analogously, ϕ[x = 1] is simplified by removing every clause containing the literal x, and removing the literal x from the remaining clauses.

Let Q.ϕ be a formula such that Q1 = · · · = Qi = ∀ and Qi+1 = · · · = Qn = ∃ for some 1 ≤ i ≤ n. Then we write that Q.ϕ is a ∀∃BF, and replace BF by CNF and d-CNF if ϕ is in CNF and d-CNF, respectively.

Following the convention in the literature, we write QBFSAT for the problem of deciding whether a QCNF is true, and by d-QBFSAT, ∀∃QBFSAT and ∀∃d-QBFSAT we denote the same problem restricted to Qd-CNF, ∀∃CNF and ∀∃d-CNF formulas, respectively.

3 Algorithms for QBFSAT

We show that QBFSAT parameterized by the number of existential variables and the maximum size of any clause is lineartime fixed-parameter tractable, i.e., with a running time linear in the size of formula. The algorithm is based on a chain of reductions involving two novel natural problems and for which we provide corresponding fixed-parameter algorithms along the way. We begin by defining the OR-CNF TAUTOLOGY problem.

OR-CNF TAUTOLOGY

INSTANCE: A set of variables X and d-CNF formulas

ϕ1, . . . , ϕk on X.

QUESTION: Is ϕ1 ∨ · · · ∨ ϕk a tautology?

The following lemma follows via an application of quantifier elimination.

Lemma 1 (⋆). There is an algorithm that takes a Qd-CNF Q.ϕ with k existentially quantified variables, and in time O(2k |ϕ|) constructs an instance I of OR-CNF TAUTOLOGY with 2k d-CNF formulas of size at most |ϕ| such that Q.ϕ holds if and only if I is a yes-instance.

As the next step, we provide a polynomial-time reduction from OR-CNF TAUTOLOGY to the problem of finding an independent set of size k in a well-structured graph. For a set of variables X and integer d, let C dX be the set of all clauses with exactly d distinct literals over variables in X. A pair (G, λ) is a k-partite d-clause graph over X if G is an undirected kpartite graph with V (G) = V1⊎· · ·⊎Vk, and λ : V (G) → C dX is a function, injective on Vi for every i ∈ [k]. Moreover, two vertices u ∈ Vi and v ∈ Vj in G are connected by an edge if and only if i ̸= j and λ(u) and λ(v) clash, i.e. they contain a pair of opposite literals. The problem of finding an independent set in such a graph can be formally defined as follows.

CLAUSE-GRAPH INDEPENDENT SET

INSTANCE: A k-partite d-clause graph (G, λ) over X.

QUESTION: Is there an independent set S ⊆ V (G)

such that |S ∩ Vi| = 1 for all 1 ≤ i ≤ k?

In the following we will use λ-1 as the inverse of λ, which is well-defined if the part Vi is clear from the context since λ is injective on every part Vi. We also use λ(S) to denote the set {λ(v) : v ∈ S} for every set S ⊆ V .

Lemma 2. There is a linear-time reduction that takes an instance I = (X, {ϕ1, . . . , ϕk}) of OR-CNF TAUTOLOGY, where each ϕi is a d-CNF, and produces an instance I ′ = (G,X, λ) of CLAUSE-GRAPH INDEPENDENT SET where (G, λ) is a k-partite d-clause graph over X with the i-th part having at most |ϕi| vertices such that I is a no-instance if and only if I ′ is a yes-instance.

Proof. Given an instance I of OR-CNF TAUTOLOGY, construct the k-partite d-clause graph (G, λ) over X by letting V (G) = V1 ⊎· · ·⊎Vk, where Vi contains one vertex v for every clause C in ϕi, and setting λ(v) = C; by the assumption that all clauses in ϕi are distinct, this definition ensures that λ is injective on every part Vi. For every 1 ≤ i < j ≤ n and every u ∈ Vi and v ∈ Vj , add an edge {u, v} to G if clauses λ(u) and λ(v) clash. To ensure that every clause λ(v) contains exactly d literals, we add d - 1 new variables to X and add d-|λ(v)| of those positively to the clause λ(v). Note that this does not modify the edge set of the graph because all new variables only occur positively. The ideas behind the reduction is illustrated in Figure 1. Clearly, this reduction requires polynomial time.

For correctness, first assume that I is a no-instance, i.e. ϕ1 ∨ · · · ∨ ϕk is not a tautology. Then there exists an assignment α : X → {0, 1} that falsifies every formula ϕi. For each 1 ≤ i ≤ k, let Ci be a clause in ϕi falsified by α, and let vi ∈ Vi be the vertex of G such that λ(vi) = Ci. Observe that α satisfies ∧ki=1 ¬Ci = ∧ℓ∈C1∪...Ck ℓ, hence no pair of clauses Ci and Cj clash. By construction of G, this implies that there is no edge between vi and vj for any i and j, i.e. {vi : 1 ≤ i ≤ k} is an independent set in G.

Now suppose I ′ is a yes-instance, i.e. G contains an independent set S = {v1, . . . , vk}, where vi ∈ Vi for all 1 ≤ i ≤ k. By construction of (G, λ), no two clauses λ(vi) and λ(vj) clash. Observe that ϕ′ = ∧ki=1 ¬λ(vi) is a conjunction of literals, and it contains no two opposite literals, hence ϕ′ is satisfiable. Any assignment α′ : X → {0, 1} that satisfies ϕ′ falsifies at least one clause in every formula ϕi, namely λ(vi). Thus, α′ falsifies ϕ1 ∨ · · · ∨ϕk, proving that it is not a tautology.

The following theorem shows that CLAUSE-GRAPH INDEPENDENT SET is in XP parameterized by k only.

Theorem 3 (⋆). CLAUSE-GRAPH INDEPENDENT SET can be solved in time O((maxki=1 |Vi|)k d(k2)) and is therefore in XP parameterized by k.

Now we will show that CLAUSE-GRAPH INDEPENDENT SET is in FPT parameterized by k and d. To this end, we will use the sunflower lemma. For a family F of sets over some universe U, we say that a subset S ⊆ F is a sunflower if there is a subset C ⊆ U such that F ∩F ′ = C for every two distinct F, F ′ ∈ S, i.e. all pairs of distinct sets in S have a common intersection C, which we also call the core of the sunflower. If S is a sunflower with core C and F ∈ S, then we call F \C

the petal of F . Observe that the petals {F \ C | F ∈ S} of a sunflower are pairwise disjoint.

Lemma 4 ([Erd¨os and Rado, 1960]). Let F be a family of subsets of a universe U, each of size exactly b, and let a ∈ N. If |F| ≥ b!(a - 1)b , then F contains a sunflower S of size at least a. Moreover, S can be computed in time O(|F|d).

For a graph G and a vertex v, we write G - v to denote the graph obtained from G by deleting the vertex v with all incident edges.

Lemma 5. Let (G, λ) be a k-partite d-clause graph, and Vi be one of the parts. If the family λ(Vi) contains a sunflower S of size at least s = (k - 1)d + 2, then, for every v with λ(v) ∈ S, instances (G, λ,X) and (G- v, λ,X) of CLAUSE-GRAPH INDEPENDENT SET are equivalent.

Proof. Let S be the sunflower in λ(Vi) of size at least s, let F ∈ S be an arbitrary clause in S, and v = λ-1 (F) be the corresponding vertex in G. We claim that v satisfies the statement of the lemma, i.e. (G, λ) has an independent set S with |S∩Vi| = 1 if and only if so does (G-v, λ). The reverse direction of the claim is clear since G-v is a subgraph of G.

Towards showing the forward direction, let S be a solution to (G, λ,X). If v /∈ S, then S is also a solution to (G - v, λ,X). Now suppose that v ∈ S. We claim that there exists a clause F ′ ∈ S such that F ′ does not clash with any clause λ(u) for u ∈ S \ {v}, so we can replace v with v′ = λ-1 (F ′ ) in the independent set S. To this end, let S′ = S \ v and let C be the core of S. Note that every clause contains exactly d literals, therefore it can share variables with the petals of at most d clauses in S. Thus, the clauses in λ(S′ ) share variables with at most |S′ |d = (k - 1)d petals of S in total. Since |S \{F}| ≥ s-1 = (k-1)d+1, there is a clause F ′ ∈ S \ {F} whose petal F ′ \ C shares no variables with any clause in λ(S′ ). Moreover, the core C ⊆ F does not clash with any clause in λ(S′ ) since v = λ-1 (F) is not adjacent to any vertex in S′ . Therefore, v′ = λ-1 (F ′ ) is not adjacent to any vertex in S′ and S′ ∪ {v′ } is an independent set in G- v.

Theorem 6. CLAUSE-GRAPH INDEPENDENT SET has a kernel with at most d!(s - 1)d - 1 vertices in every part Vi, where s = (k - 1)d + 2. Note that this implies that CLAUSE-GRAPH INDEPENDENT SET has a kernel of size at most dkd!(s - 1)d . The kernel can be computed in time O(min{d!(s - 1)dd|V (G)|, d|V (G)|2 }).

Proof. Let (G, λ) be a k-partite d-clause graph with parts V1, . . . , Vk over some variables X. If |Vi| < d!(s - 1)d for every i ∈ [k], where s = (k - 1)d + 2, then the instance is already kernelized. So suppose that |Vi| ≥ d!(s - 1)d . By Lemma 4, λ(Vi) has a sunflower S of size at least s, and S can be found in polynomial time. Note that by taking any subset V ′ ⊆ λ(Vi) of size at least d!(s - 1)d , S can be found in time O(min{d!(s - 1)dd, d|V (G)|}). Then, by Lemma 5, we can remove any vertex in λ-1 (S) from Vi and obtain an equivalent but smaller instance. Therefore, applying this procedure exhaustively, we obtain in polynomial time an equivalent instance of CLAUSE-GRAPH INDEPENDENT SET such that |Vi| < d!(s - 1)d for every

1 ≤ i ≤ k. Notice that we need to apply the above procedure O(|V (G)|) times and hence the running time is at most O(min{d!(s - 1)dd|V (G)|, d|V (G)|2 }).

Corollary 7. CLAUSE-GRAPH INDEPENDENT SET is fixedparameter tractable parameterized by k + d. In particular, it can be solved in time (dk)O(dk) |V (G)|.

Proof. The statement that CLAUSE-GRAPH INDEPENDENT SET is fixed-parameter tractable parameterized by k + d follows immediately from Theorem 6. Let (G, λ) be a k-partite d-clause graph with parts V1, . . . , Vk over some variables X. First we can employ Theorem 6 to obtain the kernel (G′ , λ′ ) with parts V ′ 1 , . . . , V ′ k in time d!(s - 1)dd|V (G)|, where s = (k-1)d+2, that is equivalent to (G, λ) and satisfies |V ′ i | ≤ d!(s-1)d . We can then use Theorem 3 to solve the instance (G′ , λ′ ) of CLAUSE-GRAPH INDEPENDENT SET in time O((maxki=1 |V ′ i |)k d(k2)) = O((d!)k (s - 1)dk d(k2)), which is bounded from above by (dk)O(dk) . Altogether, we therefore obtain (dk)O(dk) + O(d!(s - 1)dd|V (G)|), which is bounded by (dk)O(dk) |V (G)| as the running time of our algorithm.

Combining Lemma 2 and Lemma 1, we obtain:

Corollary 8. There is a reduction that takes a Qd-CNF Q.ϕ with k existentially quantified variables, and in time O(2k |ϕ|) produces an instance I ′ = (G, λ,X) of CLAUSE-GRAPH INDEPENDENT SET where (G, λ) is a 2k -partite d-clause graph over X with each part having at most |ϕ| vertices such that I is a no-instance if and only if I ′ is a yes-instance.

We now show that QBFSAT with k existential variables and clauses of size d is in FPT parameterized by k + d.

Theorem 9. QBFSAT is fixed-parameter tractable parameterized by the number k of existential variables plus the maximum size d of any clause. In particular, there is an algorithm solving this problem in time (2k d)O(2k d) |ϕ| for a QCNF formula Q.ϕ.

Proof. Let Φ = Q.ϕ be the given QBFSAT formula with k existential variables having clauses of size at most d. We first use Corollary 8 to obtain in time O(2k |ϕ|) the 2k -partite d-clause graph (G, λ) with parts V1, . . . , V2k such that Φ is false if and only if (G, λ) has an independent set S with |S ∩ Vi| = 1. We then use Corollary 7 to decide in time (d2k )O(d2k ) |V (G)| = (d2k )O(d2k ) 2k |ϕ| = (d2k )O(d2k ) |ϕ| whether (G, λ) has an independent set S with |S ∩ Vi| = 1. If so, we return that Φ is false, otherwise we return that Φ is true. Altogether the total runtime of the algorithm is at most (d2k )O(d2k ) |ϕ|.

Last, via a straightforward algorithm we remark that QBFSAT is in XP parameterized by the number of existential variables. As we will see in Section 5 this problem is unlikely to admit an FPT algorithm unless FPT=W[1].

Theorem 10 (⋆). QBFSAT is in XP parameterized by the number k of existential variables. In particular, QBFSAT can be solved in time O(m2k d(k2) + 2k |ϕ|) for a QCNF-formula Q.ϕ with m clauses.

4 The QCSP Problem

We now consider the finite-domain generalization of QBFSAT known as the quantified constraint satisfaction problem (QCSP). An instance of the constraint satisfaction problem (CSP) (without quantifiers) is (X,D,C), where X = {x1, . . . , xn} is a set of variables, D = {D1, . . . ,Dn} is a set of domains (of values) for each variable, and C = {C1, . . . ,Cm} is a set of constraints, where Cj = Rj(xj1 , . . . , xjar(Rj) ), Rj ⊆ Dj1 ×· · ·×Djar(Rj) is a relation of arity ar(Rj), and 1 ≤ j1, . . . , jar(Rj) ≤ n. The instance is satisfiable if there exists an assignment α : X → ⋃ni=1 Di of values to the variables such that α(xi) ∈ Di for all i ∈ [n], and (α(xj1 ), . . . , α(xjar(Rj) )) ∈ Rj for all constraints in j ∈ [m]. Let d = maxni=1 |Di| be the largest domain size and r = maxmj=1 ar(Rj) be the maximum arity of a constraint in C. For example, 3-SAT can be cast as CSP with d = 2 (every variable is assigned a Boolean value) and r = 3 (every clause is a ternary constraint).

Parameterized complexity of the CSP with respect to n, d and r is well-understood [Samer and Szeider, 2010]: the problem is in FPT parameterized by n+d, W[1]-hard parameterized by n+r, in XP parameterized by n, and paraNP-hard parameterized by d + r.

QCSP is a generalization where the input additionally comes with a set of quantifiers Q = (Q1, . . . , Qn). The basic notions in Section 2 easily extends to the CSP setting and we write QCSP for the (PSPACE-complete) decision problem of verifying whether an instance Q.ϕ is true or false, where ϕ is a CSP instance over the variables occurring in the quantifier prefix Q. Naturally, if a variable xi has domain Di then we in the context of a universal quantifier require that the subsequent formula is true for all values in Di, and for at least one value in Di if the quantifier is existential. We manage to generalize Theorem 9 to QCSP.

Theorem 11 (⋆). QCSP is FPT when parameterized by the number of existentially quantified variables, the domain, and the maximum arity of any relation.

It is worth remarking that by Samer & Szeider [Samer and Szeider, 2010] and the forthcoming Theorem 15 each of the above three conditions are necessary in the sense that we obtain a W[1]-hard problem if any condition is dropped.

5 Lower Bounds

We proceed by complementing our positive FPT result by two strong lower bounds. We begin by ruling out an FPT algorithm for ∀∃QBFSAT parameterized by the number of existential variables for unbounded clause size via a reduction from the W[1]-complete problem MULTIPARTITE INDEPENDENT SET. Using the following auxiliary result, we strengthen this result even further under the ETH.

Theorem 12 ([Chen et al., 2006], cf. Theorem 14.21 in [Cygan et al., 2015]). Assuming the ETH, there is no algorithm that decides if a graph on n vertices has an independent set of size k in f(k) · no(k) time for any computable function f.

For our purposes, it is more convenient to work with the following variant of the INDEPENDENT SET problem. In MULTIPARTITE INDEPENDENT SET, an instance is a graph with the vertex set partitioned into k parts, and the question is whether the graph contains an independent set with one vertex from each part. Using a well-known reduction (cf. Section 13.2 in [Cygan et al., 2015]) that takes an instance (G, k) of INDEPENDENT SET and constructs in polynomial time an equivalent instance of MULTIPARTITE INDEPENDENT SET with |V (G)|k vertices and the same parameter k, we obtain the following corollary.

Corollary 13 (⋆). Assuming the ETH, there is no algorithm that solves MULTIPARTITE INDEPENDENT SET in f(k) · no(k) time for any computable function f.

Lemma 14. There is a polynomial-time reduction that takes an instance (G, k) of MULTIPARTITE INDEPENDENT SET and produces in polynomial time a ∀∃CNF formula with ⌈log2(k)⌉ existential variables such that (G, k) is a yesinstance if and only if the formula is false.

Proof. Let G be a graph with vertex set V1 ⊎ · · · ⊎ Vk. It will be convenient to assume that k is a power of two. To this end, let κ = ⌈log2(k)⌉, and add 2κ - k new parts to V (G), each consisting of one isolated vertex. Clearly, the new instance is equivalent to the original one, so we assume from now on that k = 2κ . Enumerate vertices in each part of the graph. For convenience, we refer to vertex j in part Vi as (i, j).

We will construct a formula ∀Y ∃X.ϕ on variables Y = {yv : v ∈ V (G)} and X = {x1, . . . , xκ} that is false if and only if (G, k) has an independent set with exactly one vertex from every part. To this end, enumerate all functions α1, . . . , αk from X to {0, 1}. For every vertex v = (i, j) ∈ V (G′ ), add a clause Cv to ϕ with the following literals:

• yv and yu for all u ∈ V (G) \ Vi such that {u, v} ∈ E(G),
• xℓ if αi(xℓ) = 0 and xℓ if αi(xℓ) = 1 for all ℓ ∈ [k].

This completes the construction.

Towards correctness, first assume that S is an independent set in G with one vertex from each Vi. Consider the set of clauses CS = {C ∀ v : v ∈ S}; recall that C ∃ and C ∀ for a clause C denotes the restriction of C to existential and universal variables, respectively. We claim that there is an assignment that falsifies every clause in CS. It suffices to show that no pair of clauses in CS clashes, i.e. contain opposite literals. Consider two clauses C ∀ u , C ∀ v ∈ CS. Since S is an independent set, u and v are not adjacent, so C ∀ u does not contain yv and C ∀ v does not contain yu. Furthermore, both C ∀ u \{yu} and C ∀ v \{yv} only contain negative literals, so they do not clash either. Now, let τ : Y → {0, 1} be an assignment that falsifies all clauses in CS. We claim that ∃X.ϕ[τ] is false, i.e. ϕ[τ] is not satisfiable. Indeed, for every assignment αi : X → {0, 1}, there is a vertex v = (i, j) ∈ S in G, and hence a clause C ∃ v remains in ϕ[τ], which excludes αi as the satisfying assignment. Thus, all assignments are excluded, and ∃X.ϕ[τ] is false.

For the other direction, suppose ∀Y ∃X.ϕ is false. Then there exists an assignment τ ′ : Y → {0, 1} such that ∃X.ϕ[τ ′ ] is false, i.e. ϕ[τ ′ ] is not satisfiable. By construction, every clause of ϕ[τ ′ ] is a κ-clause with literals over all variables x1, . . . , xκ. Each such clause excludes exactly one satisfying assignment, so ϕ[τ ′ ] contains exactly 2κ = k clauses. Thus, for every assignment αi : X → {0, 1}, there exists a clause Cv where v ∈ Vi and τ ′ falsifies C ∀ v . Pick one such clause Cv for every i, and let vertices v form a set S. We claim that S is an independent set in G. Suppose towards contradiction that u, v ∈ S and {u, v} ∈ E(G). By construction, yu ∈ C ∀ u and yu ∈ C ∀ v , so τ ′ cannot falsify both of them, which contradicts our choice of u, v.

Theorem 15. ∀∃QBFSAT is W[1]-hard parameterized by the number of existential variables. Moreover, assuming the ETH, this problem cannot be solved in f(k) · |ϕ|o(2k ) time for any computable function f : N → N, where Q.ϕ is the ∀∃CNF with k existential variables.

Proof. W[1]-hardness is immediate from Lemma 14 and the fact that MULTIPARTITE INDEPENDENT SET is W[1]-hard. Moreover, if there is an algorithm deciding whether a ∀∃CNF with matrix ϕ and κ existential variables is true or false in f(κ) · |ϕ|o(2κ ) time for any computable function f , then it can be combined with the reduction of Lemma 13 to solve MULTIPARTITE INDEPENDENT SET in f(⌈log2 k⌉) · 2o(k) time, contradicting the ETH.

For lower bounds for ∀∃3-QBFSAT, we first observe that this problem cannot be solved in 2o(k) · |ϕ|O(1) time under the ETH (since we have a trivial reduction from 3-SAT). However, we can significantly sharpen this under the SETH and in fact rule out every 2O(k) time algorithm, i.e. the problem is not solvable in ck · |ϕ|O(1) time for any constant c ≥ 1. We rely on the following result.

Theorem 16 ([Calabro et al., 2013]). Assuming the SETH, ∀∃3-QBFSAT is not solvable is O∗ (cn ) time 1 for any c < 2.

Theorem 17. Assuming the SETH, ∀∃3-QBFSAT parameterized by the number of existentially quantified variables k is not solvable in ck · |ϕ|O(1) time for any constant c.

Proof. Let k and ℓ denote the number of existential and universal variables in an input formula, respectively, and let n = k + ℓ. We consider two algorithms for ∀∃3-QBFSAT. The first one is the hypothetical FPT algorithm that solves ∀∃3-QBFSAT in O∗ (ck ) time for constant c. The second algorithm enumerates assignments to universal variables, and solves the resulting 3-SAT formulas. The latter requires O(2ℓ c3 k ) time, where c3 the infimum of all b such that 3-SAT is solvable in O∗ (bn ) time. Observe that c3 < 2. Now, let δ = k/n be the proportion of existential variables in the input formula. We claim that, depending on the value of δ, we can use either the first or the second algorithm to solve ∀∃3-QBFSAT in O∗ (dn ) time for some d < 2, contradicting SETH by Theorem 16. To this end, define T = 1+log2(c)-log2(c3), and observe that T ≥ 1 since ∀∃3-QBFSAT is more general than 3-SAT and c ≥ c3.

First, suppose δ > 1/T, i.e. k > n/T. Then use the first algorithm, which runs in O∗ (cn/T ) = O∗ (2(log2 (c)/T )n )

1 The notation O∗ hides factors polynomial in n.

time. Now suppose δ ≤ 1/T , i.e. k ≤ n/T . Then use the second algorithm, which runs in O∗ (2(1-δ)n c3 δn ) time. Observe that (1-δ)+log2(c3)δ ≤ 1-(1-log2(c3))/T ≤ log2(c)/T . In both cases, our algorithm runs in O∗ (2(log2 (c)/T)n ) time. Since c3 < 2, we have log2(c3) < 1 and log2(c) < T , which completes the proof.

6 Discussion

In this paper we investigated a simple and overlooked parameter for QBFSAT and proved FPT with respect to the number of existentially quantified variables and the maximum arity of any clause. This parameterization is particularly noteworthy since applied QBF solving is frequently based on the idea of expanding universally quantified variables in order to get an instance that can be solved with SAT techniques. This strategy comes with the downside that (1) after removing universally quantified variables one still needs to solve an NP-hard problem, and (2) the strategy is inefficient for instances with many universally quantified variables. Our result is complementary in the sense that instances with many universal but few existential variables can now be handled efficiently with our novel FPT algorithm. While we in this paper concentrate on the theory it is natural to speculate whether these two approaches can be merged in actual QBF solvers to solve previously intractable instances faster.

For improvements, there is a gap between our 2O(k2k ) FPT algorithm and our lower bound (under the SETH) which rules out any single-exponential 2O(k) algorithm. It is not immediately which direction could be strengthened and new algorithmic ideas would likely be needed to bring down the running time to 2O(kc ) for some fixed c. It would also be interesting to generalize our FPT algorithm to even broader classes of problems. A promising candidate is the depedency quantified Boolean formula (DQBF) formalism, i.e. Boolean formulas equipped with Henkin quantifiers. This problem is generally NEXPTIME-complete and has comparably few FPT results. Naturally, Lemma 1 would need to be modified to the DQBF setting, but besides that the main ideas should carry over.

From a purely theoretical perspective rather little is known about the logical fragment where we allow unrestricted universal quantification but only limited existential quantification. As a starting point one could define a closure operator on sets of Boolean relations induced by logical formulas allowing universal but no existential quantification over conjunctions of atoms from a predetermined structure. Such formulas would generalize quantifier-free primitive positive definitions (qfpp-definitions) which has been used to study fine-grained complexity aspects of CSPs [Lagerkvist and Wahlstr¨om, 2022], but be more restrictive than the formulas considered by B¨orner et al. [2003] developed to study classical complexity of QCSPs. Could it, for example, be possible to give a classification akin to Post's classification of Boolean clones, or find a reasonable notion of algebraic invariance? A reasonable guess extending B¨orner et al. [2003] would be to consider algebras consisting of partial, surjective polymorphisms.

Acknowledgements

The second author is partially supported by the Swedish research council under grant VR-2022-03214. The fourth author was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.