Dynamic Dependency Awareness for QBF

1 Introduction

Proof complexity is the study of proof size in systems of formal logic. Since its beginnings the field has enjoyed strong connections to computational complexity [Cook and Reckhow, 1979; Buss, 2012] and bounded arithmetic [Cook and Nguyen, 2010], and has emerged in the past two decades as the primary means for the comparison of algorithms in automated reasoning.

Recent successes in that area, epitomised by progress in SAT solving, have motivated broader research into the efficient solution of computationally hard problems. Amongst them, the logic of quantified Boolean formulas (QBF) is an established field with a substantial volume of literature. QBF extends propositional logic with the addition of existential and universal quantification, and naturally accommodates more succinct encodings of problem instances. This gives rise to diverse applications in areas including conformant planning [Rintanen, 2007; Egly et al., 2017], verification [Benedetti and Mangassarian, 2008], and ontologies [Kontchakov et al., 2009].

It is fair to say that much of the early research into QBF solving [Zhang and Malik, 2002; Samulowitz and Bacchus, 2005; Giunchiglia et al., 2006], and later the proof complexity of associated theoretical models [Beyersdorff et al., 2017a; 2018; 2017b], was built upon existing techniques for SAT. For example, QCDCL [Giunchiglia et al., 2009] is a major paradigm in QBF solving based on conflict-driven clause learning (CDCL [Silva and Sakallah, 1996]), the dominant paradigm for SAT. By analogy, the fundamental theoretical model of QCDCL, the calculus Q-resolution (Q-Res [Kleine B¨uning et al., 1995]), is an extension of propositional resolution, the calculus that underpins CDCL. Given, however, that the decision problem for QBF is PSPACE-complete, it is perhaps unsurprising that the implementation of QCDCL presents novel obstacles for the practitioner, beyond those encountered at the level of propositional logic.

∗This paper is an abridged version of a paper titled 'Shortening QBF Proofs with Dependency Schemes' that won the Best Paper Award at the SAT 2017 conference.

Arguably, the biggest challenge concerns the allowable order of variable assignments. In traditional QCDCL, the freedom to assign variables is limited according to a linear order imposed by the quantifier prefix. Whereas decision variables must be chosen carefully to ensure sound results, coercing the order of assignment to respect the prefix is frequently needlessly restrictive [Lonsing, 2012]. Moreover, limiting the choice adversely affects the impact of decision heuristics. In contrast, such heuristics play a major role in SAT solving [Silva, 1999; Shacham and Zarpas, 2003; Liang et al., 2015; Moskewicz et al., 2001], where variables may be assigned in an arbitrary order.

Dependency awareness, as implemented in the solver DepQBF [Lonsing and Biere, 2010], is a QBF-specific paradigm that attempts to maximise the impact of decision heuristics. By computing a dependency scheme before the search process begins, the linear order of the prefix is effectively supplanted by a partial order that better approximates the variable dependencies of the instance, granting the solver greater freedom regarding variable assignments. Use of the scheme is static; dependencies are computed only once and do not change during the search. Despite the additional computational cost incurred, empirical results demonstrate improved solving on many benchmark instances [Lonsing, 2012].

Dependency schemes themselves are tractable algorithms that identify dependency information by appeal to the syntactic form of an instance. From the plethora of schemes that have been proposed in the literature, two have emerged as principal objects of study. The standard dependency scheme (Dstd [Samer and Szeider, 2009]), a variant of which is used by DepQBF, was originally proposed in the context of backdoor sets. This scheme uses sequences of clauses connected by common existential variables to determine a dependency relation between the variables of an instance. The reflexive resolution path dependency scheme (Drrs [Slivovsky and Szeider, 2016]) utilises the notion of a resolution path, a more refined type of connection introduced in [Van Gelder, 2011].

A solid theoretical model for dependency awareness was only recently proposed in the form of the calculus Q(D)-Res [Slivovsky and Szeider, 2016], a parametrisation of Qresolution by the dependency scheme D. Whereas the body of work on Q(D)-Res and related systems has focused on soundness [Slivovsky and Szeider, 2016; Peitl et al., 2016; Beyersdorff and Blinkhorn, 2016], authors of all three papers have cited open problems in proof complexity. Indeed, prior to this paper there were no proof-theoretic results to support any claims concerning the potential of dependency schemes in the practice of QBF solving.

