Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The logic of dependency quantified Boolean formulas (DQBF) [23] generalises the notion of quantified Boolean formulas (QBF) that allow Boolean quantifiers over a propositional problem. DQBF is a relaxation of QBF in that the quantifier order is no longer necessarily linear and the dependencies of the quantifiers are completely specified. This is achieved using Henkin quantifiers [16], usually put into a Skolem form. DQBF is \(\mathsf {NEXPTIME}\)-complete [1], compared to the \(\mathsf {PSPACE}\)-completeness of QBF [28]. Thus, unless the classes are equal, many problems that are difficult to express in QBF can be succinctly represented in DQBF.

Recent developments in QBF proof complexity [5–11, 17–19, 27] have increased our theoretical understanding of QBF proof systems and proof systems in general and have shown that there is an intrinsic link between proof complexity and SAT-, QBF-, and DQBF-solving. Lower bounds in resolution-based proof systems give lower bounds to CDCL-style algorithms. In propositional logic there is only one resolution system (although many subsystems have been studied [24, 29]), but in QBF, resolution can be adapted in different ways to get sound and complete calculi of varying strengths [7, 15, 19, 30].

The first and best-studied QBF resolution system is Q-Res introduced in [21]. For Q-Res there are two main enhanced versions: QU-Res [30], which allows resolution on universal variables, and LD-Q-Res [15], which introduces a process of merging positive and negative universal literals under certain conditions. These two concepts were combined into a single calculus LQU \(^+\)-Res [5].

While these calculi model CDCL solving, another group of resolution systems were developed with the goal to express ideas from expansion solving. The first and most basic of these systems is \(\forall \textsf {Exp+Res}\) [19], which also uses resolution, but is conceptually very different from Q-Res. In [7] two further proof systems IR-calc and IRM-calc are introduced, which unify the CDCL- and expansion-based approaches in the sense that IR-calc simulates both Q-Res and \(\forall \textsf {Exp+Res}\). The system IRM-calc enhances IR-calc and additionally simulates LD-Q-Res. The relative strength of these QBF resolution systems is illustrated in Fig. 1.

Fig. 1.
figure 1

The simulation order of QBF resolution systems [8] and soundness/completeness of their lifted DQBF versions (Color figure online)

Full size image

The aim of this paper is to clarify which of these QBF resolution systems can be lifted to DQBF. This is motivated both by the theoretical quest to understand which QBF resolution paradigms are robust enough to work in the more powerful DQBF setting, as well as from the practical perspective, where recent advances in DQBF solving [12–14, 31] prompt the question of how to model and analyse these solvers proof-theoretically.

Our starting point is the work of Balabanov, Chiang, and Jiang [3], who show that Q-Res can be naturally adapted to a sound calculus for DQBF, but they show it is not strong enough and lacks completeness. Using an idea from [5] we extend their result to QU-Res, thus showing that the lifted version of this system to DQBF is not complete either. We present an example showing that the lifted version of LD-Q-Res is not sound, and this transfers to the DQBF analogues of the stronger systems LQU \(^+\)-Res and IRM-calc.

While this rules out most of the existing QBF resolution calculi already—and in fact all CDCL-based systems (cf. Fig. 1)—we show that IR-calc, lifted in a natural way to a DQBF calculus D-IR-calc, is indeed sound and complete for DQBF; and this holds as well for the lifted version of the weaker expansion system \(\forall \textsf {Exp+Res}\).

Conceptually, our soundness and completeness arguments use the known correspondence of QBF and DQBF to first-order logic [25], and in particular to the fragment EPR, also known as the Bernays-Schönfinkel class, the universal fragment of first-order logic without function symbols of non-zero arity. Similarly to DQBF, EPR is \(\mathsf {NEXPTIME}\)-complete [22]. In addition to providing soundness and completeness this explains the semantics of both IR-calc and D-IR-calc and identifies these systems as special cases of first-order resolution.

2 Preliminaries

