The Riis Complexity Gap for QBF Resolution

1.Introduction

The Complexity Gap Theorem [23] considers a translation of a first-order sentence ϕ to a sequence of propositional formulas, and states that the complexity of refuting these propositional formulas in tree-like Resolution depends on whether ϕ has any [in]finite models. The nth member of the sequence of propositional formulas is satisfiable if and only if ϕ has a model of size n. When ϕ has an infinite model but no finite models then all tree-like Resolution refutations of related propositional formulas are exponential in size. When ϕ also has no infinite model then there must exist polynomial-size tree-like Resolution refutations of the propositional formulas.

Quantified Boolean logic is an extension of propositional logic in which variables may be existentially or universally quantified. Determining the truth value of a quantified Boolean formula (QBF) naturally extends the satisfiability problem (SAT) on propositional formulas, and the success of SAT solving algorithms has motivated the development of QBF solvers and proof systems [12]. Recent research has sought to understand which proof-theoretic techniques lift to the QBF setting [1,7,8] as well as developing QBF specific techniques [2,4,6,13].

We investigate whether the Complexity Gap Theorem holds in various QBF resolution systems [5,18,19,24]. We first introduce a method to translate a first-order sentence ϕ to a sequence of QBFs, which echoes similar translations of quantified constraint satisfaction problems (QCSPs) to QBFs that have appeared in [16,17]. The translation will ensure that the nth member of the sequence has size at most polynomial in n, and is true precisely when ϕ has a model of size n.

We demonstrate that tree-like Q-Resolution [19] will always require exponential size to refute the nth member of the sequence of QBFs when ϕ has an infinite model but no finite model. However, unlike the propositional case, there exist formulas with no models but requiring exponential sized tree-like Q-Resolution refutations for the nth member of the sequence. We show that if the first-order formula ϕ is embellished with additional structure (precisely defined in Section 6) to obtain a formula ϕ∗ before applying the translation then tree-like Q-Resolution is able to refute the nth member of the sequence in polynomial time precisely when ϕ has no models. Our main result is:

Thus we obtain, à la Riis, a gap between polynomial and exponential in which certain growth behaviours (e.g. subexponential 2i) are forbidden.

We prove that the same phenomenon holds in the system of tree-like QU-Resolution [24], which extends tree-like Q-Resolution. In contrast, in the QBF resolution system of tree-like ∀Exp+Res from [18], modelling QBF expansion solving, the gap holds naturally, that is without the embellishment. In this sense, ∀Exp+Res does not possess the same deficiency as tree-like Q-Resolution.

2.Preliminaries

We restrict attention to QBFs in closed prenex conjunctive normal form, Ψ=Qψ, where ψ is a propositional formula (in CNF). The prefix Q takes the form Q1x1Q2x2…Qkxkψ where Qi∈{∀,∃}, xi are distinct Boolean variables. In closed formulas, all the variables in ψ must appear in Q. The prefix also enforces a partial order on the variables. If Qi=Qi+1 we say xi and xi+1 are in the same quantifier level in the prefix. If xi and xj are not in the same quantifier level and i<j, then we say that xj has higher quantification level than xi. Variables in the same level may be reordered arbitrarily to create another logically equivalent QBF, but otherwise changing the order that variables appear in the prefix may not preserve the truth value of Ψ. Where convenient to do so we write the quantifier once per level rather than for each variable.

Q-Resolution consists of a resolution rule and universal reduction. The resolution rule is

where C and D are clauses and x is an existentially quantified variable, and for all variables y≠x that appear in C, the negation of y does not appear in D. We call x the pivot of this resolution step.

The universal reduction rule is

where x is universally quantified and belongs to the inner-most quantifier level of all variables appearing in C.

A QBF is false if and only if it is possible to derive the empty clause by application of these rules. A Q-Resolution refutation of Ψ is a sequence of clauses C1…Cn such that every Ci is either a clause from ψ, derived by resolution from Cj and Ck (j,k<i) or derived by ∀-reduction from Cj (j<i). A Q-Resolution proof has an underlying DAG structure, with edges denoting inference either by resolution or reduction. In a tree-like Q-Resolution proof this graph must be a tree. Each derived clause can therefore only be used once in the proof.

QU-Resolution [24] is similar to Q-Resolution except that the pivot of a resolution step is also permitted to be universally quantified.

