Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths

Abstract

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any DQBF proof system. We further explore the power of DQBF resolution systems parameterised by dependency schemes and show that our new scheme results in exponentially shorter proofs in comparison to the reflexive resolution path dependency scheme when used in the expansion DQBF system $\mathsf {\forall {Exp{\text{+ }}Res}}$.

On QBFs, we demonstrate that our new scheme is exponentially stronger than the reflexive resolution path dependency scheme when used in Q-resolution, thus resulting in the strongest QBF dependency scheme known to date.

This research was supported by grants from FWF (J-4361), the John Templeton Foundation (grant no. 60842), and the Carl Zeiss Foundation.

1 Introduction

Quantified Boolean formulas (QBF) have been intensively studied in the past decade, both practically and theoretically. On the practical side, there have been huge improvements in QBF solving [30]. These build on the success of SAT solving [36], but also incorporate new ideas genuine to the QBF domain, such as expansion solving [21] and dependency schemes [32]. Due to its PSPACE completeness, QBF solving is relevant to many application domains that cannot be efficiently encoded into SAT [17, 23, 26]. On the theoretical side, there is a substantial body of QBF proof complexity results (e.g. [3, 6, 8,9,10]), which calibrates the strength of solvers while guiding their development.

In QBF solving, a severe technical complication is that variable dependencies stemming from the linear order of quantification¹ must be respected when assigning variables. In contrast, a SAT solver can assign variables in any order, granting complete freedom to decision heuristics, which are crucial for performance. As a remedy, QBF researchers have developed dependency schemes. Dependency schemes try to determine algorithmically which of the variable dependencies are essential, thereby identifying spurious dependencies which can be safely disregarded. The result is greater freedom for decision heuristics.

Practical QBF solving utilises dependency schemes, for example the solvers DepQBF [24] and Qute [27, 28], and experiments show dependency-aware solving is particularly competitive on QBFs with high quantifier complexity [20, 25].

The performance gains are also underlined by theoretical findings. There is a sequence of results [7, 29, 35] that establish how and when dependency schemes are sound to use with a QBF proof system, such as the central QBF resolution systems Q-resolution [22] and long-distance Q-resolution [2]. In [6] it is demonstrated that using the reflexive resolution path dependency scheme (${\mathcal {D}^{\text{ rrs }}}$ [35]) in Q-resolution can exponentially shorten proofs.

While dependency schemes aim to algorithmically determine spurious dependencies, dependency quantified Boolean formulas (DQBF) allow to directly express variable dependencies by specifying, for each existential variable $x$, a dependency set of universal variables on which $x$ depends. This is akin to the use of Henkin quantifiers in first-order logic [18]. Compared to QBFs, DQBFs boost reasoning power and enable further applications (cf. [33] for an overview). The price of succinct encodings is an increase of the complexity of the satisfiability problem from PSPACE (for QBF) to NEXP (for DQBF) [1].

It seems natural that there should be a relationship between dependency schemes and DQBF, and indeed the paper [7] suggests that dependency schemes for QBF should be viewed as truth-preserving mappings from QBF to DQBF.

Now, is there even a need for dependency schemes for DQBF? The answer is yes: also for DQBFs it is possible that the dependency sets contain spurious dependencies, which can be safely eliminated [37]. Indeed, Wimmer et al. [37] showed that several dependency schemes for QBF, including ${\mathcal {D}^{\text{ rrs }}}$, can be lifted to DQBF. They also demonstrate that using dependency schemes for DQBF preprocessing can have a significant positive impact on solving time.

However, in contrast to QBF, there are currently no results on how DQBF dependency schemes can be incorporated into DQBF proof systems, and how this affects their proof-theoretic strength.

This paper contributes to the theory of DQBF dependency schemes on three main fronts.

A. A proof complexity framework for DQBF dependency schemes. We extend the interpretation of QBF dependency schemes proposed in [7] to DQBF. The result is a framework in which a sound DQBF dependency scheme $\mathcal {D}$ can be straightforwardly incorporated into an arbitrary DQBF proof system $\mathsf {P}$, yielding the parametrised system $\mathsf {P}(\mathcal {D})$. More precisely, in our framework a proof of $\varPhi$ in $\mathsf {P}(\mathcal {D})$ is simply a $\mathsf {P}$ proof of $\mathcal {D}(\varPhi )$, where $\mathcal {D}$ is a mapping between DQBFs.

A major benefit of this approach is that the rules of the proof system remain independent of the dependency scheme, which essentially plays the role of a preprocessor. Moreover, soundness of a dependency scheme is characterised by the natural property of full exhibition [4, 34], independently of proofs. This is a welcome feature, since even defining sound parameterisations on the QBF fragment has been fairly non-trivial, e.g. for the long-distance Q-resolution calculus [4, 29].

We also extend the notion of genuine proof size lower bounds [12, 14] to DQBF proof systems. Since DQBF encompasses QBF, proof systems are susceptible to lower bounds from QBF proof complexity. We define a precise condition by which hardness from the QBF fragment is factored out. As such, our framework fosters the first dedicated DQBF proof complexity results.

B. The tautology-free dependency scheme. We define and analyse a new DQBF dependency scheme called the tautology-free dependency scheme (${\mathcal {D}^{\text{ tf }}}$). Our scheme builds on the reflexive resolution path dependency scheme (${\mathcal {D}^{\text{ rrs }}}$) [35], originally defined for QBFs, which prior to this paper was the strongest known DQBF scheme. ${\mathcal {D}^{\text{ tf }}}$ improves on ${\mathcal {D}^{\text{ rrs }}}$ by disallowing certain kinds of tautologies in resolution paths, thereby identifying further spurious dependencies.

We show that ${\mathcal {D}^{\text{ tf }}}$ is fully exhibited, and therefore sound, by reducing its full exhibition to that of ${\mathcal {D}^{\text{ rrs }}}$. For this, we point out that the full exhibition of ${\mathcal {D}^{\text{ rrs }}}$ on DQBF is an immediate consequence of results of Wimmer et al. [37].

C. Exponential separations of (D)QBF proof systems. To demonstrate the strength of our new scheme ${\mathcal {D}^{\text{ tf }}}$, we show that it can exponentially shorten proofs in DQBF proof systems. As a case study, we consider the expansion calculus $\mathsf {\forall {Exp{\text{+ }}Res}}$. The choice of $\mathsf {\forall {Exp{\text{+ }}Res}}$ is motivated by two considerations: (1) it is a natural calculus, whose QBF fragment models expansion solving [21], and (2) other standard QBF resolution systems such as Q-resolution and long-distance Q-resolution do not lift to DQBF [11].

For $\mathsf {\forall {Exp{\text{+ }}Res}}$ parameterised by dependency schemes we show that

$$\begin{aligned} \mathsf {\forall {Exp{\text{+ }}Res}}< \mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})} < \mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})} \end{aligned}$$

(1)

forms a hierarchy of DQBF proof systems of strictly increasing strength.

Since there exist no prior DQBF proof complexity results whatsoever, this entails proving exponential proof-size lower bounds in the first two systems. We obtain these by introducing two new DQBF versions of the equality formulas (originally QBFs [8, 13]). Together with the corresponding upper bounds, this yields the separations in (1). We highlight that these are genuine separations in the precise sense of our DQBF framework, whereby hardness due to the QBF fragment is factored out.

Finally, we show that our new dependency scheme ${\mathcal {D}^{\text{ tf }}}$ is also relevant for QBFs: we prove that Q-resolution parameterised by ${\mathcal {D}^{\text{ tf }}}$ is exponentially stronger than Q-resolution with ${\mathcal {D}^{\text{ rrs }}}$. Thus ${\mathcal {D}^{\text{ tf }}}$ currently constitutes the strongest known dependency scheme for Q-resolution.