A literal is a Boolean variable or its negation. If l is a literal, \(\lnot l\) denotes the complementary literal, i.e., \(\lnot \lnot x=x\). A clause is a set of literals understood as their disjunction. The empty clause is denoted by \(\bot \), which is semantically equivalent to false. A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses. For a literal \(l=x\) or \(l=\lnot x\), we write \({{\mathrm{\text {var}}}}(l)\) for x and extend this notation to \({{\mathrm{\text {var}}}}(C)\) for a clause C.

A Dependency Quantified Boolean Formula (DQBF) \(\phi \) in prenex Skolem form consists of a quantifier prefix \(\varPi \) and a propositional matrix \(\psi \). QBF \(\phi \) can also be written as \(\varPi \cdot \psi \). Here we mainly study DQBFs where \(\psi \) is in CNF. The propositional variables of \(\psi \) are partitioned into sets Y and X. We define Y as the set of universal variables and X the set of existential variables. For every \( y\in Y\), \(\varPi \) contains the quantifier \(\forall y\). For every \(x\in X\) there is a predefined subset \(Y_x\subseteq Y\) and \(\varPi \) contains the quantifier \(\exists x(Y_x)\).

The semantics of DQBF is defined in terms of Skolem functions. A Skolem function \(f_x: \{0,1\}^{Y_x} \rightarrow \{0,1\}\) describes the evaluation of an existential variable x under the possible assignments to its dependencies \(Y_x\). Given a set F of Skolem functions, where \(F=\left\{ {f_x} \;|\; {x\in X}\right\} \) for all the existential variables and an assignment \(\alpha : Y \rightarrow \{0,1\}\) for the universal variables, the extension of \(\alpha \) by F is defined as for \(x\in X\) and \(\alpha _F(y) = \alpha (y)\) for \(y \in Y\). A DQBF \(\phi \) is true if there exist Skolem functions \(F=\left\{ {f_x} \;|\; {x\in X}\right\} \) for the existential variables such that for every assignment \(\alpha : Y \rightarrow \{0,1\}\) to the universal variables the matrix \(\psi \) propositionally evaluates to 1 under the extension \(\alpha _F\) of \(\alpha \) by F.

In QBF, the quantifier prefix is a sequence of standard quantifiers of the form \(\exists x\) and \(\forall y\). To see that this is a special case of DQBF, we use the sequence from left to right to assign to every variable in the prefix a unique index \({{\mathrm{\text {ind}}}}:X\cup Y\rightarrow \mathbb {N}\), and make every existential variable x depend on all the preceding universal variables by setting \(Y_x=\{y\in Y\mid {{\mathrm{\text {ind}}}}(y)<{{\mathrm{\text {ind}}}}(x)\}\).

We now give a brief overview of the main existing resolution-based calculi for QBF. We start by describing the proof systems modelling CDCL-based QBF solving; their rules are summarized in Fig. 2. The most basic and important system is Q-resolution ( Q-Res ) by Kleine Büning et al. [21]. It is a resolution-like calculus that operates on QBFs in prenex form with CNF matrix. In addition to the axioms, Q-Res comprises the resolution rule S\(\exists \)R and universal reduction \(\forall \)-Red (cf. Fig. 2).

Long-distance resolution ( LD-Q-Res ) appears originally in the work of Zhang and Malik [32] and was formalized into a calculus by Balabanov and Jiang [4]. It merges complementary literals of a universal variable u into the special literal \(u^*\). These special literals prohibit certain resolution steps. In particular, different literals of a universal variable u may be merged only if \({{\mathrm{\text {ind}}}}(x)<{{\mathrm{\text {ind}}}}(u)\), where x is the resolved variable. LD-Q-Res uses the rules L\(\exists \)R, \(\forall \)-Red and \(\forall \)-Red\(^*\).