In this work, not only do we provide the first such results, we also demonstrate the potential of dependency schemes to further reduce the size of proofs if they are applied dynamically. We summarise our contributions below.

The first separations for dependency calculi. We use the well-known formulas of Kleine B¨uning et al. [Kleine B¨uning et al., 1995] to prove the first exponential separation for Q(D)-Res. We show that Drrs can identify crucial independencies in these formulas, leading to short proofs in the systemQ(Drrs )-Res. In contrast, we show that Dstd cannot identify any non-trivial independencies, allowing us to lift the exponential lower bound for Q-Res [Kleine B¨uning et al., 1995; Beyersdorff et al., 2015] to Q(Dstd )-Res.

A model of dynamic dependency analysis. We propose the new calculus dyn-Q(D)-Res that models the dynamic application of a dependency scheme in Q-resolution. The system employs a so-called 'reference rule' that allows new axioms, called reference clauses, to be introduced into the proof. The key insight is that the application of an assignment to an instance formula may allow the dependency scheme to unlock new independencies. As such, the reference rule alludes to an explicit refutation of the formula under an appropriate restriction, and is analogous to the recomputation of dependencies at an arbitrary point of the QCDCL procedure. We prove that dyn-Q(D)-Res is sound whenever the dependency scheme D is fully exhibited.

Separation of static and dynamic systems. Our final contribution demonstrates that the dynamic application of dependency schemes can shorten Q-resolution proofs even further, yielding an exponential improvement over the static approach. Using a modification of the aforementioned formulas from [Kleine B¨uning et al., 1995], we prove that dyn-Q(Drrs )-Res is exponentially stronger than Q(Drrs )-Res.

2 Preliminaries

Quantified Boolean formulas. In this paper, we consider quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF), typically denoted Φ = Q · φ. A PCNF over Boolean variables z1, . . . , zn consists of a quantifier prefix Q = Q1z1 · · ·Qnzn, Qi ∈ {∃, ∀} for i ∈ [n], in which all variables are quantified either existentially or universally, and a propositional conjunctive normal form (CNF) formula φ called the matrix. The prefix Q imposes a linear ordering <Φ on the variables of Φ, such that zi <Φ zj holds whenever i < j, in which case we say that zj is right of zi.

A literal is a variable or its negation, a clause is a disjunction of literals, and a CNF is a conjunction of clauses. Throughout, we refer to a clause as a set of literals and to a CNF as a set of clauses. We typically write x for existential variables, u for universals, and z for either. For a literal l, we write var(l) = z iff l = z or l = ¬z, for a clause C we write vars(C) = {var(l) | l ∈ C}, and for a PCNF Φ we write vars(Φ) for the variables in the prefix of Φ.

A (partial) assignment δ to the variables of Φ is represented as a set of literals, typically denoted {l1, . . . , lk}, where literal z (resp. ¬z) represents the assignment z ↦→ 1 (resp. z ↦→ 0). The restriction of Φ by δ, denoted Φ[δ], is obtained by removing from φ any clause containing a literal in δ, and removing the negated literals ¬l1, . . . , ¬lk from the remaining clauses, while the variables of δ and their associated quantifiers are removed from the prefix Q.

QBF resolution. Resolution is a well-studied refutational proof system for propositional CNF formulas with a single inference rule: the resolvent C1 ∪ C2 may be derived from clauses C1 ∪ {x} and C2 ∪ {¬x} (variable x is the pivot). Resolution is refutationally sound and complete: that is, the empty clause can be derived from a CNF iff it is unsatisfiable.