Organisation. Section 2 defines DQBF preliminaries. In Sect. 3 we explain dependency schemes. Section 4 details how to parameterise DQBF proof systems by dependency schemes. In Sect. 5 we define our new scheme ${\mathcal {D}^{\text{ tf }}}$ and show its soundness. In Sect. 6 we prove the proof complexity upper and lower bounds needed for the strict hierarchy in (1). Section 7 applies ${\mathcal {D}^{\text{ tf }}}$ to QBF and shows that it is stronger than ${\mathcal {D}^{\text{ rrs }}}$ when used with Q-resolution.

2 Preliminaries

DQBF Syntax. We assume familiarity with the syntax of propositional logic and the notion of Boolean formula (simply formula). A variable is an element $z$ of the countable set $\mathbb {V}$. A literal is a variable $z$ or its negation $\overline{{z}}$. The negation of a literal $a$ is denoted $\overline{{a}}$, where $\overline{{\overline{{z}}}} := z$ for any variable $z$. A clause is a disjunction of literals. A conjunctive normal form formula (CNF) is a conjunction of clauses. The set of variables appearing in a formula $\psi$ is denoted $\text{ vars }({\psi })$. For ease, we often write clauses as sets of literals, and CNFs as sets of clauses. For any clause $C$ and any set of variables $Z$, we define ${C}{\upharpoonright }_{Z} := \{{a\in C}:{\text{ var }({a}) \in Z}\}$.

A dependency quantified Boolean formula (DQBF) is a sentence of the form $\varPsi := {\varPi }\cdot {\psi }$, where $\varPi := \forall u_1 \cdots \forall u_m\exists x_1(S_{x_1}) \cdots \exists x_n(S_{x_n})$ is the quantifier prefix and $\psi$ is a CNF called the matrix. In the quantifier prefix, each existential variable $x_i$ is associated with a dependency set $S_{x_i}$, which is a subset of the universal variables $\{u_1, \dots , u_m\}$. With $\text{ vars }_\forall ({\varPsi })$ and $\text{ vars }_\exists ({\varPsi })$ we denote the universal and existential variable sets of $\varPsi$, and with $\text{ vars }({\varPsi })$ their union. We deal only with closed DQBFs, in which $\text{ vars }({\psi }) \subseteq \text{ vars }({\varPsi })$. We define a relation $\mathsf {deps}({\varPsi })$ on $\text{ vars }_\forall ({\varPsi }) \times \text{ vars }_\exists ({\varPsi })$, where $(u,x) \in \mathsf {deps}({\varPsi })$ if, and only if, $u\in S_x$.

The set of all DQBFs is denoted $\mathsf {DQBF}$. A QBF is a DQBF whose dependency sets are linearly ordered with respect to set inclusion, i.e. $S_{x_1} \subseteq \cdots \subseteq S_{x_n}$. The prefix of a QBF can be written as a linear order in the conventional way. The set of all QBFs is denoted $\mathsf {QBF}$.

DQBF Semantics. An assignment $\alpha$ to a set $Z$ of Boolean variables is a function from $Z$ into the set of Boolean constants $\{0,1\}$. The domain restriction of $\alpha$ to a subset $Z^\prime \subseteq Z$ is written ${\alpha }{\upharpoonright }_{Z^\prime }$. The set of all assignments to $Z$ is denoted $\langle {Z}\rangle$. The restriction of a formula $\psi$ by $\alpha$, denoted ${\psi }[{\alpha }]$, is the result of substituting each variable $z$ in $Z$ by $\alpha (z)$, followed by applying the standard simplifications for Boolean constants, i.e. $\overline{{0}} \mapsto {1}$, $\overline{{1}} \mapsto {0}$, $\phi \vee 0 \mapsto \phi$, $\phi \vee 1 \mapsto 1$, $\phi \wedge 1 \mapsto \phi$, and $\phi \wedge 0 \mapsto 0$. We say that $\alpha$ satisfies $\psi$ when ${\psi }[{\alpha }] = 1$, and falsifies $\psi$ when ${\psi }[{\alpha }] = 0$.

A model for a DQBF $\varPsi := {\varPi }\cdot {\psi }$ is a set of functions $f:= \{{f_x}:{x\in \text{ vars }_\exists ({\varPsi })}\}$, $f_x: \langle {S_x}\rangle \rightarrow \langle {\{x\}}\rangle$, for which, for each $\alpha \in \langle {\text{ vars }_\forall ({\varPsi })}\rangle$, the combined assignment $\alpha \cup \{{f_x({\alpha }{\upharpoonright }_{S_x})}:{x\in \text{ vars }_\exists ({\varPsi })}\}$ satisfies $\psi$. A DQBF is called true when it has a model, otherwise it is called false. When two DQBFs share the same truth value, we write $\varPsi \overset{\text{ tr }}{\equiv }\varPsi ^\prime$.

DQBF Expansion. Universal expansion is a syntactic transformation that removes a universal variable from a DQBF. Let $\varPsi$ be a DQBF, let $u$ be a universal, and let $y_1, \dots , y_k$ be the existentials for which $u\in S_{y_i}$. The expansion of $\varPsi$ by $u$ is obtained by creating two ‘copies’ of $\varPsi$. In the first copy, $u$ is assigned $0$ and each $y_i$ is renamed $y^{\overline{{u}}}_i$. In the second copy, $u$ is assigned $1$ and each $y_i$ is renamed $y^{{u}}_i$. The two copies are then combined, and $u$ is removed completely from the prefix. Formally, $\mathsf {exp}({\varPsi },{u}) := {\varPi ^\prime }\cdot {\psi ^\prime }$, where $\varPi ^\prime$ is obtained from $\varPi$ by removing $\forall u$ and replacing each $\exists y_i(S_{y_i})$ with $\exists y_i^{\overline{{u}}}(S_{y_i} \setminus \{u\}) \, \exists y_i^{{u}}(S_{y_i} \setminus \{u\})$, and

$$\psi ^\prime := {\psi }[{u\mapsto 0, y_1 \mapsto y^{\overline{{u}}}_1, \dots , y_k \mapsto y^{\overline{{u}}}_k}] \wedge {\psi }[{u\mapsto 1, y_1 \mapsto y^{{u}}_1, \dots , y_k \mapsto y^{{u}}_k}]\,.$$

Universal expansion is known to preserve the truth value, i.e. $\varPsi \overset{\text{ tr }}{\equiv }\mathsf {exp}({\varPsi },{u})$. Expansion by a set of universal variables $U$ is defined as the successive expansion by each $u\in U$ (the order is irrelevant), and is denoted $\mathsf {exp}({\varPsi },{U})$. Expansion by the whole set $\text{ vars }_\forall ({\varPsi })$ is denoted $\mathsf {exp}({\varPsi })$, and referred to as the total expansion of $\varPsi$. The superscripts in the renamed existential variables are known as annotations. Annotations grow during successive expansions. In the total expansion, each variable is annotated with a total assignment to its dependency set.

3 DQBF Dependency Schemes and Full Exhibition

In this section, we lift the ‘DQBF-centric’ interpretation of QBF dependency schemes [7] to the DQBF domain, and recall the definition of full exhibition.

How Should We Interpret Variable Dependence? Dependency schemes [32] were originally introduced to identify so-called spurious dependencies: sometimes the order of quantification implies that $z$ depends on $z^\prime$, but forcing $z$ to be independent preserves the truth value. Technically, a dependency scheme $\mathcal {D}$ was defined to map a QBF $\varPhi$ to a set of pairs $(z^\prime , z) \in \text{ vars }({\varPhi }) \times \text{ vars }({\varPhi })$, describing an overapproximation of the dependency structure: $(z^\prime , z) \in \mathcal {D}(\varPhi )$ means that the dependence of $z$ on $z^\prime$ should not be ignored, whereas $(z^\prime , z) \notin \mathcal {D}(\varPhi )$ means that it can be. The definition was tailored to QBF solving, in which variable dependencies for both true and false formulas come into play.