QU-resolution ( QU-Res ) [30] removes the restriction from Q-Res that the resolved variable must be an existential variable and allows resolution of universal variables. The rules of QU-Res are S\(\exists \)R, S\(\forall \)R and \(\forall \)-Red. \({{\textsf {\textit{LQU}}}}^+{{\textsf {\textit{-Res}}}}\) [5] extends LD-Q-Res by allowing short and long distance resolved literals to be universal; however, the resolved literal is never a merged literal \(z^*\). LQU \(^+\)-Res uses the rules L\(\exists \)R, L\(\forall \)R, \(\forall \)-Red and \(\forall \)-Red\(^*\).

Fig. 2.
figure 2

The rules of CDCL-based proof systems

Full size image

The second type of calculi models expansion-based QBF solving. These calculi are based on instantiation of universal variables: \(\forall \textsf {Exp+Res}\)  [20], IR-calc, and IRM-calc  [7]. All these calculi operate on clauses that comprise only existential variables from the original QBF, which are additionally annotated by a substitution to some universal variables, e.g. \(\lnot x^{0/u_1 1/u_2}\). For any annotated literal \(l^\sigma \), the substitution \(\sigma \) must not make assignments to variables at a higher quantification index than that of l, i.e., if \(u\in {{\mathrm{\mathsf{dom}}}}(\sigma )\), then u is universal and \({{\mathrm{\text {ind}}}}(u)<{{\mathrm{\text {ind}}}}(l)\).

To preserve this invariant we use the following definition. Fix a DQBF \(\varPi \cdot \psi \). Let \(\tau \) be a partial assignment of the universal variables Y to \(\{0,1\}\) and let x be an existential variable. \({{\mathrm{\mathsf{restrict}}}}_x(\tau )\) is the assignment where \({{\mathrm{\mathsf{dom}}}}({{\mathrm{\mathsf{restrict}}}}_x(\tau ))= {{\mathrm{\mathsf{dom}}}}(\tau )\cap Y_x\) and \({{\mathrm{\mathsf{restrict}}}}_x(\tau )(u)=\tau (u)\).

The simplest of the instantiation-based calculi we consider is \(\forall \textsf {Exp+Res}\) from [19] (cf. also [7, 8]). The system IR-calc extends \(\forall \textsf {Exp+Res}\) by enabling partial assignments in annotations. To do so, we utilize the auxiliary operation of instantiation. We define \({{\mathrm{\textsf {inst}}}}_\tau (C)\) to be the clause containing all the literals \(l^{{{\mathrm{\mathsf{restrict}}}}_{{{\mathrm{\text {var}}}}(l)}(\sigma )}\), where \(l^\xi \in C\) and \({{\mathrm{\mathsf{dom}}}}(\sigma )={{\mathrm{\mathsf{dom}}}}(\xi )\cup {{\mathrm{\mathsf{dom}}}}(\tau )\) and \(\sigma (u)=\xi (u)\) if \(u\in {{\mathrm{\mathsf{dom}}}}(\xi ) \) and \(\sigma (u)=\tau (u)\) otherwise.

Fig. 3.
figure 3

The rules of IR-calc [7] and of D-IR-calc (Sect. 4)

Full size image

The calculus IRM-calc from [7] further extends IR-calc by enabling annotations containing \(*\), similarly as in LD-Q-Res.

3 Problems with Lifting QBF Calculi to DQBF

There is no unique method for lifting calculi from QBF to DQBF. However, we can consider ‘natural’ generalisations of these calculi, where we interpret index conditions as dependency conditions. This means that when a proof system requires for an existential variable x and a universal variable y with \({{\mathrm{\text {ind}}}}(y)<{{\mathrm{\text {ind}}}}(x)\), this should be interpreted as \(y\in Y_x\). Analogously \({{\mathrm{\text {ind}}}}(x)<{{\mathrm{\text {ind}}}}(y)\) should be interpreted as \(y\notin Y_x\). This approach was followed when taking Q-Resolution to D-Q-Resolution in Theorem 7 of [3]. Balabanov et al. showed there that D-Q-Resolution is not complete for DQBF using some specific formula. This formula is easily shown to be false, but no steps are possible in D-Q-Resolution, hence D-Q-Resolution is not complete [3]. Consider now the following modification of that formula where the universal variables are doubled:

$$\begin{aligned}&\qquad \qquad \quad \forall x_1 \forall x_1' \forall x_2 \forall x_2' \exists y_1(x_1, x_1') \exists y_2(x_2, x_2')\\&\nonumber \begin{array}{lll} \{y_1, y_2, x_1, x_1'\}&{}&{}\{\lnot y_1, \lnot y_2, x_1, x_1'\}\\ \{y_1, y_2, \lnot x_1, \lnot x_1', \lnot x_2, \lnot x_2'\}&{} &{}\{\lnot y_1, \lnot y_2, \lnot x_1, \lnot x_1', \lnot x_2, \lnot x_2'\} \\ \{y_1, \lnot y_2, \lnot x_1, \lnot x_1', x_2, x_2'\}&{} &{}\{ \lnot y_1, y_2, \lnot x_1, \lnot x_1', x_2, x_2'\}. \end{array} \end{aligned}$$
(1)

The falsity of (1) follows from the fact that its hypothetical Skolem model would immediately yield a Skolem model for the original formula using assignments with \(x_1=x_1'\), \(x_2=x_2'\). But there is no such model because the original formula is false. However, since we have doubled the universal literals we cannot perform any generalised QU-Res steps to begin a refutation. This technique of doubling literals was first used in [5].

Now we look at another portion of the calculi from Fig. 1, namely the calculi that utilise merging. As a specific example we consider LD-Q-Res and show that it is not sound when lifted to DQBF in the natural way.

To do this we look at the condition of (L\(\exists \)R) given in Fig. 2. Here instead of requiring \({{\mathrm{\text {ind}}}}(x)<{{\mathrm{\text {ind}}}}(u)\) as a condition for u becoming merged, we require \(u\notin Y_x\). This is unsound as we show by the following DQBF:

figure a

Its truth is witnessed by the Skolem functions \(x(u)=u\), \(y(v)=\lnot v\), and \(z(u,v)=(u\wedge v) \vee (\lnot u \wedge \lnot v)\). However, the lifted version of LD-Q-Res admits a refutation:

figure b

This shows that LD-Q-Res is unsound for DQBF. Likewise, since IRM-calc, LQU -Res and LQU \(^+\)-Res step-wise simulate LD-Q-Res, this proof would also be available, showing that these are all unsound calculi in the DQBF setting.

4 A Sound and Complete Proof System for DQBF

In this section we introduce the D-IR-calc refutation system and prove its soundness and completeness for DQBF. The calculus takes inspiration from IR-calc, a system for QBF [7], which in turn is inspired by first-order translations of QBF. One such translation is to the EPR fragment, i.e., the universal fragment of first-order logic without function symbols of non-zero arity (this means we only allow constants). We broaden this translation to DQBF and then bring this back down to D-IR-calc in a similar way as in IR-calc.

We adapt annotated literals \(l^\tau \) to DQBF, such that l is an existential literal and \(\tau \) is an annotation which is a partial assignment to universal variables in \(Y_x\). In QBF, \(Y_x\) contains all universal variables with an index lower than x, and this is exactly the maximal range of the potential annotation to x literals. Thus our definition of annotated literals generalises those used in IR-calc.

The definitions of \({{\mathrm{\mathsf{restrict}}}}\) and \({{\mathrm{\textsf {inst}}}}\) were defined for QBF, but with dependency already in mind. With these definitions at hand we can now define the new calculus D-IR-calc. Its rules are exactly the same as the ones for IR-calc stated in Fig. 3, but applied to DQBF.

Before analysing D-IR-calc further we present the translation of DQBF into EPR. We use an adaptation of the translation described for QBF [25], which becomes straightforward in the light of the DQBF semantics based on Skolem functions. The key observation is that for the intended two valued Boolean domain the Skolem functions can be represented by predicates.