Finally, ∀Exp+Res [18] describes an alternative approach to QBF solving in which existentially quantified variables are expanded according to different possible Boolean assignments to the universal variables. This produces an entirely existential formula that can be refuted by propositional Resolution. When an axiom is downloaded into a ∀Exp+Res proof, some complete assignment μ to the universal variables is implicitly being considered. For C a clause in ψ, the assignment will be one which does not automatically satisfy the clause (i.e. if universal literal u appears in C then μ will set u=0). The universal literals in C are falsified by the assignment and so are removed, and each existential variable x in C is annotated with μ, to show which part of the expanded formula it relates to. Because x can only depend on universal variables that appear in an earlier level than x in the quantifier prefix, μ is truncated for each existential literal in C to only reference the part of the assignment that is relevant for this literal.

If μ and ω are distinct assignments to universal variables appearing before x in the prefix, then xμ and xω are distinct, existentially quantified variables, and μ and ω are referred to as annotations of xμ and xω. Every clause in a ∀Exp+Res refutation is either introduced in this way as an axiom, or is the result of a propositional resolution step between some xμ and ¬xμ.

3.Rendering a First-Order Sentence as a Sequence of QBFs

We now give a method to translate a first-order sentence ϕ to a sequence ⟨Φi⟩i∈N of QBFs. We consider first-order logic to be relational and possibly with constants. Functions can be encoded as relations in the standard way. The method is inspired by the encoding of ϕ into propositional formulas in conjunctive normal form (CNF) previously given by Riis [23], and is similar to other translations used to encode QCSP instances as QBF in [16]. A more succinct “binary” or “logarithmic” form of encoding is discussed in [17] but for our purposes, since ϕ is fixed, the benefit of this more succinct encoding is not important.

We begin with a first-order sentence

Each first-order variable x becomes n Boolean variables x1,…,xn. If xi is made true this indicates that x is evaluated as the ith element in a model of size n. We introduce existentially quantified variables associated with each instantiation of a relational predicate Rij(λ1,…,λk) indicating that the tuple (λ1,…,λk) is in the relation Rij.

In the original sentence a variable x can only take on one value at a time, and must be given some value. We introduce clauses so that if any existential variable is not given exactly one value the QBF is falsified, and if any universal variable is not given exactly one value then the QBF is made true. Let [n]:={1,…,n}. ∑i∈[n]xi=1 asserts that precisely one of the xi is true, i.e. it is an abbreviation for (∨i∈[n]xi)∧∧j≠i∈[n](¬xi∨¬xj). Similarly ¬(∑i=1nxi=1) is shorthand for the conjunction of clauses (¬xi∨∨j≠ixj).

We can now build our sequence of QBFs

By construction, ϕn is true if and only if ϕ has a model of size n (the size of the domain). The quantifier-free part of ϕn can be expanded to CNF and this expansion is not of size larger than polynomial in n. If the disjuncts Di contain equality relationships between variables then these can be enforced by restriction of the λ1,…,λk∈[n]; indeed, if the disjuncts only involve some subset of x1,…,xk then plainly only those need be mentioned. We call Boolean variables of the form Rij(λ1,…,λk), always existentially quantified outermost, relational variables.

4.The Lower Bound

In this section we lift Riis’ proof to show the following result.

We use the game of [9] for tree-like Q-Resolution, which we now recall. The game proceeds between a Prover and Delayer, who build a partial assignment to the variables of a QBF Φ. The game starts with the empty assignment and ends when the current assignment falsifies the matrix of Φ. Each round of the game has the following phases:

Intuitively, the points scored by Prover correspond to the depth of the proof, and for full binary trees, the tree size is exponential in the depth of the tree. Thus exhibiting good Delayer strategies that score many points will lead to lower bounds for proof size. This is the intuition of the original Prover–Delayer game from [22]. Using the more refined version of the game with weights as described above (originating from [9,11]) the game exactly characterises tree-like Q-Resolution size. An example for a Delayer strategy for propositional tree-like Resolution on the pigeonhole formulas is contained in [10]. More examples for tree-like Q-Resolution can be found in [9].

Assignments made in the query phase correspond to branching points in the tree. In particular, if there exists a strategy and some choice of weighting, such that Delayer is guaranteed at least p points in a game on Φ, regardless of how Prover behaves, then any tree-like Q-Resolution refutation of Φ must have size at least 2p. We give such a strategy for Delayer on any QBF generated through the above translation, for which the underlying first-order formula has an infinite model.

For QBF Φn, representing the (false) statement that the original first-order sentence ϕ has a model of size n, Delayer’s strategy is stated in terms of the set of models that satisfy the original first-order sentence. Let M be the set of all models of ϕ. Delayer cannot win this game since Φn is false, but he can guarantee Ω(n) points, meaning that the tree-like Q-Resolution proof must have size 2Ω(n).