The DQBF-centric interpretation [7] followed somewhat later. There, the goal was a dependency scheme framework tailored to refutational QBF proof systems. Refutational systems work only with false formulas, and this allows a broad refinement: the dependence of universals on existentials can be ignored. As such, it makes sense to consider merely the effect of deleting some universal variables from the existential dependency sets. Thus, a dependency scheme becomes a mapping from $\mathsf {QBF}$ into $\mathsf {DQBF}$.

Likewise, in this work we seek a framework tailored towards refutational proof systems. Hence we advocate the same approach for the whole domain $\mathsf {DQBF}$. A DQBF dependency scheme will be viewed as a mapping to and from $\mathsf {DQBF}$, in which the dependency sets may shrink. The notion of shrinking dependency sets is captured by the relation following.

Definition 1

We define the relation $\le$ on $\mathsf {DQBF}\times \mathsf {DQBF}$ as follows: ${\varPi ^\prime }\cdot {\phi } \, \le \, {\varPi }\cdot {\psi }$ if, and only if, $\phi = \psi$, $\text{ vars }_\exists ({\varPsi ^\prime }) = \text{ vars }_\exists ({\varPsi })$, and the dependency set of each existential in $\varPi ^\prime$ is a subset of that of $\varPi$.

In this paper, we only consider poly-time computable dependency schemes.

Definition 2 (dependency scheme)

A dependency scheme is a polynomial-time computable function $\mathcal {D}: \mathsf {DQBF}\rightarrow \mathsf {DQBF}$ for which $\mathcal {D}(\varPsi ) \le \varPsi$ for all $\varPsi$.

Under this definition, a spurious dependency according to $\mathcal {D}$ is a pair $(u,x)$ such that $u$ is in the dependency set for $x$ in $\varPsi$, but not in $\mathcal {D}(\varPsi )$. A natural property of dependency schemes, identified in [37], is monotonicity.²

Definition 3

(monotone (adapted from [37])). We call a dependency scheme $\mathcal {D}$ monotone when $\varPsi ^\prime \le \varPsi$ implies $\mathcal {D}(\varPsi ^\prime ) \le \mathcal {D}(\varPsi )$, for all $\varPsi$ and $\varPsi ^\prime$.

A fundamental concept in the DQBF-centric framework, which has strong connections to soundness in related proof systems [6], is full exhibition. First used by Slivovsky [34], the name was coined later in [4], describing the fact that there should be a model which ‘fully exhibits’ all spurious dependencies. ‘Full exhibition’ is synonymous with ‘truth-value preserving’.

Definition 4

(full exhibition [4, 34]). A dependency scheme $\mathcal {D}$ is called fully exhibited when $\varPsi \overset{\text{ tr }}{\equiv }\mathcal {D}(\varPsi )$, for all $\varPsi$.

4 Parametrising DQBF Calculi by Dependency Schemes

In this section we show how to incorporate dependency schemes into DQBF proof systems. In the spirit of so-called ‘genuine’ lower bounds [12], we also introduce a notion of genuine DQBF hardness.

Refutational DQBF Proof Systems. We first define what we mean by a DQBF proof system. With $\mathsf {FDQBF}$ we denote the set of false DQBFs. We consider only refutational proof systems, which try to show that a given formula is false. Hence, ‘proof’ and ‘refutation’ can be considered synonymous.

Following [15], a DQBF proof system over an alphabet $\varSigma$ is a polynomial-time computable onto function $\mathsf {P}: \varSigma ^*\rightarrow \mathsf {FDQBF}$. In practice, we do not always want to define a proof system explicitly as a function on a domain of strings. Instead, we define what constitutes a refutation in the proof system $\mathsf {P}$, and then show: (1) Soundness: if $\varPsi$ has a refutation, it is false (the codomain of $\mathsf {P}$ is $\mathsf {FDQBF}$); (2) Completeness: every false DQBF has a refutation ($\mathsf {P}$ is onto); (3) Checkability: refutations can be checked efficiently ($\mathsf {P}$ is polynomial-time computable).

Two concrete examples of DQBF proof systems from the literature are the fundamental expansion-based system $\mathsf {\forall {Exp{\text{+ }}Res}}$ [7], and the more sophisticated instantiation-based system $\mathsf {IR{\text{- }}calc}$ [7].

Incorporating Dependency Schemes. A dependency scheme, interpreted as a DQBF mapping as in Definition 2, can be combined with an arbitrary proof system in a straightforward manner.

Definition 5

($\mathsf {P(\mathcal {D})}$). Let $\mathsf {P}$ be a DQBF proof system and let $\mathcal {D}$ be a dependency scheme. A $\mathsf {P(\mathcal {D})}$ refutation of a DQBF $\varPsi$ is a $\mathsf {P}$ refutation of $\mathcal {D}(\varPsi )$.

The proof system $\mathsf {P(\mathcal {D})}$ essentially utilises the dependency scheme as a preprocessing step, mapping its input $\varPsi$ to the image $\mathcal {D}(\varPsi )$ before proceeding with the refutation. In this way, the application of the dependency scheme $\mathcal {D}$ is separated from the rules of the proof system $\mathsf {P}$, and consequently the definition of $\mathsf {P}$ need not be explicitly modified to incorporate $\mathcal {D}$ (cf. [4, 35]).

Of course, we must ensure that our preprocessing step is correct; we do not want to map a true formula to a false one, which would result in an unsound proof system. Now it becomes clear why full exhibition is central for soundness.

Proposition 6

Given a DQBF proof system $\mathsf {P}$ and a dependency scheme $\mathcal {D}$, $\mathsf {P(\mathcal {D})}$ is sound if, and only if, $\mathcal {D}$ is fully exhibited.

Proof

Suppose that $\mathcal {D}$ is fully exhibited. Let $\pi$ be a $\mathsf {P(\mathcal {D})}$ refutation of a DQBF $\varPsi$. Then $\pi$ is a $\mathsf {P}$ refutation of $\mathcal {D}(\varPsi )$, which is false by the soundness of $\mathsf {P}$. Hence $\varPsi$ is false by the full exhibition of $\mathcal {D}$, so $\mathsf {P(\mathcal {D})}$ is sound.

Suppose now that $\mathcal {D}$ is not fully exhibited. By definition of dependency scheme, for each DQBF $\varPsi$ we have $\varPsi \ge \mathcal {D}(\varPsi )$. It follows that $\mathcal {D}$ preserves falsity, so there must exist a true DQBF $\varPsi$ for which $\mathcal {D}(\varPsi )$ is false. Then there exists a $\mathsf {P}$ refutation of $\mathcal {D}(\varPsi )$ by the completeness of $\mathsf {P}$, so $\mathsf {P(\mathcal {D})}$ is not sound.    $\square$

Note that completeness and checkability of $\mathsf {P}$ are preserved trivially by any dependency scheme, so we can even say that $\mathsf {P(\mathcal {D})}$ is a DQBF proof system if, and only if, $\mathcal {D}$ is fully exhibited. Thus full exhibition characterises exactly the dependency schemes whose incorporation preserves the proof system.

Simulations, Separations and Genuine Lower Bounds. Of course, the rationale for utilising a dependency scheme as a preprocessor lies in the potential for shorter refutations. We first recall the notion of p-simulation from [15]. Let $\mathsf {P}$ and $\mathsf {Q}$ be DQBF proof systems. We say that $\mathsf {P}$ p-simulates $\mathsf {Q}$ (written ${\mathsf {Q}}\le _p{\mathsf {P}}$) when there exists a polynomial-time computable function from $\mathsf {Q}$ refutations to $\mathsf {P}$ refutations that preserves the refuted formula.