To translate a DQBF \(\varPi \cdot \psi \) we introduce on the first-order side (1) a predicate symbol p of arity one and two constant symbols 0 and 1 to describe the Boolean domain, (2) for every existential variable \(x \in X\) a predicate symbol x of arity \(|Y_x|\), and (3) for every universal variable \(y \in Y\) a first-order variable \({y}\).

Now we can define a translation mapping \(t_\varPi \). It translates each occurrence of an existential variable x with dependencies \(Y_x = \{y_1,\ldots ,y_k\}\) to the atom \(t_\varPi (x) = x({y_1},\ldots ,{y_k})\) (we assume an arbitrary but fixed order on the dependencies which dictates their placement as arguments) and each occurrence of a universal variable y to the atom \(t_\varPi (y) = p({y})\). The mapping is then homomorphically extended to formulas: \(t_\varPi (\lnot \psi ) = \lnot t_\varPi (\psi )\), \(t_\varPi ( \psi _1 \vee \psi _2) = t_\varPi (\psi _1) \vee t_\varPi (\psi _2)\), and \(t_\varPi ( \psi _1 \wedge \psi _2) = t_\varPi (\psi _1) \wedge t_\varPi (\psi _2)\). This means a CNF matrix \(\psi \) is mapped to a corresponding first-order CNF \(t_\varPi (\psi )\). As customary, the first-order variables of \(t_\varPi (\psi )\) are assumed to be implicitly universally quantified at the top level.

Lemma 1

A DQBF \(\varPi \cdot \psi \) is true if and only if \(t_\varPi (\psi ) \wedge p(1) \wedge \lnot p(0)\) is satisfiable.

Proof

(Idea). When the DQBF \(\varPi \cdot \psi \) is true, this is witnessed by the existence of Skolem functions \(F=\left\{ {f_x} \;|\; {x\in X}\right\} \). On the other hand, if \(t_\varPi (\psi ) \wedge p(1) \wedge \lnot p(0)\) is satisfiable then we can by Herbrand’s theorem assume it has a Herbrand model H over the base \(\{0,1\}\). We can naturally translate between one and the other by setting \(f_x({{\varvec{v}}}) = 1 \text { iff } x({{\varvec{v}}}) \in H\) for every \(x \in X\) and \({{\varvec{v}}} \in \{0,1\}^{|Y_x|}\). The lemma then follows by structural induction over \(\psi \).    \(\square \)

For the purpose of analysing D-IR-calc, the mapping \(t_\varPi \) is further extended to annotated literals: \(t_\varPi (x^\tau ) = t_\varPi (x)\tau \) for an existential variable x. Here we continue to slightly abuse notation and treat \(\tau \), an annotation in the propositional context, as a first-order substitution over the corresponding translated variables in the first-order context (recall point (3) above).

We aim to show soundness and completeness of D-IR-calc by relating it via the above translation to a first-order resolution calculus FO-res. This calculus consists of (1) a lazy grounding rule: given a clause C and a substitution \(\sigma \) derive the instance \(C\sigma \), and (2) the resolution rule: given two clauses \(C \cup \{l\}\) and \(D \cup \{\lnot l\}\), where l is a first-order literal, derive \(C \cup D\). Note that similarly to propositional clauses, we understand first-order clauses as sets of literals. Thus we do not need any explicit factoring rule. Also note that we require the resolved literals of the two premises of the resolution rule to be equal (up to the polarity). Standard first-order resolution, which involves unification of the resolved literals, can be simulated in FO-res by combining the instantiation and the resolution rule. It is clear that FO-res is sound and complete for first-order logic.

Our argument for the soundness of D-IR-calc is now the following. Given \(\pi = (L_1, L_2, \dots , L_\ell )\), a D-IR-calc derivation of the empty clause \(L_\ell = \bot \) from DQBF \(\varPi \cdot \psi \), we show by induction that \(t_\varPi (L_n)\) is derivable from \(\varPsi = t_\varPi (\psi ) \wedge p(1) \wedge \lnot p(0)\) by FO-res for every \(n\le \ell \). Because \(t_\varPi (\bot )=\bot \) is unsatisfiable, so must \(\varPsi \) be, by soundness of FO-res and therefore \(\varPi \cdot \psi \) is false by Lemma 1.