There exist a host of resolution-based QBF proof systems - see [Beyersdorff et al., 2015] for a detailed account. Qresolution (Q-Res) introduced in [Kleine B¨uning et al., 1995] is the standard refutational calculus for PCNF. In addition to resolution over existential pivots, the calculus has a universal reduction rule which allows a clause C to be derived from C ∪ {l}, provided var(l) is a universal variable right of all existentials in C. Tautologies are explicitly forbidden; one may not derive a clause containing both z and ¬z.

For a QBF resolution system P, a P derivation of a clause C from a PCNF Φ is a sequence C1, . . . ,Cm of clauses in which C = Cm, and each clause is either an axiom or is derived from previous clauses in the sequence using an inference rule. A refutation of Φ is a derivation of the empty clause from Φ. P is complete iff every false PCNF has a P refutation, and sound iff no true PCNF has a refutation.

A QBF proof system P p-simulates another Q iff each Q refutation can be transformed in polynomial time into a P refutation of the same formula [Cook and Reckhow, 1979].

QBF models. Let Φ = Q1z1 · · ·Qnzn · φ be a PCNF over existential variables V∃ and universal variables V∀. A model f for Φ is a mapping from total assignments to V∀ to total assignments to V∃ that satisfies two conditions: (a) whenever α and α′ agree on all universals left of a variable zi, then f(α) and f(α′ ) agree on all existential variables left of (and including) zi; (b) for each α in the domain of f, α ∪ f(α) satisfies every clause C ∈ φ (that is, C ∩ (α ∪ f(α)) ̸= ∅). A PCNF is true iff it has a model, otherwise it is false.

Axiom rule: axiom(φ)

• C is a non-tautological clause in φ.
• literal l is universal.
• (var(l), x) /∈ D(Φ) holds for each existential variable x in vars(C).
• variable x is existential.
• x ∈ C1 and ¬x ∈ C2.
• the resolvent is nontautological.

Reduction rule: red(C, l)

Resolution rule: res(C1, C2, x)

Figure 1: The rules of Q(D)-Res . D is a dependency scheme and Φ = Q · φ is a PCNF.

3 Static Dependencies in Q-Resolution

For the duration of this work, we deal only with the (in)dependence of existential variables on universal variables. For an arbitrary PCNF Φ, the trivial dependency relation captures the linear order of the quantifier prefix of Φ, and is given by Dtrv (Φ) = {(u, x) ∈ vars∀(Φ)×vars∃(Φ) | u <Φ x}. Formally, a dependency scheme D is a mapping from the set of all PCNFs that satisfies D(Φ) ⊆ Dtrv (Φ) for each PCNF Φ. The existence of a pair (u, x) ∈ D(Φ) should be interpreted as 'existential x depends on universal u in Φ according to dependency scheme D'. We say that D′ is at least as general as D iff D′ (Φ) ⊆ D(Φ) for each PCNF Φ, and is more general if the inclusion is strict for some PCNF.

We give definitions of the standard (Dstd ) and reflexive resolution path (Drrs ) dependency schemes below.

Definition 1 [Samer and Szeider, 2009] Let Φ = Q · φ be a PCNF. The pair (u, x) ∈ Dtrv (Φ) is in Dstd (Φ) iff there exists a sequence of clauses C1, . . . ,Cn ∈ φ with u ∈ vars(C1), x ∈ vars(Cn), such that, for each i ∈ [n - 1], vars(Ci) ∩ vars(Ci+1) contains an existential variable right of u.

Definition 2 [Slivovsky and Szeider, 2016] Let Φ = Q · φ be a PCNF. The pair (u, x) ∈ Dtrv (Φ) is in Drrs (Φ) iff there is a sequence of clauses C1, . . . , Cn ∈ φ and a sequence of existential literals l1, . . . , ln-1 for which the following four conditions hold: (a) u ∈ C1 and ¬u ∈ Cn; (b) x = var(li), for some i ∈ [n - 1]; (c) u <Φ var(li), li ∈ Ci and ¬li ∈ Ci+1, for each i ∈ [n - 1]; (d) var(li) ̸= var(li+1) for each i ∈ [n - 2].

The theoretical model for the use of dependency schemes in dependency-aware solving is captured by the calculus Q(D)-Res [Slivovsky and Szeider, 2016], shown in Fig. 1.