5.A Surprising Lower Bound

Proof: We show a strategy that allows Delayer to score Ω(n) points. Delayer uses the rules below for responding to Prover queries.

In items 1 to 7 Delayer forces Prover to answer according to his wish by setting weights 0 and 1 (Delayer’s preferred choice gets weight 1), but Delayer will not score any points. Thus Delayer only scores a point when item 8 applies.

There are three ways that the QBF can become false. First, by having simultaneously that x=c, y=d, z=e and ¬R(c,d,e). This cannot happen because if x=c and y=d then R(c,d,e) is made true by rule 6, and if x=c and ¬R(c,d,e) then y cannot be given the value d due to rule 2. x cannot be set after y by the rules of Q-Resolution. Second, the QBF could be made false by having simultaneously that u=c, v=d, w=e and R(c,d,e) and similarly this is not possible according to rules 4, 5 and 7. Third, the QBF may become false by failing to assign exactly one value to some existentially quantified variable. The first rule ensures that at most one value is given to each existential variable. Therefore the QBF must become false by failing to assign any value to some existential.

Now we need to show that Delayer scores linearly many points before all possible values are excluded for any existentially quantified variable. We consider the cases when u, w or y is the subject of the conflict.

Values for u are excluded by rules 3 or 4, or may have been excluded directly by a Prover choice scoring one point. Rule 3 can only exclude one value for u at a time. For rule 4 to exclude a value we must have one of the R variables assigned positively, and it must be a different variable for each excluded value of u. Either this was done in a Prover choice (scoring one point) or it was forced by rule 6, but then y must have been assigned its value by a Prover choice (since Delayer rules only exclude values for y). For rule 6 to force R variables that would be able to exclude different values for u it would be necessary to change the assignment to x, which requires forgetting and re-querying y. Therefore, if the game ends by ruling out all values of u then Delayer has scored at least n−1 points.

If instead it is w that has every value excluded then for each of these values we have either that it was set in a Prover choice and Delayer scores one point, or else it was forced through rule 5. Rules 3 and 4 ensure that it is not possible to have simultaneously u=c and R(c,d,e) unless R(c,d,e) was assigned in a Prover choice, and a different R assignment would be needed for each excluded value of w. If the game ends by exhausting all possible assignments to w then Delayer has scored at least n points.

Finally, if the game ends because no value is assigned to y then for each of the possible values either it was excluded in a choice made by Prover or it was excluded by rule 2. A different R variable would be needed for each excluded value of y, and they could only have been forced by rule 7 requiring a new assignment to v and so a new positive assignment to w for each one. In this case Delayer scores at least n points before the game ends.

Because Delayer must score Ω(n) points by the end of the game we have that any tree-like Q-Resolution proof of Θn has size Ω(2n).  □

This lower bound is surprising because if the result of [23] lifted directly to Q-Resolution on this natural translation to QBF then we would expect a formula without any models to yield a sequence of QBFs with polynomial size Q-Resolution proofs. We would expect these short proofs to use the refutation of the first-order formula itself as a basis, similar to the methods used in [14,23]. We briefly discuss why this approach fails for Q-Resolution.

Figure 1.

Universal variables are replaced by free variables (lower case with indices), existential variables are written as functions (upper case) over those free variables. The tableau is closed by the unification Unif: x2←U1(x1,z1), v1←Y2(x2), z2←W1(x1,z1,v1). Through this substitution we have twin atoms R(U1(x1,z1),Y2(x2),W1(x1,z1,v1)) and ¬R(U1(x1,z1),Y2(x2),W1(x1,z1,v1)) which resolve to a contradiction. For more details on these tableau refutations please see [20].

Consider the tableau refutation in Fig. 1. The unification that closes the tableau suggests a strategy for Prover, which is to query u and set x accordingly, then query y and set v accordingly, then query w and set z to match, at which point the contradiction is immediate. However, the strategy does not respect the order of the quantifier prefix. In the game representing tree-like Q-Resolution all existential assignments at a higher level must be forgotten in order to make a universal assignment at a lower level. Therefore it is not possible for Prover to set x matching u. Disobeying this rule in the game corresponds to using ∀-reduction while existential variables with a higher quantification level remain in the clause and is not sound in general. Our strategy for Delayer shows that this problem cannot be overcome in tree-like Q-Resolution with the proposed translation from the first-order formula to QBF. Instead, we will modify the translation to provide Prover with a mechanism for ‘remembering’ choices that have previously been made, while still respecting the rules of the game. Finally, we show that ∀Exp+Res is able to use the unification to construct a valid strategy and a short proof on the first, more natural, translation to QBF.