We need to consider the three cases by which a clause is derived in D-IR-calc. First, it is easy to verify that D-IR-calc instantiation by an annotation \(\tau \) corresponds to FO-res instantiation by \(\tau \) as a substitution, i.e., \(t_\varPi ({{\mathrm{\textsf {inst}}}}_\tau (C)) = t_\varPi (C)\tau .\) Also the D-IR-calc and FO-res resolution rules correspond one to one in an obvious way. Thus the most interesting case concerns the Axiom rule.

Intuitively, the Axiom rule of D-IR-calc removes universal variables from a clause while recording their past presence (and polarity) within the applied annotation \(\tau \). We simulate this step in FO-res by first instantiating the translated clause by \(\tau \) and then resolving the obtained clause with the unit p(1) and/or \(\lnot p(0)\). Here is an example for a DQBF prefix \(\varPi = \forall u\, \forall v\, \forall w\, \exists x(u,v)\, \exists y(v,w)\):

figure c

Theorem 2

D-IR-calc is sound.

We now show completeness. Let \(\varPi \cdot \psi \) be a false DQBF and let us consider \(\mathcal {G}(t_\varPi (\psi ))\), the set of all ground instances of clauses in \(t_\varPi (\psi )\). Here, by a ground instance of a clause C we mean the clause \(C\sigma \) for some substitution \(\sigma :{{\mathrm{\text {var}}}}(C)\rightarrow \{0,1\}\). By the combination of Lemma 1 and Herbrand’s theorem, \(\mathcal {G}(t_\varPi (\psi )) \wedge p(1) \wedge \lnot p(0)\) is unsatisfiable and thus it has a FO-res refutation. Moreover, by completeness of ordered resolution [2], we can assume that (1) the refutation does not contain clauses subsumed by p(1) or \(\lnot p(0)\), and (2) any clause containing the predicate p is resolved on a literal containing p. From this it is easy to see that any leaf in the refutation gives rise (in zero, one or two resolution steps with p(1) or \(\lnot p(0)\)) to a clause \(D = t_\varPi (C)\) where C can be obtained by D-IR-calc Axiom from a \(C_0 \in \psi \). The rest of the refutation consists of FO-res resolution steps which can be simulated by D-IR-calc. Thus we obtain the following.

Theorem 3

D-IR-calc is refutationally complete for DQBF.

Although one can lift the above argument with ordered resolution to show that the set \(\left\{ {t_\varPi (C)} \;|\; {C~\text {follows by Axiom from some}~C_0 \in \psi }\right\} \) is unsatisfiable for any false DQBF \(\varPi \cdot \psi \), we have shown how to simulate ground FO-res steps by D-IR-calc. That is because a lifted FO-res derivation may contain instantiation steps which rename variables apart for which a subsequent resolvent cannot be represented in D-IR-calc. An example is the resolvent \(\{{y}({v}) , {z}({v}')\}\) of clauses \(\{{x}({u}) , {y}({v})\}\) and \(\{\lnot {x}({u}) , {z}({v}')\}\) which is obviously stronger than the clause \(\{{y}({v}) , {z}({v})\}\). However, only the latter has a counterpart in D-IR-calc.

We also remark that in a similar way we can also lift to DQBF the QBF calculus \(\forall \textsf {Exp+Res}\) from [19]. It is easily verified that the simulation of \(\forall \textsf {Exp+Res}\) by IR-calc shown in [7] directly transfers from QBF to DQBF. Hence Theorem 2 immediately implies the soundness of \(\forall \textsf {Exp+Res}\) lifted to DQBF. Moreover, because all ground instances are also available in \(\forall \textsf {Exp+Res}\) lifted to DQBF, this system is also complete as can be shown by repeating the argument of Theorem 3.