Since a p-simulation is computed in polynomial time, the translation from $\mathsf {Q}$ into $\mathsf {P}$ incurs at most a polynomial size blow-up. As such, the conventional approach to proving the non-existence of a p-simulation is to exhibit a family of formulas $\{\varPsi _n\}_{n \in \mathbb {N}}$ that has polynomial-size refutations in $\mathsf {Q}$, while requiring super-polynomial size in $\mathsf {P}$.

Now, it is of course possible that the hard formulas $\{\varPsi _n\}_{n \in \mathbb {N}}$ are QBFs. While this suffices to show that ${\mathsf {Q}}\nleq _p{\mathsf {P}}$, it is not what we want from a study of DQBF proof complexity; it is rather a statement about the QBF fragments of the systems $\mathsf {P}$ and $\mathsf {Q}$. In reality the situation is even more complex. The lower bound may stem from QBF proof complexity even when $\{\varPsi _n\}_{n \in \mathbb {N}}$ are not QBFs. More precisely, there may exist an ‘embedded’ QBF family $\{\varPhi _n\}_{n \in \mathbb {N}}$ which is already hard for $\mathsf {P}$, where ‘embedded’ means $\varPhi _n \le \varPsi _n$. Under the reasonable assumption that decreasing dependency sets cannot increase proof size,³ any DQBF family in which $\{\varPhi _n\}_{n \in \mathbb {N}}$ is embedded will be hard for $\mathsf {P}$.

For that reason, we introduce a notion of genuine DQBF hardness that dismisses all embedded QBF lower bounds.

Definition 7

Let $\mathsf {P}$ and $\mathsf {Q}$ be DQBF proof systems. We write ${\mathsf {Q}}\nleq ^*_p{\mathsf {P}}$ when there exists a DQBF family $\{\varPsi _n\}_{n \in \mathbb {N}}$ such that:

• (a) $\{\varPsi _n\}_{n \in \mathbb {N}}$ has polynomial-size $\mathsf {Q}$ refutations;

• (b) $\{\varPsi _n\}_{n \in \mathbb {N}}$ requires superpolynomial-size $\mathsf {P}$ refutations;

• (c) every QBF family $\{\varPhi _n\}_{n \in \mathbb {N}}$ with $\varPhi _n \le \varPsi _n$ has polynomial-size $\mathsf {P}$ refutations.

We write ${\mathsf {P}}<^*_p{\mathsf {Q}}$ when both ${\mathsf {P}}\le _p{\mathsf {Q}}$ and ${\mathsf {Q}}\nleq ^*_p{\mathsf {P}}$ hold.

Hence, ${\mathsf {P}}<^*_p{\mathsf {Q}}$ means that $\mathsf {Q}$ simulates $\mathsf {P}$, but $\mathsf {P}$ does not simulate $\mathsf {Q}$, and the hardness result for $\mathsf {P}$ is a genuine DQBF lower bound. Prior to this paper, there were no such hardness results in the DQBF literature.

5 The Tautology-Free Dependency Scheme

In this section we define the tautology-free dependency scheme ${\mathcal {D}^{\text{ tf }}}$ and show that it is fully exhibited.

For any DQBF $\varPsi$, we denote by $I_\exists ({\varPsi })$ the set of independent existential variables, i.e. $I_\exists ({\varPsi }) := \{{x\in \text{ vars }_\exists ({\varPsi })}:{S_x= \emptyset }\}$ is the set of existentials whose dependency sets are empty. For any $k \in \mathbb {N}$, we define $[k] := \{{n \in \mathbb {N}}:{n \le k}\}$.

Definition 8

(${\mathcal {D}^{\text{ rrs }}}$ [35] and ${\mathcal {D}^{\text{ tf }}}$). The reflexive resolution path dependency scheme (${\mathcal {D}^{\text{ rrs }}}$) is defined as the mapping $\varPsi \mapsto \varPsi ^\prime$, where

and $S^\prime _i$ is the set of universal variables $u\in S_i$ for which there exists a sequence $C_1, \dots ,C_k$ of clauses in $\psi$ and a sequence $p_1, \dots , p_{k-1}$ of existential literals satisfying the following conditions:

• (a) $u\in C_1$ and $\overline{{u}} \in C_k$;

• (b) for some $j \in [k-1]$, $x_i = {\text{ var }({p_j})}$;

• (c) for each $j \in [k-1]$, $p_j \in C_j$, $\overline{{p}}_j \in C_{j+1}$, and $u\in S_{\text{ var }(p_j)}$;

• (d) for each $j \in [k-2]$, $\text{ var }({p_j}) \ne \text{ var }({p_{j+1}})$.

The tautology-free dependency scheme (${\mathcal {D}^{\text{ tf }}}$) adds to ${\mathcal {D}^{\text{ rrs }}}$ the condition

• (e) for each $j \in [k-1]$, ${(C_j \cup C_{j+1})}{\upharpoonright }_{I_\exists ({\varPsi })}$ is non-tautological.

Let us give an example, illustrating that ${\mathcal {D}^{\text{ tf }}}$ is stronger than ${\mathcal {D}^{\text{ rrs }}}$.

Example 9

Consider the DQBF $\varPsi = {\exists x\forall u\exists z}\cdot {C_1 \wedge C_2}$, where $C_1 = x\vee u\vee z$ and $C_2 = \overline{{x}} \vee \overline{{u}} \vee \overline{{z}}$. The sequence of clauses $C_1, C_2$ and the sequence consisting of the single literal $p_1 = z$ show that $(u, z) \in \mathsf {deps}({{\mathcal {D}^{\text{ rrs }}}(\varPsi )})$. However, the same sequence of clauses violates condition (e) of Definition 8 because ${(C_1 \cup C_2)}{\upharpoonright }_{I_\exists ({\varPsi })}$ is a tautology on $x\in I_\exists ({\varPsi })$. Since there are no other sequences that satisfy (a), we conclude that $(u, z) \not \in \mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\varPsi )})$.    $\square$

Proposition 10

${\mathcal {D}^{\text{ tf }}}$ is a monotone dependency scheme.

Proof

It is easy to see that ${\mathcal {D}^{\text{ tf }}}(\varPsi ) \le \varPsi$ for each $\varPsi$. It remains to verify polynomial-time computability and monotonicity.

Polynomial-Time Computability. As there are polynomially many pairs, it suffices to show that whether $(u, x)$ is in $\mathsf {deps}({\varPsi })$ can be decided in polynomial time for each pair $(u, x)$. Consider the directed graph $G^{u}_{\varPsi } = (V_{\varPsi }, E^{u}_{\varPsi })$ with the vertex set $V_{\varPsi }=\{(C, a) : C\in \varPsi , a\in C\}$ and with an edge from $(C, a)$ to $(D, e)$ if $\overline{{e}} \in C$, $u\in S_{\text{ var }({e})}$, $\text{ var }({a}) \ne \text{ var }({e})$, and ${(C\cup D)}{\upharpoonright }_{I_\exists ({\varPsi })} \text { is non-tautological}$.

We claim that $(u, x) \in \mathsf {deps}({\varPsi })$ if, and only if, there is a literal $a$, $\text{ var }({a}) = x$, and clauses $C, C', C''$ such that $\overline{{u}} \in C''$, $(C', a)$ is reachable from $(C, u)$ and $(C'', e)$ is reachable from $(C', a)$ for some e. Indeed, it is easy to verify that the concatenation of a pair of such paths directly translates to the required sequences from Definition 8, and vice versa. Clearly, $G^{u}_{\varPsi }$ can be constructed in polynomial time, hence we can test all candidates $(C, u)$, compute all middle points $(C', a)$ reachable from them, and check whether some $(C'', e)$ is reachable from any of them, all in polynomial time.

Monotonicity. Let $\varPsi , \varPsi ^\prime$ be DQBFs with $\varPsi ^\prime \le \varPsi$, let $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\varPsi ^\prime )})$. We show that $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\varPsi )})$. It follows that ${\mathcal {D}^{\text{ tf }}}(\varPsi ^\prime ) \le {\mathcal {D}^{\text{ tf }}}(\varPsi )$.