6.Embellishing the QBFs

Continuing with the same example, expand the formula by introducing a side condition

We put this expanded formula into prenex form:

The idea is that when the existential variable u is queried and given the value a, Prover can then ask Delayer to identify some specific sub-problem with u=a that evaluates to true. If Delayer refuses to do this, their choice of u in the original formula quickly generates a contradiction, and otherwise x can be set based on the S variable that was made true. In this way, the S variables act as a memory of Delayer’s choices.

We describe the decision tree for this formula. Recall that the QBF is constructed so that if all of the existential variables {xi}i=1n are assigned 0 then the formula is immediately falsified; similarly no universal set {yi}i=1n may have more than one value given at a time, else the formula is immediately satisfied.

For each instance of an existential variable e in the unification closing the tableau refutation, the decision tree has branched once on either e, or e′, as well as branching once on the n variables S(α,∗,γ,a).

This motivating example shows how additional structure derived from the original sentence can aid Prover in the resulting sequence of QBFs. To generalise this method we will introduce new relational variables for each level of the quantifier prefix.

We are now more interested in blocks of variables than individual variables, so represent our general formula with slightly different notation to emphasise this. Take the first-order sentence

It is modified to include new relations Sk,Sk′,…, S1, S1′. The following statement is conjoined to the original.

The models are essentially unchanged by the proposed modification, the number of variables has only increased polynomially, and the arity of the new S relations is still bounded above by the number of variables in the original first-order sentence. Therefore, the proof of the exponential lower bound in the case that ϕ (and so ϕ∗) has an infinite model still applies exactly as given in Section 4.

Proof: Taking an analytic tableau refutation [20] of a logical contradiction ϕ, we explain how to generate a decision tree for Φn. The unification that closes the tableau shows how to determine universal assignments from choices made for the existential variables. Follow the unification in order, expanding existential variables with a branching factor of n. When it is necessary to set a universal variable (unless this can be done within the rules for ∀-reduction), first use the S relations to find a specific sub-problem claimed to be correct for the variables that have been assigned so far. Once in a position to derive R variables (recall these are outermost and existential in our QBF), we do so.

Let ζi (resp. ηi) range over all assignments to variables in the block Xi (resp. Yi). If all S(ζ1,η1,…,ζj,ηj) (similarly S′(ζ1,η1,…,ζj)) are set to false, we work through the sub-sentence

If instead some S(ζ1,η1,…,ζi,ηi) is set true, then any remaining S(ζ1,η1,…,ζi,ηi) do not need to be considered in this branch. The assignments to relational variables (S and R) are never changed on a given branch, and they will form a memory during backtracking, when later existential assignments need to be forgotten in order to make universal assignments.

Let m be the number of Skolem functions in the unification, b the number of variables in the original first-order sentence, n the size of model being searched for. The decision tree branches m times on existential variables, with a branching factor of n. Up to b sets of S variables have been added, each with up to nb members, and we may branch on any of these sets, once only. The size of the decision tree refutation is therefore O(nm⋅nb2).  □

7.Extension to QU-Resolution

Although stated in terms of tree-like Q-Resolution, our result also holds for tree-like QU-Resolution, in which the Resolution rule may be applied to universally, as well as existentially, quantified variables.

Since QU-Resolution contains Q-Resolution, our upper bound immediately transfers. For the exponential lower bound, we note that the game description of tree-like Q-Resolution can be extended to describe QU-Resolution by allowing Prover to query universally quantified variables as well as existentially quantified [9]. This may shorten the refutation, since it offers a way for Prover to set universal variables after existential variables that are later in the prefix have already been assigned. However, it does not affect the crux of our argument, that Ω(n) values must be considered in a free choice at some point during the game, and only constantly many values can be considered in each free choice. Thus, the analogous version of Theorem 1 holds for QU-Resolution as well.

QU-Resolution is exponentially stronger than Q-Resolution in the DAG-like case. This is demonstrated in [24] via the formulas of Kleine Büning, Karpinski and Flögel [19]. It is not known whether a separation exists between the tree-like variants. Our results here mean that such a separation – if it exists – cannot be shown by using translations of first-order formulas as considered here.

8.A Polynomial Upper Bound for ∀Exp+Res

Our observation of the behaviour of tree-like Q-Resolution on the initial translation of these formulas reveals a weakness in the proof system, which can be understood in the game description as Prover lacking memory of previous answers. We show that tree-like ∀Exp+Res does not share this weakness and enjoys short proofs for QBFs generated by our first translation whenever the underlying first-order formula has no models. Thus we have given both a specific example and a schema of QBFs separating tree-like ∀Exp+Res from tree-like Q-Resolution.