Soundness of Q(D)-Res is not guaranteed, and hinges on the choice of the dependency scheme D. It is known that the concept of full exhibition, which imposes a natural condition on D, is sufficient to prove soundness in Q(D)-Res [Slivovsky, 2015]. Following [Beyersdorff and Blinkhorn, 2016], we say that a model f exhibits the independence of x on u iff, for each α in the domain of f, the assignment to x in f(α) remains unchanged when the assignment to u in α is flipped.

Definition 3 [Slivovsky, 2015; Beyersdorff and Blinkhorn, 2016] A model f for a PCNF Φ is a Dmodel iff, for each (u, x) ∈ Dtrv (Φ) \ D(Φ), f exhibits the independence of x on u. A dependency scheme D is fully exhibited iff each true PCNF has a D-model.

In the remainder of this section, we prove that Q(Drrs )-Res is exponentially stronger than Q(Dstd )-Res. Given that Q(Dstd )-Res trivially p-simulates Q-Res, we thereby separate Q(Drrs )-Res and Q-Res, thus answering the question initially posed in [Slivovsky and Szeider, 2016]. The separating formulas are a well-studied family of PCNFs, originally introduced in [Kleine B¨uning et al., 1995]. We recall the definition of this formula family, which is hereafter denoted Ψ(n).

Definition 4 [Kleine B¨uning et al., 1995] The formula family Ψ(n) := Q(n) · ψ(n) has prefixes Q(n) := ∃x1∃y1∀u1 · · · ∃xn∃yn∀un∃t1 · · · ∃tn and matrices ψ(n) consisting of the clauses

We first show that the standard dependency scheme cannot identify any non-trivial independencies for Ψ(n).

The salient consequence of Prop. 1 is that every application of ∀-reduction in a Q(Dstd )-Res derivation from Ψ(n) is also available in Q-Res. As a result, the Q-Res lower bound for Ψ(n) [Kleine B¨uning et al., 1995; Beyersdorff et al., 2015] lifts directly to Q(Dstd )-Res.

Theorem 1 The QBFs Ψ(n) require exponential-size Q(Dstd )-Res refutations.

In contrast, the more general dependency scheme Drrs can identify some crucial non-trivial independencies in Ψ(n).

According to Prop. 2, a Q(Drrs )-Res refutation of Ψ(n) may contain ∀-reduction steps that are disallowed in Q-Res. Such steps permit the construction of O(n)-size Q(Drrs )-Res refutations.

Theorem 2 The formulas Ψ(n) have linear-size Q(Drrs )-Res refutations.

The following result is an immediate consequence of Theorems 1 and 2.

Theorem 3 Q(Drrs )-Res is exponentially stronger than Q(Dstd )-Res.

Reference rule: ref(δ, π)

• δ is a D-assignment for Φ.
• π is a dyn-Q(D)-Res refutation of Φ[δ]
• C is the largest falsified clause of δ.

Figure 2: The reference rule of dyn-Q(D)-Res. D is a dependency scheme and Φ = Q · φ is a PCNF.

4 Modelling Dynamic Dependency Awareness

In this section, we introduce the dynamic dependency calculus dyn-Q(D)-Res and prove that it is exponentially stronger than Q(D)-Res when D is Drrs . We first define a particular kind of assignment to the variables of a PNCF that, in a clear sense, 'respects' the dependency scheme D.

Definition 5 Let D be a dependency scheme and let δ be a partial assignment to the variables of a PCNF Φ. Then δ is a D-assignment for Φ iff, whenever δ assigns an existential variable x, then δ assigns all universal variables in the set {u | (u, x) ∈ D(Φ)}.

We also define the largest falsified clause of an assignment.

Definition 6 Let δ = {l1, . . . , lk} be an assignment. The largest falsified clause of δ is {¬l1, . . . , ¬lk}.