There exists a sequence of clauses $C_1, \dots , C_k$ and a sequence of literals $p_1, \dots , p_{k-1}$ satisfying conditions (a) to (e) in Definition 8 with respect to $(u, x) \in \mathsf {deps}({\varPsi ^\prime })$. We show that the same sequences satisfy conditions (a) to (e) with respect to $(u, x) \in \mathsf {deps}({\varPsi })$, which implies $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\varPsi )})$.

Conditions (a), (b) and (d) are satisfied trivially. Since $\varPsi ^\prime \le \varPsi$, each dependency set $S_{\text{ var }({p_i})}$ in $\varPsi$ is a superset of the corresponding dependency set $S^\prime _{\text{ var }({p_i})}$ in $\varPsi ^\prime$, so condition (c) is satisfied. Condition (e) is satisfied since the set of independent variables $I_\exists ({\varPsi })$ is a subset of $I_\exists ({\varPsi ^\prime })$.    $\square$

Wimmer et al. [37] essentially showed that ${\mathcal {D}^{\text{ rrs }}}$ is fully exhibited, even though they did not use that term. Theorems 3 and 4 in [37] together imply that all spurious dependencies can be removed one by one in any order without changing the truth value (as is remarked at the start of Sect. 3.1 in that paper).

Theorem 11

(Wimmer et al. [37]). ${\mathcal {D}^{\text{ rrs }}}$ is fully exhibited.

We show full exhibition of ${\mathcal {D}^{\text{ tf }}}$ by reduction to full exhibition of ${\mathcal {D}^{\text{ rrs }}}$.

Theorem 12

${\mathcal {D}^{\text{ tf }}}$ is fully exhibited.

Proof

Since ${\mathcal {D}^{\text{ tf }}}(\varPsi ) \le \varPsi$, we only need to show that if $\varPsi$ is true, then ${\mathcal {D}^{\text{ tf }}}(\varPsi )$ is true. Assume $\varPsi$ is true; then there is an assignment $\sigma \in \langle {I_\exists ({\varPsi })}\rangle$ such that ${\varPsi }[{\sigma }]$ is true. We claim that $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ rrs }}}({\varPsi }[{\sigma }])})$ implies $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\varPsi )})$. Consider sequences $C_1, \dots , C_k$ and $p_1, \dots , p_{k-1}$ witnessing $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ rrs }}}({\varPsi }[{\sigma }])})$. For each $C_i$ there is $C_i' \in \varPsi$, such that $C_i = {C_i'}[{\sigma }]$, i.e. $C_i' \subseteq C_i \cup \overline{{\sigma }}$, where $\overline{{\sigma }}$ is the largest clause falsified by $\sigma$. It is readily verified that the sequences $C_1', \dots , C_k'$ and $p_1, \dots , p_{k-1}$ witness $(u, x) \in \mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\varPsi )})$. In particular, no tautologies can appear among ${(C_i' \cup C_{i+1}')}{\upharpoonright }_{I_\exists ({\varPsi })}$, because all $C_i'$ agree with $\overline{{\sigma }}$ on the variables of $I_\exists ({\varPsi })$. Hence, we get ${\mathcal {D}^{\text{ rrs }}}({\varPsi }[{\sigma }]) \le {{\mathcal {D}^{\text{ tf }}}(\varPsi )}[{\sigma }]$. By full exhibition of ${\mathcal {D}^{\text{ rrs }}}$, we have that ${\mathcal {D}^{\text{ rrs }}}({\varPsi }[{\sigma }])$ is true, which means ${{\mathcal {D}^{\text{ tf }}}(\varPsi )}[{\sigma }]$ is true, and hence ${\mathcal {D}^{\text{ tf }}}(\varPsi )$ is true.    $\square$

Example 13

Consider $\varPsi$ from Example 9. It is easy to see that $\varPsi$ is true. As shown in Example 9, ${\mathcal {D}^{\text{ tf }}}(\varPsi ) = {\exists x\exists z\forall u}\cdot {(x\vee z\vee u) \wedge (\overline{{x}} \vee \overline{{z}} \vee \overline{{u}})}$. We can see that the assignment $x\mapsto 1, z\mapsto 0$ is a model of ${\mathcal {D}^{\text{ tf }}}(\varPsi )$, which is therefore true, in line with full exhibition of ${\mathcal {D}^{\text{ tf }}}$.    $\square$

6 Proof Complexity of $\mathsf {\forall {Exp{\text{+ }}Res}({\mathcal {D}})}$

Among the first DQBF proof systems to be introduced, the expansion based system $\mathsf {\forall {Exp{\text{+ }}Res}}$ [7, 21] is arguably the most natural. In this section we investigate its proof complexity under parametrisation by dependency schemes; that is, we investigate the proof complexity of $\mathsf {P(\mathcal {D})}$ where $\mathsf {P}$ is $\mathsf {\forall {Exp{\text{+ }}Res}}$. Our main result is the following theorem.

Theorem 14

${{\mathsf {\forall {Exp{\text{+ }}Res}}}<^*_p{\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}}}<^*_p{\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})}}$.

The simulations present in Theorem 14 follow from two observations, namely (1) ${\mathcal {D}^{\text{ tf }}}(\varPsi ) \le {\mathcal {D}^{\text{ rrs }}}(\varPsi )$ (by definition), and (2) $\varPsi ^\prime \le \varPsi$ guarantees that $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutations of $\varPsi ^\prime$ are no larger than those of $\varPsi$. Indeed, given a refutation of $\varPsi$, restricting the annotations to the dependency sets of $\varPsi ^\prime$ produces a refutation of $\varPsi ^\prime$ of the same size. We refer to this property as the monotonicity of $\mathsf {\forall {Exp{\text{+ }}Res}}$.

The challenge is to show the genuine separations (Theorems 20 and 26). We note that the QBF analogue of the first separation is known [6]. The question (and indeed the notion) of a genuine separation was not previously considered.

The DQBF Proof System $\mathsf {\forall {Exp{\text{+ }}Res}}$. We recall the propositional resolution proof system [31]. A resolution refutation of a CNF $\psi$ is a sequence $C_1, \dots ,C_k$ of clauses where $C_k$ is empty and each $C_i$ is derived by one of the following rules:

• A Axiom: $C_i$ is a clause in $\psi$;

• R Resolution: $C_i = A \vee B$, where $C_r = A \vee x$ and $C_s = B \vee \overline{{x}}$, for some $r,s < i$.

The DQBF proof system $\mathsf {\forall {Exp{\text{+ }}Res}}$, with which we shall concern ourselves for the remainder of the section, is built upon resolution. Perhaps the most obvious way to decide DQBF is to reduce it to propositional logic by expanding out all the universal variables, based on the fact that $\varPsi$ is true if, and only if, the matrix of $\mathsf {exp}({\varPsi })$ is satisfiable. This is exactly how $\mathsf {\forall {Exp{\text{+ }}Res}}$ works. The input DQBF is first expanded, and then refuted in resolution.

Definition 15

($\mathsf {\forall {Exp{\text{+ }}Res}}$ [7, 21]). A $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutation of a DQBF $\varPsi$ is a resolution refutation of the matrix of $\mathsf {exp}({\varPsi })$.

It is known that $\mathsf {\forall {Exp{\text{+ }}Res}}$ is sound, complete and checkable on DQBFs [7]. Note that a $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutation of $\varPsi$ may be small even if its expansion $\mathsf {exp}({\varPsi })$ is large, since the underlying resolution refutation of $\mathsf {exp}({\varPsi })$ need not necessarily introduce every clause as an axiom.