Proof: The idea is to use the unification witnessing that ϕ is false to structure the ∀Exp+Res proof. The unification is made up of assignments from the value of a Skolem function to a universal variable. The Skolem function represents an existential variable x and is evaluated for a setting of (a subset of) the universal variables prior x in the quantifier prefix.

We can mimic this process in ∀Exp+Res using the game description for Resolution [11] over annotated variables. Prover queries the value of x with an annotation α. If a variable in the domain of the Skolem function is appearing in the unification for the first time it can be set arbitrarily in α. Otherwise it is given the value already specified earlier in the unification. Because x has been split into x1…xn by the translation to QBF Prover will in fact query some or all of the xi,α until one of them is made true. Then all other xi,α would be forced to false so Prover can move on to the next assignment in the unification.

Once the assignments for the unification have been made Prover can query relational variables to quickly reach a contradiction. Each branch of the tableau contains two entries that are directly contradictory under (part of) the assignment given by the unification. For each branch in turn Prover queries the relations(s) that close the branch using the assignments determined in the first stage of the game. By construction, any sequence of Delayer answers results in an immediate contradiction, in particular some clause of the form (¬x1λ1∨⋯∨xkλk∨Di(λ1,…,λk)) is falsified.

We need to show that Delayer scores O(lg(n)) points. The number of queries of the relational variables does not depend on n. For each query Prover can select the value that gives Delayer the lowest score so each choice has a maximum value of 1 point (when p0=p1=12).

There are also constantly many Skolem functions in the unification, but each of these requires (up to) n queries to assign a value to an (annotated) existential variable. The number of points remains limited to lg(n) points.

To assign a value to xα Prover first queries x1,α. Delayer responds with weights p0 and p1. If p1<1∕n then set x1,α=1 so Delayer scores lg(n) points. Otherwise set x1,α=0. p0<n−1n so Delayer scores lg(nn−1) points.

Over xi,α for i=1,…,j Delayer has either scored lg(n) points and some xi,α=1 or has scored lg(n)−lg(n−j) points and all xi,α=0. If some xi,α=1 then we are done and Prover does not need to query xj+1,α. Otherwise Delayer sets p0 and p1, if p1<=1n−j then Prover sets xj+1,α=1. Delayer scores at most lg(n−j) points for this, so a total of lg(n) points. If p1>1n−j then Prover sets xj+1,α=0 and Delayer scores at most lg(n−jn−j−1) points for this, giving a total of lg(n)−lg(n−j−1) points.

In total Delayer has scored O(lg(n)) points, so the proof size is nO(1).  □

9.Conclusion

We have demonstrated a translation from first-order formulas to QBF families for which a complexity gap exists in tree-like Q-Resolution. Our translation is not as natural as that used in Riis’ original translation to propositional logic, due to an inherent constraint in Q-Resolution that ∀-reduction must respect the order of variables in the prefix. This manifests when trying to construct short tree-like Q-Resolution proofs. Section 5 shows that this is in general not possible for the original FO translations, which is why we need to add additional structure to the translation (the embellishment of Section 6). This bypasses the constraint on ∀-reduction in this setting so that short proofs can be achieved where the original formula had no models. We have also noted that in this setting, tree-like QU-Resolution and Q-Resolution coincide, with the additional power of QU-Resolution providing at most a polynomial improvement in the proof length.

It is not currently known whether there are any situations in which tree-like QU-Resolution is exponentially stronger than tree-like Q-Resolution, the separation of these two systems has only been demonstrated in the DAG-like variant. Generating a series of QBFs from the unsatisfiable first-order formula ∀x∃y∀z∃u∀v∃wR(x,y,z)∧¬R(u,v,w), that has short proofs in tree-like ∀Exp+Res but exponential sized proofs in tree-like Q-Resolution and in fact tree-like QU-Resolution, we have exhibited new formulas that separate the two systems.

Finally, we remark that tree-like Resolution systems – both propositionally and for QBF – are rather weak calculi (which in particular are not strong enough to model solving paradigms such as (Q)CDCL [3,21]). It would be very interesting to explore whether similar gap theorems as shown here and previously in [14,23] can be obtained for stronger calculi, with dag-like (Q)-Resolution being a very interesting case. However, presently we only have quite limited knowledge on this (cf. [15] for some results on dag-like Resolution) with the case of general dag-like Q-Resolution completely unexplored.