Definition of the calculus. We define dyn-Q(D)-Res as the proof system that has the rules of Q(D)-Res in addition to the reference rule shown in Fig. 2. On an intuitive level, the reference rule is based on the following fact: Given a PCNF Φ and a fully exhibited dependency scheme D, if Φ is false under restriction by a D-assignment δ, then adding the largest falsified clause of δ to the matrix of Φ preserves satisfiability. Therefore, if the calculus is capable of refuting Φ[δ], it should be able to introduce the largest falsified clause of δ.

We refer to a clause derived by application of the reference rule as a reference clause. As stated in the rule itself, a reference clause may only be introduced if an explicit refutation π of Φ[δ] can be given. This feature allows the size of a dyn-Q(D)-Res derivation to be suitably defined. We refer to π as a referenced refutation.

The reference degree of a dyn-Q(D)-Res derivation is 0 iff it does not contain any reference clauses (i.e. it is a Q(D)-Res derivation). For all other derivations π, the reference degree is d+1, where d is the largest reference degree of a refutation referenced from π.

The size of a dyn-Q(D)-Res derivation π of reference degree 0 is the number of clauses in the proof. The size of a derivation π with non-zero reference degree is a + b, where a is the number of clauses in π and b is the sum of the sizes of refutations referenced from π.

Similarly as for static systems, one can prove that full exhibition of D is sufficient for soundness in dyn-Q(D)-Res. The task is essentially reduced to proving that the reference clauses derived from a true PCNF are satisfied by a D-model.

Theorem 4 The calculus dyn-Q(D)-Res is sound if D is fully exhibited.

Since Drrs is fully exhibited [Beyersdorff and Blinkhorn, 2016] and Drrs is at least as general as Dstd , it follows that dyn-Q(Dstd )-Res and dyn-Q(Drrs )-Res are both sound.

To show the separation of dyn-Q(Drrs )-Res and Q(Drrs )-Res, we introduce the formula family Ξ(n), a modification of Ψ(n) which employs the following operation.

Definition 7 Let C be a clause and let φ be a CNF matrix. The clause-matrix product C ⊗ φ is the CNF matrix with clauses {C ∪C ′ | C ′ ∈ φ}.

Definition 8 Let Ψ(n) := Q(n) · ψ(n) be the formulas of Kleine B¨uning et al. (as in Def. 4). The formula family Ξ(n) has prefixes ∃aQ(n)∃b and matrices

To prove the lower bound for the static calculus, one first shows that Drrs (Ξ(n)) = Dtrv (Ξ(n)), from which it follows that any Q(Drrs )-Res refutation of Ξ(n) is also a Q-Res refutation. Then one shows that any Q-Res refutation of Ξ(n) contains an embedded refutation of Ψ(n), which has exponential size [Kleine B¨uning et al., 1995; Beyersdorff et al., 2015].

Theorem 5 The QBFs Ξ(n) require exponential-size Q(Drrs )-Res refutations.

The upper bound argument makes use of the construction of short refutations from the proof of Theorem 2. By referencing those refutations, dyn-Q(Drrs )-Res admits simple O(n)-size refutations of Ξ(n).

Theorem 6 The formulas Ξ(n) have linear-size dyn-Q(Drrs )-Res refutations.

Our final result is immediate from Theorems 5 and 6.

Theorem 7 The calculus dyn-Q(Drrs )-Res is exponentially stronger than Q(Drrs )-Res.

5 Conclusions

We demonstrated that the use of dependency schemes in Qresolution can yield exponentially shorter proofs, and thereby provided strong theoretical evidence supporting the notion that dependency schemes can be utilised for improved solving. We also demonstrated that the dynamic use of schemes has further potential, beyond that of the static approach in existing implementations.

We emphasize that, at the present time, there is no implementation for Drrs , and that DepQBF uses (a refinement of) Dstd . Since we do not separate Q-Res and Q(Dstd )-Res, our theoretical results are not exactly in line with experimental results. We believe, however, that our results should be viewed as sound motivation for further research into (dynamic) dependency-aware solving.

Finally, we suggest strongly that the results in this paper will lift to further QBF calculi, and most notably to expansion-based systems. We therefore highlight the potential for dependency schemes in expansion solving, and endorse the move in this direction mooted at the conclusion of [Janota et al., 2016].