Given that fully exhibited dependency schemes like ${\mathcal {D}^{\text{ tf }}}$ and ${\mathcal {D}^{\text{ rrs }}}$ (Theorem 12) can be incorporated into an arbitrary DQBF proof system $\mathsf {P}$ (Proposition 6), we obtain the DQBF proof systems $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ and $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})}$.

Next we show the two genuine separations that together constitute a proof of Theorem 14.

Separation of $\mathsf {\forall {Exp{\text{+ }}Res}}$ and $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$. Our separating formulas are DQBFs based on the equality QBFs [8]. Our modification exploits a refined dependency structure and utilises the following notation: the matrix-clause product of a CNF $\psi$ and a clause $C$ is the CNF $\psi \otimes C:= \{{D\cup C}:{D\in \psi }\}$.

Definition 16

(EQ$^0_n$ (adapted from [8])).$\text{ EQ }^0_n := {\varPi ^{\text{ EQ }}_n}\cdot {\psi ^{\text{ EQ }}_n}$, where

$$\begin{aligned} \begin{aligned} \varPi ^{\text{ EQ }}_n&:= \forall u_1 \cdots \forall u_n \exists x_1(\emptyset ) \cdots \exists x_n(\emptyset ) \, \exists z_1(u_1) \cdots \exists z_n(u_n) \,,\\ \psi ^{\text{ EQ }}_n&:= (\overline{{z_1}} \vee \cdots \vee \overline{{z_n}}) \wedge \bigwedge \nolimits ^n_{i=1} \Big ( (\overline{{x_i}} \vee \overline{{u_i}} \vee {z}_i) \wedge ({x}_i \vee {u}_i \vee {z}_i) \Big ) \,. \end{aligned} \end{aligned}$$

Since the dependency sets of $\text{ EQ }^0_n$ are strict subsets of those of the original equality formulas (in which each $z_i$ depends on each $u_j$), the QBF lower bound for $\mathsf {\forall {Exp{\text{+ }}Res}}$ [5] does not suffice for $\text{ EQ }^0_n$. Nonetheless, a similar argument works, based on the fact that no small subset of clauses in the expansion is unsatisfiable.

Theorem 17

$\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ requires exponential-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutations.

Proof

The total expansion of $\text{ EQ }^0_n$ is the CNF $\psi \wedge \bigwedge \nolimits ^n_{i=1} \left( (\overline{{x_i}} \vee {z_i^{\overline{{u_i}}}}) \wedge ({x}_i \vee {z_i^{{u_i}}}) \right) ,$ where $\psi$ is the conjunction of all clauses of the form $(\overline{{z_1^{a_1}}} \vee \cdots \vee \overline{{z_n^{a_n}}})$ with $\text{ var }({a_i}) = u_i$. We show that removing any of the $2^n$ clauses from $\psi$ makes the total expansion satisfiable. It follows that any resolution refutation of $\mathsf {exp}({\text{ EQ }^0_n})$ must have $2^n$ axiom clauses.

Suppose that some clause A is absent from $\psi$, and let us assume without loss of generality that $A := (\overline{{z_1^{u_1}}} \vee \cdots \vee \overline{{z_n^{u_n}}})$, i.e. the clause corresponding to $u_i \mapsto 1$ for each i (the general case is symmetrical). Now, assigning each $z_i^{u_i} \mapsto 1$ satisfies every clause in $\psi$ except A. Assigning each $z_i^{\overline{{u_i}}} \mapsto 0$ satisfies each clause $(\overline{{x_i}} \vee {z_i^{\overline{{u_i}}}})$. Finally, assigning each $x_i \mapsto 1$ satisfies each clause $({x}_i \vee {z_i^{{u_i}}})$.    $\square$

The corresponding upper bound for $\text{ EQ }^0_n$ in $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ does follow from that of the original equality QBFs (by the monotonicity of ${\mathcal {D}^{\text{ rrs }}}$ and $\mathsf {\forall {Exp{\text{+ }}Res}}$). We give a full proof nonetheless, since we will use the details later. The main point is that ${\mathcal {D}^{\text{ rrs }}}$ identifies all pairs as spurious dependencies.

Proposition 18

([6]). For all n, the dependency sets of ${\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)$ are empty.

Proof

Aiming for contradiction, suppose that there exists a sequence of clauses $C_1, \dots , C_k$ and a sequence of literals $p_1, \dots , p_{k-1}$ satisfying conditions (a) to (d) of Definition 8 with respect to $(u_i, z_i) \in \mathsf {deps}({\text{ EQ }^0_n})$. Since $z_i$ is the unique variable whose dependency set contains $u_i$, we must have $k=2$, by conditions (c) and (d). By condition (a), we have $u_i \in C_1$, so $C_1 = (x_i \vee u_i \vee z_i)$, and by condition (c) we have $p_1 = z_i$. Also by condition (c) we have $\overline{{z_i}} \in C_2$, so $C_2 = (\overline{{z_1}} \vee \dots \vee \overline{{z_n}})$. We therefore reach a contradiction, since $\overline{{u_i}} \notin C_2$ violates condition (a).    $\square$

Theorem 19

([6]).$\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutations.

Proof

By Proposition 18, the total expansion of ${\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)$ is obtained simply by removing the universal literals; that is, the matrix of $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)})$ is

$$\begin{aligned} (\overline{{z_1}} \vee \cdots \vee \overline{{z_n}}) \wedge \bigwedge \nolimits ^n_{i=1} \Big ((\overline{{x_i}} \vee {z}_i) \wedge ({x}_i \vee {z}_i) \Big ) \,. \end{aligned}$$

(2)

It is easy to see that this CNF has linear-size resolution refutations. First, resolve each pair $(x_i \vee z_i),(\overline{{x_i}} \vee z_i)$ over $x_i$, and resolve the resulting unit clauses $(z_i)$ with the remaining clause to obtain the empty clause.    $\square$

Theorems 17 and 19 together imply that $\mathsf {\forall {Exp{\text{+ }}Res}}$ does not p-simulate $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$. It remains to show that the lower bound is genuine.

Theorem 20

${\mathsf {\forall {Exp{\text{+ }}Res}}}\nleq ^*_p{\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}}$.

Proof

It is easy to see that the largest QBF $\varPhi ^0_n$ that is smaller than $\text{ EQ }^0_n$ has exactly one non-empty dependency set. Let us assume without loss of generality that this is $S_{z_n} = \{u_n\}$. We will show that $\varPhi ^0_n$ has a linear-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutation. Hence, by the monotonicity of $\mathsf {\forall {Exp{\text{+ }}Res}}$, any family of QBFs smaller than $\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutations. Thus, by Theorems 17 and 19, $\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ satisfies all the conditions of Definition 7.

It remains to show that $\varPhi ^0_n$ has a linear-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutation, or equivalently, that $\mathsf {exp}({\varPhi ^0_n})$ has a linear-size resolution refutation. It is readily verified that $\mathsf {exp}({\varPhi ^0_n})$ contains every clause in $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_{n-1})})$ except $(\overline{{z_1}} \vee \cdots \vee \overline{{z_{n-1}}})$. Figure 1 illustrates that this clause can be derived from $\mathsf {exp}({\varPhi ^0_n})$ in a constant number of resolution steps. Since $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_{n-1})})$ has a linear-size resolution refutation by Theorem 19, so does $\mathsf {exp}({\varPhi ^0_n})$.    $\square$

Fig. 1.

The prelude to a linear-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutation of $\varPhi ^0_n$. In order to reduce $\mathsf {exp}({\varPhi ^0_n})$ to $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_{n-1})})$, we need only derive the clause $(\overline{{z_1}} \vee \cdots \vee \overline{{z_{n-1}}})$.

Separation of $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ and $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})}$. For our second separation, we introduce another DQBF family. This time, we refine the prefix of an existing modification of the equality formulas.

Definition 21

(EQ$^1_n$ (adapted from [13])). For each natural number n,

$$\begin{aligned} \begin{aligned} \text{ EQ }^1_n \, := \,\,&\,\varPi ^{\text{ EQ }}_n \, \exists r(\emptyset ) \, \exists s(\{u_1, \dots , u_n\}) \, \cdot \\&\left( \psi ^{\text{ EQ }}_n \otimes (r \vee s)\right) \wedge \left( \psi ^{\text{ EQ }}_n \otimes (\overline{{r}} \vee \overline{{s}})\right) \wedge (r \vee \overline{{s}}) \wedge (\overline{{r}} \vee s)\,. \end{aligned} \end{aligned}$$

The main idea is that the addition of the fresh variables r and s is enough to obfuscate all the spurious dependencies for ${\mathcal {D}^{\text{ rrs }}}$. As such, preprocessing with ${\mathcal {D}^{\text{ rrs }}}$ has no effect, and hardness can be proved via the $\mathsf {\forall {Exp{\text{+ }}Res}}$ lower bound for $\text{ EQ }^0_n$ (Theorem 17).

Proposition 22

For each n, ${\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^1_n) = \text{ EQ }^1_n$.

Proof

To prove the proposition, we must find sequences satisfying conditions (a) to (d) of Definition 8 with respect to both $(u_i, z_i), (u_i, s) \in \mathsf {deps}({\text{ EQ }^1_n})$ for each i. In fact, for both pairs $(u_i, z_i)$ and $(u_i, s)$, the sequence of clauses

$$(r \vee x_i \vee u_i \vee z_i \vee s),(r \vee \overline{{z_1}} \vee \cdots \vee \overline{{z_n}} \vee s),(\overline{{r}} \vee \overline{{x_i}} \vee \overline{{u_i}} \vee z_i \vee \overline{{s}})$$

and the sequence of literals $z_i, s$ suffice.    $\square$

Theorem 23

$\{\text{ EQ }^1_n\}_{n \in \mathbb {N}}$ requires exponential-size $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutations.

Proof

Consider the assignment $\alpha$ defined by $r \mapsto 0, s \mapsto 0$. It is easy to see that ${\text{ EQ }^1_n}[{\alpha }] = \text{ EQ }^0_n$. Now consider the ‘expanded’ assignment $\alpha ^U$ defined by $r \mapsto 0, s^\sigma \mapsto 0$ for each $\sigma \in \langle {\{u_1, \dots , u_n\}}\rangle$. It is less easy to see, but readily verified, that ${\mathsf {exp}({\text{ EQ }^1_n})}[{\alpha ^U}] = \mathsf {exp}({{\text{ EQ }^1_n}[{\alpha }]}) = \mathsf {exp}({\text{ EQ }^0_n})$. Let $\pi$ be a $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutation of $\text{ EQ }^1_n$; that is, a resolution refutation of $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^1_n)})$. By Proposition 22, $\pi$ is a resolution refutation of $\mathsf {exp}({\text{ EQ }^1_n})$. Since resolution is closed under restrictions, ${\pi }[{\alpha ^U}]$ is a resolution refutation of ${\mathsf {exp}({\text{ EQ }^1_n})}[{\alpha ^U}] = \mathsf {exp}({\text{ EQ }^0_n})$ with $\left| {{\pi }[{\alpha ^U}]}\right| \le \left| {\pi }\right|$. By Theorem 17, $2^n \le \left| {{\pi }[{\alpha ^U}]}\right| \le \left| {\pi }\right|$.    $\square$

The situation is quite different for the tautology-free dependency scheme ${\mathcal {D}^{\text{ tf }}}$. Here, the simple detection of consecutive-clause tautologies in the variable r is enough to identify all spurious dependencies, resulting in linear-size refutations.

Proposition 24

For each n, the dependency sets of ${\mathcal {D}^{\text{ tf }}}(\text{ EQ }^1_n)$ are all empty.

Proof

Aiming for contradiction, suppose that there exists a sequence of clauses $C_1, \dots , C_k$ and a sequence of literals $p_1, \dots , p_{k-1}$ satisfying conditions (a) to (e) of Definition 8 with respect to $(u_j, y) \in \mathsf {deps}({\text{ EQ }^1_n})$, for some $y \in \{z_j, s\}$.

By condition (c), none of the $\text{ var }({p_i})$ is r. Hence, if some $C_i$ is either $(r \vee \overline{{s}})$ or $\overline{{s}} \vee r$, we must have $i=1$ or $i=k$, violating condition (a). Therefore those clauses do not appear in the sequence. It follows that none of the $\text{ var }({p_i})$ is s, for otherwise we would have consecutive clauses $C_i$ and $C_{i+1}$ whose resolvent over s contains complementary literals in r, violating condition (e).

Hence each $\text{ var }({p_i}) = z_j$, and we must have $k=2$, by conditions (c) and (d). Now we reach a contradiction as in the proof of Proposition 18, despite the addition of literals in r and s. By condition (a), we have $u_i \in C_1$, and we deduce that $\overline{{u_i}} \notin C_2$, contradicting condition (a).    $\square$

Theorem 25

$\{\text{ EQ }^1_n\}_{n \in \mathbb {N}}$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})}$ refutations.

Proof

By Proposition 24, the total expansion of ${\mathcal {D}^{\text{ tf }}}(\text{ EQ }^1_n)$ is obtained by removing universal literals, hence $\mathsf {exp}({{\mathcal {D}^{\text{ tf }}}(\text{ EQ }^1_n)})$ is the CNF

$$\begin{aligned} {\begin{matrix} &{}(r \vee \overline{{z_1}} \vee \cdots \vee \overline{{z_n}} \vee s) \wedge \bigwedge \nolimits ^n_{i=1} \Big ((r \vee \overline{{x_i}} \vee {z}_i \vee s) \wedge (r \vee {x}_i \vee {z}_i \vee s) \Big ) \wedge (r \vee \overline{{s}}) \wedge {}\\ &{}(\overline{{r}} \vee \overline{{z_1}} \vee \cdots \vee \overline{{z_n}} \vee \overline{{s}}) \wedge \bigwedge \nolimits ^n_{i=1} \Big ((\overline{{r}} \vee \overline{{x_i}} \vee {z}_i \vee \overline{{s}}) \wedge (\overline{{r}} \vee {x}_i \vee {z}_i \vee \overline{{s}}) \Big ) \wedge (\overline{{r}} \vee s) \,. \end{matrix}} \end{aligned}$$

By resolution of $(r \vee \overline{{s}})$ over r with each clause containing $\overline{{r}}$, and likewise of $(\overline{{r}} \vee s)$ with each clause containing r, we obtain all clauses in the CNF

$$(\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)}) \otimes (s)) \wedge (\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)}) \otimes (\overline{{s}}))\,,$$

where $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)})$ is the CNF (2) from the proof of Theorem 19. By resolution over s we obtain $\mathsf {exp}({{\mathcal {D}^{\text{ rrs }}}(\text{ EQ }^0_n)})$ itself, which has a linear-size resolution refutation by Theorem 19. It is easy to see that the whole refutation of $\mathsf {exp}({{\mathcal {D}^{\text{ tf }}}(\text{ EQ }^1_n)})$ is of linear size.    $\square$

Theorem 26

${\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}}\nleq ^*_p{\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})}}$.

Proof

It is easy to see that the largest QBF $\varPhi ^1_n$ that is smaller than $\text{ EQ }^1_n$ has $S_s = \{u_1, \dots , u_n\}$ and exactly one other non-empty dependency set $S_{z_i} = \{u_i\}$, where $i = n$ without loss of generality. We will prove that $\varPhi ^1_n$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutations. We therefore prove the theorem, since by Theorems 23 and 25, and the monotonicity of $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$, $\{\text{ EQ }^1_n\}_{n \in \mathbb {N}}$ satisfies all the conditions of Definition 7.

A $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutation of $\varPhi ^1_n$ is a $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutation of ${\mathcal {D}^{\text{ rrs }}}(\varPhi ^1_n)$. By definition, ${\mathcal {D}^{\text{ rrs }}}(\varPhi ^1_n) \le \varPhi ^1_n$. Now, $\varPhi ^1_n$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutations: it is readily verified that $\mathsf {exp}({\text{ EQ }^1_n})$, which has linear-size resolution refutations, can be derived from $\mathsf {exp}({\varPhi ^1_n})$ in a linear number of resolution steps. Hence ${\mathcal {D}^{\text{ rrs }}}(\varPhi ^1_n)$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}}$ refutations, by the monotonicity of $\mathsf {\forall {Exp{\text{+ }}Res}}$; i.e. $\varPhi ^1_n$ has linear-size $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutations.    $\square$

7 Tautology-Free Dependencies for QBF

We now turn our attention to dedicated QBF proof complexity, in particular to the QBF proof systems $\mathsf {{Q{\text{- }}Res}({\mathcal {D}})}$ [35] that were introduced to model dependency-aware QBF solving. We show the following.

Theorem 27

$\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$ is exponentially stronger than $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$.

Since ${\mathcal {D}^{\text{ rrs }}}$ was state-of-the-art for $\mathsf {{Q{\text{- }}Res}({\mathcal {D}})}$, Theorem 27 shows that ${\mathcal {D}^{\text{ tf }}}$ is currently the strongest known dependency scheme applicable to dependency-aware QBF solving. We recall the definition of the QBF proof system $\mathsf {{Q{\text{- }}Res}({\mathcal {D}})}$.

Definition 28

($\mathsf {{Q{\text{- }}Res}({\mathcal {D}})}$ [22, 35]). A $\mathsf {Q{\text{- }}Res}$ refutation of a DQBF $\varPsi$ is a sequence $C_1, \dots ,C_k$ of clauses in which $C_k$ is empty and each $C_i$ is derived by one of the following rules:

• A Axiom: $C_i$ is a non-tautological clause in the matrix of $\varPsi$;

• R Resolution: $C_i = A \vee B$, where $C_r = A \vee x$ and $C_s = B \vee \overline{{x}}$, for some $r,s < i$ and some $x\in \text{ vars }_\exists ({\varPhi })$, and $C_i$ is not a tautology.

• U Universal reduction: $C_i \vee a = C_r$ for some $r < i$ and some literal a with $\text{ var }({a}) = u\in \text{ vars }_\forall ({\varPsi })$ and $(u,x) \notin \mathsf {deps}({\varPsi })$ for each $x\in \text{ vars }({C_i})$.

Given a QBF dependency scheme $\mathcal {D}$, a $\mathsf {{Q{\text{- }}Res}({\mathcal {D}})}$ refutation of a QBF $\varPhi$ is a $\mathsf {Q{\text{- }}Res}$ refutation of $\mathcal {D}(\varPhi )$.

$\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$ is complete for QBF by [22], and soundness follows by full exhibition.

Theorem 29

$\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$ is a QBF proof system.

QBF Separation of $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ and $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$. Our separating formulas are the QBFs on which our DQBF modification $\text{ EQ }^1_n$ (Definition 21) was based. An exponential lower bound for these formulas in $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ was shown in [13].

Definition 30

(EQ$^2_n$ [13]). For each natural number n,

$$\begin{aligned} \begin{aligned} \text{ EQ }^2_n \, := \,\,&\,\exists r \exists x_1 \cdots \exists x_n \forall u_1 \cdots \forall u_n \exists z_1 \cdots z_n \exists s \, \cdot \\&\left( \psi ^{\text{ EQ }}_n \otimes (r \vee s)\right) \wedge \left( \psi ^{\text{ EQ }}_n \otimes (\overline{{r}} \vee \overline{{s}})\right) \wedge (r \vee \overline{{s}}) \wedge (\overline{{r}} \vee s) \end{aligned} \end{aligned}$$

Theorem 31

([6]). $\{\text{ EQ }^2_n\}_{n \in \mathbb {N}}$ requires exponential-size $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ rrs }}}})}$ refutations.

We show that $\text{ EQ }^2_n$ have linear-size refutations in $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$. The proof is along similar lines as our upper bound for $\text{ EQ }^1_n$ in $\mathsf {\forall {Exp{\text{+ }}Res}({{\mathcal {D}^{\text{ tf }}}})}$. We first show that ${\mathcal {D}^{\text{ tf }}}$ identifies the full set of spurious dependencies, which gives rise naturally to short refutations.

Proposition 32

For each n, the dependency sets of ${\mathcal {D}^{\text{ tf }}}(\text{ EQ }^2_n)$ are all empty.

Proof

Aiming for contradiction once again, suppose that there exists a sequence of clauses $C_1, \dots , C_k$ and a sequence of literals $p_1, \dots , p_{k-1}$ satisfying conditions (a) to (e) of Definition 8 with respect to $(u_i, y) \in \mathsf {deps}({\text{ EQ }^1_n})$, for some variable $y \in \{z_1, \dots , z_n, s\}$.

As in the proof of Proposition 24, we can deduce that variables r and s do not appear in the sequence of literals. By condition (a) we have $u\in C_1$. By condition (c) we have $p_1 = z_i$ and $C_2 = (\overline{{z_1}} \vee \cdots \vee \overline{{z_n}} \vee a)$, with $\text{ var }({a}) = s$. By conditions (c) and (d), we have $p_2 = \overline{{z_j}}$ for some $j \ne i$. By condition (c) $z_j \in C_2$, and by conditions (c) and (d) we must have $k = 2$. This violates condition (a), since $\overline{{u_i}} \notin C_2$.    $\square$

Theorem 33

$\{\text{ EQ }^2_n\}_{n \in \mathbb {N}}$ has linear-size $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$ refutations.

Proof

By Proposition 32, $\mathsf {deps}({{\mathcal {D}^{\text{ tf }}}(\text{ EQ }^2_n)})$ is the empty relation. It follows that all universal literals in the matrix may be removed by universal reduction. Hence, with a single axiom and universal reduction step per clause, we derive the clauses of $\mathsf {exp}({{\mathcal {D}^{\text{ tf }}}(\text{ EQ }^1_n)})$ from the proof of Theorem 25. Each step of the linear-size resolution refutation described there is also available in $\mathsf {{Q{\text{- }}Res}({{\mathcal {D}^{\text{ tf }}}})}$.    $\square$

8 Conclusions

We conclude with an interesting observation and a question for future research. The family $\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ from Definition 16 is an adaptation of the equality QBFs $\{\text{ EQ }_n\}_{n \in \mathbb {N}}$ from [8], obtained by shrinking the dependency set of each $z_i$ to just $\{u_i\}$. While in QBF $\{\text{ EQ }_n\}_{n \in \mathbb {N}}$ requires exponentially long proofs in both $\mathsf {\forall {Exp{\text{+ }}Res}}$ and $\mathsf {Q{\text{- }}Res}$ [5, 8], in DQBF $\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ remains hard only for $\mathsf {\forall {Exp{\text{+ }}Res}}$. Indeed, even though $\mathsf {Q{\text{- }}Res}$ is incomplete for DQBF, it is sound, and $\{\text{ EQ }^0_n\}_{n \in \mathbb {N}}$ has linear-size $\mathsf {Q{\text{- }}Res}$ refutations. This suggests that there may be some hidden proof-complexity relationship between $\mathsf {\forall {Exp{\text{+ }}Res}}$ and $\mathsf {Q{\text{- }}Res}$ in DQBF, even though $\mathsf {Q{\text{- }}Res}$ is incomplete there.

We have presented the strongest known dependency scheme ${\mathcal {D}^{\text{ tf }}}$. A natural question is whether some even stronger dependency schemes for (D)QBF exist.