Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study

Abstract

In Quantified Boolean Formulas QBFs, dependency schemes help to detect spurious or superfluous dependencies that are implied by the variable ordering in the quantifier prefix but are not essential for constructing countermodels. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The proof system $\texttt{QCDCL}$ recently defined by Beyersdorff and Boehm (LMCS 2023) abstracts the reasoning employed by QBF solvers based on conflict-driven clause-learning (CDCL) techniques. We show how to incorporate the use of dependency schemes into this proof system, either in a preprocessing phase, or in the propagations and clause learning, or both. We then show that when the reflexive resolution path dependency scheme $\texttt{D}^{\texttt{rrs}}$ is used, a mixed picture emerges: the proof systems that add $\texttt{D}^{\texttt{rrs}}$ to $\texttt{QCDCL}$ in these three ways are not only incomparable with each other, but are also incomparable with the basic $\texttt{QCDCL}$ proof system that does not use $\texttt{D}^{\texttt{rrs}}$ at all, as well as with several other resolution-based QBF proof systems. A notable fact is that all our separations are achieved through QBFs with bounded quantifier alternation.

1 Introduction

Despite the NP-hardness of propositional satisfiability, SAT solvers today are amazingly efficient in solving real-world instances. The best algorithms solving SAT in practice are based on the paradigm conflict-driven clause learning $\texttt{CDCL}$, that revolutionised SAT solving in the nineties. Such algorithms use a generic template as follows: repeatedly decide values of some variables, propagate hard constraints (unit clauses) until a conflict is reached, “learn” a new clause from the conflict, backtrack and continue. For unsatisfiable formulas, the learning process yields a refutation in the proof system Resolution, and it was shown over a decade ago that resolution proofs can themselves be mimicked within this framework, so $\texttt{CDCL}$ equals Resolution [1, 21]. Hence, a proof-complexity-theoretic analysis of Resolution has revealed deep insights into the strengths and limitations of this $\texttt{CDCL}$ paradigm.

With the success of propositional SAT solvers, there are many ambitious attempts now to tackle more expressive/succinct formalisms. In particular, for the PSPACE-complete problem of deciding the truth of Quantified Boolean Formulas QBF, there are now many solvers, as well as a rich (and still growing) theory about the underlying formal proof systems. Designing solvers for QBFs is a useful enterprise because many industrial applications seem to lend themselves more naturally to expressions involving both existential and universal quantifiers; see for instance [9, 24].

The proof system Resolution can be lifted to the QBF setting in many ways. The “$\texttt{CDCL}$ way” is to add a universal reduction rule, giving rise to the system $\texttt{Q}\text {-}{\texttt{Res}}$ and the more general $\texttt{QU}\text {-}{\texttt{Res}}$. Allowing contradictory literals to be merged under certain conditions gives rise to the system long-distance Q-Resolution $\texttt{LDQ}\text {-}{\texttt{Res}}$.

Another “$\texttt{CDCL}$” way is to lift the $\texttt{CDCL}$ algorithm itself to a QCDCL algorithm: decide values of variables, usually respecting the order of quantified alternation, propagate unit constraints, interpreting unit modulo universal reductions, repeat until a conflict is reached, learn a new clause, backtrack and continue. For false formulas, the learning process yields a long-distance Q-resolution refutation. However, the QCDCL refutation itself is much more restricted than an $\texttt{LDQ}\text {-}{\texttt{Res}}$ refutation. In [4], a formal proof system $\texttt{QCDCL}$ was abstracted out of the QCDCL algorithm. Noting that potentially the decision policy and the propagation policy could be modified, the authors of [4] actually formalised four different $\texttt{QCDCL}$-based proof systems. The system underlying most solvers is ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$, which we will refer to as $\texttt{QCDCL}$ without any sub/super-script; for the other systems we will explicitly write the policies.

While the aforementioned $\texttt{QCDCL}$ proof system explains the correctness of solvers for false QBFs, it ignores cube-learning from satisfying assignments. In practice, cube-learning is essential to the completeness of a $\texttt{QCDCL}$ solver; it is integral to proving a QBF to be true. (A QBF solver algorithm does not know in advance whether the input formula is true or false. It learns clauses and cubes, and concludes false/true when the empty clause/cube has been learnt.) The choice to ignore this was made in [4] because the focus there (as also here) was on refutational proof systems, proving QBFs false. In this setting, cube-learning is not an essential ingredient. However, in [13], the authors defined the system ${\texttt{QCDCL}}^{\texttt{cube}}$ that incorporates cube-learning on top of the original $\texttt{QCDCL}$, and found that cube-learning was in fact advantageous even in constructing shorter refutations for false QBFs. (More recent work (see [11]) in fact redefines $\texttt{QCDCL}$ as the augmented system with cube-learning incorporated. For this paper, we retain the notation from [4].) An interesting outcome from [11], though not directly relevant to our work, is that extracted refutations do not capture the full generality of $\texttt{LDQ}\text {-}{\texttt{Res}}$.

DepQBF [16] is the leading QCDCL solver and has many versions. Its base version still employs what the authors call “vanilla QCDCL”, and its behaviour on false QBFs is explained by the proof system $\texttt{QCDCL}$ which we are interested in exploring. Later versions of DepQBF provide options of turning on “cube learning” (when “turned on”, its behaviour is explained by the proof system ${\texttt{QCDCL}}^{\texttt{cube}}$) and also offer heuristics like whether or not to allow “dependency scheme aware propagation” and/or apply “pure literal elimination”.

A heuristic that has been found to be quite useful in many QBF solvers, and has been formalised in proof systems, is to eliminate easily-detectable spurious dependencies. In a prenex QBF, a variable “depends” on the variables preceding it in the quantifier prefix; where “depends” means that a Herbrand/Skolem function for the variable is a function of the preceding variables. However, a Herbrand function or countermodel may not really need to know the values of all preceding variables. A dependency scheme filters out as many of such unnecessary dependencies as it can detect, producing what is in effect a Dependency QBF, DQBF. Although DQBF is a significantly richer formalism that is known to be NEXP-complete (see [2, 23]), these heuristics are not aiming to solve DQBFs in general. Rather, they algorithmically detect spurious dependencies and disregard them as the algorithm proceeds. See [15,16,17, 22] for early work on this topic. Often the use of a dependency scheme makes the solvers run faster, and this is borne out by theoretical studies. Now, the universal reduction rule in the proof systems (say in $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{LDQ}\text {-}{\texttt{Res}}$) can be applied in more settings because there are fewer dependencies, and this can shorten refutations significantly. See for instance [10, 20, 25]. Note that the use of a dependency scheme must be proven to be sound and complete, and this in itself is often quite involved. The notion of a dependency scheme being “normal” was introduced in [20], where it is shown that adding any normal dependency scheme to $\texttt{LDQ}\text {-}{\texttt{Res}}$ preserves soundness and completeness.

In this paper, we examine how the usage of a dependency scheme can affect proof systems underlying the QCDCL algorithm. As far as we are aware, such a theoretical study has not been undertaken before, even though many current QBF solvers are based on the QCDCL paradigm and also do use dependency schemes. Specifically, we focus on the proof system $\texttt{QCDCL}$ (in the notation of [4], the ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$ proof system) and on the dependency scheme $\texttt{D}^{\texttt{rrs}}$ which has been studied in the context of $\texttt{Q}\text {-}{\texttt{Res}}$ and $\texttt{LDQ}\text {-}{\texttt{Res}}$, see [10, 20, 25]. We note that the proof system $\texttt{QCDCL}$ can be made aware of dependency schemes in more than one way. We identify two natural ways: (1) use a dependency scheme $\texttt{D}$ to preprocess the formula, performing reductions in the initial clauses whenever permitted by the scheme, and (2) use a dependency scheme $\texttt{D}$ in the QCDCL algorithm itself, in enabling unit propagations and in learning clauses. Denoting the first way as ${\texttt{D}+{\texttt{QCDCL}}}$ and the second as ${{\texttt{QCDCL}}(\texttt{D})}$, and noting that we could even use different dependency schemes in both these ways, we obtain the system ${\texttt{D}_1}+{\texttt{QCDCL}}(\texttt{D}_2)$. When $\texttt{D}_1$ and $\texttt{D}_2$ are both the trivial dependency scheme $\texttt{D}^{\texttt{trv}}$ inherited from the linear order of the quantifier prefix, this system is exactly $\texttt{QCDCL}$.

A third way in which the $\texttt{QCDCL}$ system can be made dependency-aware is to use dependency information in the decision policy itself. Denote this decision policy as $\texttt{DEP}\text {-}\texttt{ORD}(\texttt{D})$, in which a variable may be decided whenever all variables it depends on according to $\texttt{D}$ have been assigned. The solver DepQBF in fact does exactly this, using the standard dependency scheme $\texttt{D}^{\texttt{std}}$ in making decisions; [16, 18]. Hence it seems that this way should be incorporated first in a theoretical study. However, since the solver also uses cube-learning (essential for verifying true formulas), and since long-distance cube resolution is not yet known to be sound, the combination of long-distance resolution and dependency schemes is not supported in DepQBF 6.0. (See bottom of page 377 in [18].) In effect, then, learning has to proceed through $\texttt{Q}\text {-}{\texttt{Res}}$ or $\texttt{Q}(\texttt{D})\text {-}{\texttt{Res}}$. Since $\texttt{DEP}\text {-}\texttt{ORD}$ is subsumed in $\texttt{ANY}\text {-}\texttt{ORD}$, the net effect is captured by a sub-system of the ${\texttt{QCDCL}}^{\texttt{ANY}\text {-}\texttt{ORD}}_{\texttt{RED}}$ proof system, where the learning phase does not use long-distance steps. It is not immediately clear to us why this system is complete. The completeness of ${\texttt{QCDCL}}^{\texttt{ANY}\text {-}\texttt{ORD}}_{\texttt{RED}}$ in [4] crucially uses long-distance steps. We do believe that using $\texttt{Q}(\texttt{D})\text {-}{\texttt{Res}}$ instead of $\texttt{LDQ}\text {-}{\texttt{Res}}$ in learning should still give rise to a complete system. But, pending a formal proof of this, we for now restrict this study to the $\texttt{LEV}\text {-}\texttt{ORD}$ decision policy.

Our contributions are as follows:

• 1. We formalise the proof system ${\texttt{D}'}+{\texttt{QCDCL}}(\texttt{D})$ for dependency schemes $\texttt{D},\texttt{D}'$, and note that whenever $\texttt{D}',\texttt{D}$ are normal schemes, ${\texttt{D}'}+{\texttt{QCDCL}}(\texttt{D})$ is sound and complete (Theorem 1).

• 2. For $\texttt{D},\texttt{D}'\in \{\texttt{D}^{\texttt{trv}},\texttt{D}^{\texttt{rrs}}\}$, we study the four systems ${\texttt{D}'}+{\texttt{QCDCL}}(\texttt{D})$. As observed above, one of them is $\texttt{QCDCL}$ itself, while the others are new systems. We compare these systems with each other and show that they are all pairwise incomparable (Theorem 4). We also show that each of them is incomparable with each of the systems ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$, and $\texttt{QU}\text {-}{\texttt{Res}}$(Theorem 5), as well as with ${\texttt{QCDCL}}^{\texttt{cube}}$(Theorem 6).

  Relations among various proof systems are shown in Fig. 1.

Fig. 1

Relations between proof systems

In other words, making QCDCL algorithms dependency-aware is a “mixed bag”: in some situations this shortens runs while in others it is disadvantageous. Here are our thoughts on what this actually means.

That ${\texttt{QCDCL}}(\texttt{D})$ is stronger than $\texttt{QCDCL}$ at times is to be expected; after all, that is why the heuristic evolved. That it can be weaker at times appears a bit surprising until one recalls that even when $\texttt{QCDCL}$ was formalised in [4], it was shown that the no-reduction version ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$ can have an advantage over $\texttt{QCDCL}$; for some formulas, enabling more reductions and unit propagations can send the trails down into a trap where refuting a hard sub-formula becomes inevitable. Since dependency schemes do exactly this enabling of more reductions and propagations, custom formulas can be designed where the difference is not just between no-reductions and reductions, but also between reductions and dependency-aware reductions. This is a consequence of the level-ordering of decisions and the forcing of all unit propagations with reduction, and may not hold for the other variants of $\texttt{QCDCL}$.

That $\texttt{D}+{\texttt{QCDCL}}$ can be stronger than $\texttt{QCDCL}$ is again to be expected. That it can be weaker seems really counter-intuitive, but is again related to the comment above: the preprocessing shortens clauses and thus enables more unit propagations in subsequent trails.

One direction of our separation between $\texttt{D}+{\texttt{QCDCL}}$ and ${\texttt{QCDCL}}(\texttt{D})$ was genuinely surprising to us. We construct formulas (in Sect. 4.5) where after preprocessing (as in $\texttt{D}+{\texttt{QCDCL}}$) the resulting formula is propositional and easy to refute in Resolution, and hence the original formula is easy to refute in $\texttt{D}+{\texttt{QCDCL}}$. The same formulas, however, are hard for ${\texttt{QCDCL}}(\texttt{D})$, which uses dependencies in propagation but not for preprocessing! In other words, it is not enough for the QCDCL algorithm to be dependency-aware; this awareness must be achieved at the right stage of the algorithm.

The fact that ${\texttt{QCDCL}}(\texttt{D})$, $\texttt{D}+{\texttt{QCDCL}}$, and $\texttt{D}+{\texttt{QCDCL}}(\texttt{D})$ are all incomparable with ${\texttt{QCDCL}}^{\texttt{cube}}$ is note-worthy and interesting as allowing for cube-learning always adds strength and makes things easier as compared to without cube-learning; ${{\texttt{QCDCL}}^{\texttt{cube}}}$ as a proof system is known to be strictly more powerful than ${\texttt{QCDCL}}$ [13]. Our results show that switching on cube-learning (which most current solvers do by default) and switching on dependency-awareness as proposed here are orthogonal options. Which option is better may depend on the setting from which the instances to be solved arise.

This work is based on formalisms in [4, 10, 20, 25]. See [4] for an extensive bibliography of relevant work.

The rest of this paper is organised as follows. After spelling out the notation and required preliminaries in Sect. 2, including defining dependency schemes and describing the $\texttt{QCDCL}$ proof system, we show in Sect. 3 that the addition of normal dependency schemes results in sound and complete proof systems. In Sect. 4 we present, for some previously studied formulas as well as for some newly designed formulas, lower and/or upper bounds in the $\texttt{D}_1+{\texttt{QCDCL}}(\texttt{D}_2)$ systems when $\texttt{D}_1,\texttt{D}_2$ are in $\{\texttt{D}^{\texttt{trv}},\texttt{D}^{\texttt{rrs}}\}$. Using these bounds, we conclude in Sect. 5 that these new systems are pairwise incomparable with each other as well as with each of $\texttt{QCDCL}$, ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$, $\texttt{QU}\text {-}{\texttt{Res}}$, ${\texttt{QCDCL}}^{\texttt{cube}}$. We end with some concluding remarks in Sect. 6.

A preliminary version of this work was presented at the FSTTCS 2023 conference and appears in its proceedings, see [14].

2 Preliminaries

2.1 Basics

A Quantified Boolean Formula in prenex conjunction normal form (PCNF) consists of a prefix with an ordered list of variables, each quantified either existentially or universally, and the matrix, which is a set of clauses over these variables. That is, it has the form

$$\begin{aligned} \Phi = \mathcal {Q}\vec {x} \cdot \varphi = Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \varphi (x_1,x_2,\ldots ,x_n) \end{aligned}$$

where $\varphi$ is a propositional formula in CNF.

The formula is true if there are (Skolem) functions $s_i$ for each existentially quantified variable $x_i$, where each such $s_i$ depends only on universally quantified variables $x_j$ with $j<i$, such that substituting these $s_i$ in $\varphi$ yields a tautology. Similarly, the formula is false if there are (Herbrand) functions $h_i$ for each universally quantified variable $x_i$, where each such $h_i$ depends only on existentially quantified variables $x_j$ with $j<i$, such that substituting $h_i$ in $\varphi$ yields an unsatisfiable formula.

In this paper, we focus on false formulas; refutations must rule out the existence of Skolem functions. In the proof system $\texttt{Q}\text {-}{\texttt{Res}}$, a refutation of a false QBF is a derivation of the empty clause $\Box$ from the clauses in the matrix, using two rules: Resolution (from $A=C\vee x$ and $B=D\vee \lnot x$, derive $C\vee D$, provided the pivot x is existential and $C\vee D$ is not tautological. We denote this as $C\vee D = \texttt{res}(A,B,x)$), and Universal Reduction (from $C\vee u$ derive C if u is universal and no existential variable in C appears to the right of u in the prefix). The proof system $\texttt{QU}\text {-}{\texttt{Res}}$ generalises $\texttt{Q}\text {-}{\texttt{Res}}$ by allowing resolution on universal pivots as well. The proof system $\texttt{LDQ}\text {-}{\texttt{Res}}$ generalises $\texttt{Q}\text {-}{\texttt{Res}}$ in a different way, allowing the derivation of seemingly-tautological clauses in resolution under certain conditions: a universal variable u appearing in opposite polarities in C and D is represented as the merged literal $u^*$ in the resolvent, provided it is to the right of the pivot x.

A proof system $\texttt{P}$ simulates a proof system $\texttt{Q}$ if, for every formula, the size of the shortest $\texttt{P}$ refutation is polynomial in the size of the shortest $\texttt{Q}$ refutation. The systems $\texttt{QU}\text {-}{\texttt{Res}}$ and $\texttt{LDQ}\text {-}{\texttt{Res}}$ are both strictly more powerful than $\texttt{Q}\text {-}{\texttt{Res}}$ and incomparable with each other.

For a set S of clauses and a literal $\ell$, we use shorthand $\ell \vee S$ to denote the set of clauses $\{\ell \vee C \mid C\in S\}$.

2.2 Dependency Schemes

Dependency schemes are mappings that associate every PCNF formula $\Phi$ with a binary relation on its variables in a manner that encodes constraints on the order of pairs of variables. The most basic of dependency schemes is the trivial dependency scheme $\texttt{D}^{\texttt{trv}}$, which encapsulates the order of the quantifier prefix: an existential variable x depends on a universal variable u (i.e. $(u,x)\in \texttt{D}^{\texttt{trv}}(\Phi ))$ if x appears to the right of u in the quantifier prefix. A non-trivial dependency scheme $\texttt{D}$ produces, for any formula $\Phi$, a subset $\texttt{D}(\Phi )$ of the trivial dependencies; it does not introduce new dependencies. Some non-trivial schemes are the standard scheme $\texttt{D}^{\texttt{std}}$ and the reflexive resolution path scheme $\texttt{D}^{\texttt{rrs}}$; see [25]. Roughly speaking, in $\texttt{D}^{\texttt{rrs}}$, (u, x) is in the dependency relation of a formula if $(u,x) \in \texttt{D}^{\texttt{trv}}$ and there is a sequence of clauses with the first containing u, the last containing $\bar{u}$, some intermediate consecutive clauses containing x and $\bar{x}$, and where each pair of consecutive clauses has an existential variable, quantified after u, in opposite polarities. The non-existence of such a sequence implies that if at all there are Skolem functions for x, then there exists a Skolem function for x which does not use information about u; hence x need not depend on u. Formally, the dependence scheme is defined as follows:

Definition 1

(Reflexive Resolution Path Dependency Scheme, [25]) For a QBF $\Phi =\mathcal {Q}\phi$, the pair (u, x) is in $\texttt{D}^{\texttt{rrs}}(\Phi )$ if and only if $(u,x) \in \texttt{D}^{\texttt{trv}}(\Phi )$ and there exists a sequence of clauses $C_1, \ldots , C_n \in \phi$ and a sequence of literals $l_1,\ldots ,l_{n-1}$ such that:

• $u \in C_1$ and $\bar{u} \in C_n$,

• $x = {\textit{var}}(l_i)$ for some $i \in [n-1]$,

• ${\textit{var}}(l_i) \ne {\textit{var}}(l_{i+1})$ for each $i \in [n-2]$, and

• $(u,{\textit{var}}(l_i) \in \texttt{D}^{\texttt{trv}}(\Phi )$, $l_i \in C_i$ and $\bar{l}_i \in C_{i+1}$ for each $i \in [n-1]$.

For a dependency scheme $\texttt{D}$, a QBF $\Phi$, a universal literal $\ell _u\in \{u,\bar{u}\}$ and an existential literal $\ell _x\in \{x,\bar{x}\}$, we say that $\ell _x$ blocks $\ell _u$ if $(u,x)\in \texttt{D}(\Phi )$; in particular, this implies that x is quantified after u. For a clause C we denote by $\texttt{red}\text{- }\texttt{D}(C)$ the subclause obtained by removing all universal literals which are not blocked by any other literal in C. We denote by $\texttt{red}\text{- }\texttt{D}(\Phi )$ the QBF $\Psi$ obtained by replacing each clause C in the matrix of $\Phi$ with the clause $\texttt{red}\text{- }\texttt{D}(C)$. When $\texttt{D}=\texttt{D}^{\texttt{trv}}$, we use the notation $\texttt{red}(C)$ and $\texttt{red}(\Phi )$.

The proof systems $\texttt{Q}\text {-}{\texttt{Res}}$ and $\texttt{LDQ}\text {-}{\texttt{Res}}$, augmented with a dependency scheme $\texttt{D}$ [20], permit universal reduction of u under the more relaxed requirement that $(u,x)\not \in \texttt{D}$ for any existential variable $x\in C$. That is, they permit the derivation of $\texttt{red}\text{- }\texttt{D}(C)$ from C.

An interesting and important subclass of dependency schemes are the so-called normal dependency schemes.

Definition 2

(Normal Dependency Scheme, [20]) A dependency scheme $\texttt{D}$ is

• monotone if for every PCNF formula $\phi$, and every assignment $\tau$ to a subset of ${\textit{var}}(\phi )$, $\texttt{D}(\phi [\tau ]) \subseteq \texttt{D}(\phi )$. (Here $\phi [\tau ]$ is the restriction of $\phi$ obtained by applying the partial assignment $\tau$ to it.)

• simple if for every PCNF formula $\Phi$ of the form $\Phi = \forall X \mathcal {Q}.\phi$, every $\texttt{LDQ}(\texttt{D})\text {-}{\texttt{Res}}$ derivation P from $\Phi$, and every $u \in X$, either u or $\bar{u}$ does not appear in P.

• normal if it is both monotone and simple.

If $\texttt{D}$ is simple, then in a QBF with a leading universal block, universal variables from the first block appear in a $\texttt{LDQ}\text {-}{\texttt{Res}}$ derivation in only one polarity. This feature is useful in proving the soundness of $\texttt{LDQ}\text {-}{\texttt{Res}}$. However, for $\texttt{LDQ}\text {-}{\texttt{Res}}(\texttt{D})$, this alone is not enough. The additional property of monotonicity, expressing that applying a partial assignment can possibly erase existing dependencies but cannot create new ones, suffices to ensure soundness.

The dependency schemes $\texttt{D}^{\texttt{trv}}$, $\texttt{D}^{\texttt{std}}$, $\texttt{D}^{\texttt{rrs}}$ are all normal dependency schemes. These normal dependency schemes are important to us because for these dependency schemes $\texttt{LDQ}(\texttt{D})\text {-}{\texttt{Res}}$ is a sound proof system [20].

2.3 The Proof System $\texttt{QCDCL}$

This proof system $\texttt{QCDCL}$ defined in [4] formalises the reasoning in QCDCL algorithms. A refutation of a false QBF is a sequence of triples of the form $(T,C,\pi )$ where T is a trail (in the QCDCL algorithm) ending in a conflict, C is the clause learnt from this trail, and $\pi$ is the $\texttt{LDQ}\text {-}{\texttt{Res}}$ derivation of C explaining how C is learnt. (Recall that in (Q)CDCL, a trail is a sequence of literals, some of which are decisions made by the algorithm and the others are propagated literals. Following the standard convention, we denote decision literals in a trail in boldface.) From the last triple in the sequence we can learn the empty clause, completing the refutation. Three factors affect the construction of the refutation.

• 1. The decision policy: how to choose the next variable to branch on. In standard $\texttt{QCDCL}$ (i.e ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$, the focus of this paper), decisions must respect the quantifier prefix level order. (Variables x, y are at the same level if they are quantified the same way, and no variable with a different quantification appears between them in the prefix order.) Other policies such as $\texttt{ASS}\text {-}\texttt{ORD}$, $\texttt{ASS}\text {-}\texttt{R}\text {-}\texttt{ORD}$, $\texttt{UNI}\text {-}\texttt{ANY}$, $\texttt{ANY}\text {-}\texttt{ORD}$ are also possible; see [4, 12].

• 2. The unit propagation policy. Upon a partial assignment $\alpha$ to some variables, when does a clause C propagate a literal? In the No-Reduction policy, a clause C is unit if exactly one literal $\ell$ of C is unset, and this literal is propagated. In the Reduction policy, used by most current QCDCL solvers [16, 19], a clause C propagates literal $\ell$ if after restricting C by $\alpha$ and applying all possible universal reductions, only $\ell$ remains. In standard $\texttt{QCDCL}$ the Reduction policy is used.

  In the notation of [4], for a decision policy P and a propagation policy R, the corresponding $\texttt{QCDCL}$ proof system is denoted ${\texttt{QCDCL}}^P_R$. Thus standard QCDCL is ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$. Other variants are also defined in [4]; in particular ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$.

• 3. The set of learnable clauses. These explain the conflict at the end of a trail.

Definition 3

(Learnable clauses) From a trail

$$\begin{aligned} T := (p_{(0,1)}, \ldots , p_{(0,g_0)};\textbf{d}_\textbf{1}, p_{(1,1)}, \ldots p_{(1,g_1)}; \textbf{d}_\textbf{2}, \ldots \ldots \ldots ; \textbf{d}_\textbf{r}, p_{(r,1)}, \ldots p_{(r,g_r)} ) \end{aligned}$$

ending in a conflict $p_{(r,g_r)} = \square$, the sequence $L_T$ of learnable clauses has a clause associated with each propagation in the trail, and one more clause, described by tracing the conflict backwards through the trail as follows. ($\texttt{ante}(\ell )$ denotes the clause that causes literal $\ell$ to be propagated; i.e. the antecedent.)

• $C_{(r,g_r)} = \texttt{red}(\texttt{ante}(p_{(r,g_r)}))$.

• For $i \in \{0,1, \ldots , r\}$ and $j \in [g_i -1]$,

  $$\begin{aligned} C_{(i,j)} = {\left\{ \begin{array}{ll} \texttt{red}[\texttt{res}(C_{(i, j+1)}, \texttt{red}(\texttt{ante}(p_{(i,j)})), p_{(i,j)})] &{} \text {if} \; \bar{p}_{(i,j)} \in C_{(i,j+1)}\\ C_{(i,j+1)} &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

• For $i \in \{0,1, \ldots , r-1\}$.

  $$\begin{aligned} C_{(i,g_i)} = {\left\{ \begin{array}{ll} \texttt{red}[\texttt{res}(C_{(i+1, 1)}, \texttt{red}(\texttt{ante}(p_{(i,g_i)})), p_{(i,g_i)})] &{} \text {if} \; \bar{p}_{(i,g_i)} \in C_{(i+1,1)}\\ C_{(i+1,1)} &{}\text {otherwise} \end{array}\right. } \end{aligned}$$

In the above formulation of the $\texttt{QCDCL}$ system, we only consider trails that end in a conflict. Trails ending in a satisfying assignment are ignored. This is enough to ensure refutational completeness—the ability to prove all false QBFs false. From satisfying assignments, solvers can learn cubes (or terms), and this is necessary to prove true QBFs true. In [13] it was shown that allowing cube (or term) learning from satisfying assignments can also be advantageous while refuting false QBFs. This led to the definition of the proof system ${\texttt{QCDCL}}^{\texttt{cube}}$, which was shown to be strictly stronger than the standard $\texttt{QCDCL}$ system i.e. ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$.

Our focus, however, is on adding dependencies to the basic QCDCL system without cube learning, so wherever we talk about $\texttt{QCDCL}$ as a proof system we refer to ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$.

3 Adding Dependency Schemes to the QCDCL proof system

We first describe the generic addition of dependency schemes to $\texttt{QCDCL}$, and then show soundness and completeness for normal schemes. For a decision policy P and a propagation policy R, the corresponding $\texttt{QCDCL}$ proof system is denoted ${\texttt{QCDCL}}^P_R$. Adding a dependency scheme $\texttt{D}$ to this system can affect P, R, as well as the set of learnable clauses.

For the decision policy $P=\texttt{LEV}\text {-}\texttt{ORD}$, which is the focus of this work, adding a dependency scheme $\texttt{D}$ does not affect the decision policy. (As discussed in the introduction, it is possible to consider a decision policy that uses dependency schemes, $\texttt{DEP}\text {-}\texttt{ORD}(\texttt{D})$, but that requires independent study.)

For the propagation policy, the notion of unit clauses depends on the universal reductions allowed, and this in turn is affected by the dependency scheme. In the case of $R=\mathtt {NO\text {-}RED}$, no universal reductions are allowed anyway, so adding a dependency scheme to the proof system does not affect the policy. In the case of $R=\texttt{RED}$, the definition of a unit propagation changes. A clause C propagates a literal $\ell$ at a position in the trail if the $\forall (\texttt{D})$-reduction of C restricted to the trail so far is a unit clause. That is, the partial assignment $\alpha$ specified by the trail so far does not satisfy C, and after restricting C by $\alpha$, applying all universal reductions allowed by $\texttt{D}$ leaves the single literal $\ell$; $\texttt{red}\text{- }\texttt{D}(C\vert _\alpha )=\{\ell \}$. We denote this propagation policy as $\mathtt {RED+D}$.

The dependency scheme modifies the reduction rule, which modifies the set of learnable clauses. The set of learnable clauses is now defined in a similar way as in Definition 3, but replacing $\texttt{red}$ everywhere with $\texttt{red}\text{- }\texttt{D}$, the $\forall (\texttt{D})$ rule for universal reduction with respect to the dependency.

A completely different way in which a dependency scheme $\texttt{D}$ can be added to $\texttt{QCDCL}$ proof systems is by adding it as a preprocessing step, by applying the $\texttt{red}\text{- }\texttt{D}$ rule on the axioms of the given formula. That is, produce ${\texttt{QCDCL}}$ refutations of $\texttt{red}\text{- }\texttt{D}(\Phi )$ instead of $\Phi$.

These two ways of adding dependency schemes to $\texttt{QCDCL}$—(1) in the trail construction, propagation and learning itself, or (2) as pre-processing—can both be combined. For a particular dependency scheme $\texttt{D}$, we can think of three distinct proof systems:

• ${{\texttt{QCDCL}}(\texttt{D})}$: use $\texttt{D}$ for unit propagations and learning, but not for preprocessing.

• ${\texttt{D}+{\texttt{QCDCL}}}$: use $\texttt{D}$ only to preprocess the formula.

• ${\texttt{D}+{\texttt{QCDCL}}(\texttt{D})}$: use $\texttt{D}$ for preprocessing first and then use it again during propagation and learning.

Going a step further, we can even use different dependency schemes in the preprocessing and in the actual trails. Thus, formally, we define the general proof system ${\texttt{D}'}+{\texttt{QCDCL}}(\texttt{D})$:

Definition 4

(${\texttt{D}'}+{\texttt{QCDCL}}(\texttt{D})$ proof system) For a false QBF $\Psi =\mathcal {Q}\cdot \psi$ and a dependency scheme $\texttt{D}$, a ${{\texttt{QCDCL}}(\texttt{D})}$ derivation of a clause C from $\Psi$ is a sequence of triples $(T_i,C_i,\pi _i)$, or equivalently, a triple of sequences

$$\begin{aligned} \iota := ((T_1, \ldots , T_m), (C_1, \ldots , C_m), (\pi _1, \ldots , \pi _m)) \end{aligned}$$

where for each $i\in [m]$, the trail $T_i$ follows policies $\texttt{LEV}\text {-}\texttt{ORD}$ and $\mathtt {RED+D}$, each clause $C_j \in L_{T_j}$ is a clause learnable from $T_j$ using the $\texttt{red}\text{- }\texttt{D}$ rule, and $C_m = C$. Each $\pi _i$ is the derivation of $C_i$ from $\mathcal {Q}\cdot (\psi \cup \{C_1, \ldots , C_{i-1}\})$ in $\texttt{LDQ}(\texttt{D})\text {-}{\texttt{Res}}$.

For a false QBF $\Phi =\mathcal {Q}\cdot \phi$ and dependency schemes $\texttt{D},\texttt{D}'$, a ${\texttt{D}'}+{\texttt{QCDCL}}(\texttt{D})$ deriviation of a clause C from $\Phi$ is a ${{\texttt{QCDCL}}(\texttt{D})}$ derivation of C from $\Psi =\texttt{red}\text{- }\texttt{D}'(\Phi )$.

If $C = (\square )$, then the derivation $\iota$ is called a refutation.

Note that $\texttt{QCDCL}$ is exactly the proof system $\texttt{D}^{\texttt{trv}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{trv}})$. Using other dependency schemes instead of $\texttt{D}^{\texttt{trv}}$ is a natural generalisation.

We now show that adding normal dependency schemes $\texttt{D}_1, \texttt{D}_2$ preserves soundness and completeness.

Theorem 1

If $\texttt{D}_1$ and $\texttt{D}_2$ are normal dependency schemes, then $\texttt{D}_1+{\texttt{QCDCL}}(\texttt{D}_2)$ is a sound and complete proof system.

Proof

First we prove the soundness of the system. Suppose $\iota$ is a $\texttt{D}_1+{\texttt{QCDCL}}(\texttt{D}_2)$ refutation of a QBF $\Phi$. By definition, this is a ${{\texttt{QCDCL}}(\texttt{D}_2)}$ refutation of the QBF $\Psi =\texttt{red}\text{- }\texttt{D}_1(\Phi )$. Now, every ${\texttt{QCDCL}}(\texttt{D})$ refutation has an underlying $\texttt{LDQ}(\texttt{D})\text {-}{\texttt{Res}}$ refutation. Therefore, from $\iota$ we can extract a $\texttt{LDQ}(\texttt{D}_2)\text {-}{\texttt{Res}}$ refutation $\Pi$ of $\Psi$. Since $\texttt{D}_2$ is a normal dependency scheme, $\texttt{LDQ}(\texttt{D}_2)\text {-}{\texttt{Res}}$ is a sound proof system [20], and therefore $\Psi$ is a false QBF. Now, by completeness of $\texttt{LDQ}\text {-}{\texttt{Res}}$, there exists a $\texttt{LDQ}\text {-}{\texttt{Res}}$ refutation $\Pi '$ of $\Psi$. The reductions made to obtain $\Psi$ from $\Phi$, followed by the derivation steps in $\Pi '$, gives a $\texttt{LDQ}(\texttt{D}_1)\text {-}{\texttt{Res}}$ refutation $\Pi ''$ of $\Phi$. Since $\texttt{D}_1$ is also a normal dependency scheme, $\texttt{LDQ}(\texttt{D}_1)\text {-}{\texttt{Res}}$ is also sound, and hence, the existence of $\Pi ''$ implies that $\Phi$ is a false QBF.

Now we turn to completeness. In Theorem 3.16 of [4], $\texttt{QCDCL}$ (denoted there as ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\texttt{RED}}$) is shown to be complete. Exactly the same proof, which is actually quite intricate, works also to show the completeness of $\texttt{D}_1+{\texttt{QCDCL}}(\texttt{D}_2)$. The idea is as follows: for a false formula $\Phi$, in the 2-player evaluation game, the universal player has a winning strategy on $\Phi$. Since each clause in $\Phi$ has a subclause in $\Psi =\texttt{red}\text{- }\texttt{D}_1(\Phi )$, the same strategy is also a winning strategy in the evaluation game on $\Psi$, so $\Psi$ is false. Now, we can construct trails in level order that perform propagations whenever applicable, decide the polarity of existential variables arbitrarily, and decide the polarities of universal variables following this winning strategy. (This is possible because decisions are level-ordered.) The winning strategy guarantees that each such trail runs into a conflict. The set of learnable clauses either contains the empty clause, or is shown to contain an asserting clause—one which after backtracking becomes unit at some point in the trail—and an asserting clause is shown to be new. Thus each trail that does not terminate the refutation learns a new clause, and there are only finitely many clauses that can be added. All the arguments in this outline work also in the presence of a dependency scheme ($\texttt{D}_2$) that is used in both propagation and learning. $\square$

Having established soundness and completeness when normal dependency schemes are added, we now wish to look at how adding a particular dependency scheme affects the strength of these systems. In this work we focus on adding the reflexive resolution path dependency scheme $\texttt{D}^{\texttt{rrs}}$ as it is one of the most popular ones, and it is known that adding it to $\texttt{Q}\text {-}{\texttt{Res}}$ gives a strictly stronger system in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$. Therefore it is interesting to see if the same parallel extends to the QCDCL systems. Thus in the system $\texttt{D}_1+{\texttt{QCDCL}}(\texttt{D}_2)$, we will henceforth assume that $\texttt{D}_1,\texttt{D}_2\in \{\texttt{D}^{\texttt{trv}},\texttt{D}^{\texttt{rrs}}\}$. When a dependency scheme is $\texttt{D}^{\texttt{trv}}$, we will omit reference to it. Thus we have the systems ${\texttt{QCDCL}}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$, and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Before proceeding further, the following propositions are noteworthy to keep in mind.

Proposition 2

For a QBF $\Phi$, if $\texttt{D}(\Phi ) = \texttt{D}^{\texttt{trv}}(\Phi )$, then all of $\texttt{QCDCL}$, ${\texttt{QCDCL}}(\texttt{D})$, $\texttt{D}+{\texttt{QCDCL}}$, and $\texttt{D}+{\texttt{QCDCL}}(\texttt{D})$are equivalent on $\Phi$ and produce the same refutations.

This is simply because if $\texttt{D}=\texttt{D}^{\texttt{trv}}$, then adding the dependency scheme gives nothing new to the system as no extra reductions are enabled.

Proposition 3

For a QBF $\Phi$, $\texttt{D}^{\texttt{rrs}}(\Phi ) = \emptyset$ if and only if $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\Phi )$ is a propositional formula (no universal variables in any clause).

Further, if $\texttt{D}^{\texttt{rrs}}(\Phi ) = \emptyset$, then $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\Phi )$ is easy to refute in $\texttt{Res}$ if and only if $\Phi$ is easy to refute in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Proof

(Sketch) If $\texttt{D}^{\texttt{rrs}}(\Phi )=\emptyset$, then by definition $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\Phi )$ is propositional. If $\texttt{D}^{\texttt{rrs}}(\Phi )\ne \emptyset$, then there is some reflexive resolution path involving a universal variable u, and the occurrence of u in the first clause of the path is blocked by an existential literal even with respect to $\texttt{D}^{\texttt{rrs}}$. So $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\Phi )$ is not propositional.

If $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\Phi )$ is propositional, then after the preprocessing in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, the universal variables have no role to play and the ensuing refutation is a standard $\texttt{CDCL}$ refutation. Since $\texttt{CDCL}$ is equivalent to $\texttt{Res}$, the claim follows. $\square$

Remark 1

It is tempting to believe that if, for a QBF $\Phi$, $\texttt{red}\text{- }\texttt{D}(\Phi )$ is a propositional formula easy to refute in $\texttt{Res}$, then $\Phi$ is easy to refute in ${\texttt{QCDCL}}(\texttt{D})$ as well. However, this intuition is misleading. As we will show in Sect. 4.5, this is provably not the case.

4 Refutation Size Bounds for Some Formulas

In this section we examine the effect of adding the $\texttt{D}^{\texttt{rrs}}$ scheme to $\texttt{QCDCL}$ (obtaining the three systems ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$) by computing bounds on refutation size for some known QBF formulas, as well as for some newly-constructed QBF formulas.

4.1 The $\texttt{QParity}$ $_n$ Formulas

The first family of formulas that we study are the $\texttt{QParity}$ formulas, first defined in [6].

Formula 1

($\texttt{QParity}_n$) The $\texttt{QParity}_n$ formula has the prefix $\exists x_1, \ldots ,x_n \forall z \exists t_2, \ldots , t_n$ and the matrix

$$\begin{aligned} \begin{array}{lcccc} &{} x_1 \vee x_2 \vee \bar{t}_2 &{} \bar{x}_1 \vee \bar{x}_2 \vee \bar{t}_2 &{} x_1 \vee \bar{x}_2 \vee t_2 &{} \bar{x}_1 \vee x_2 \vee t_2 \\ \text {for}\quad i= 3,\ldots ,n: &{} x_i \vee t_{i-1} \vee \bar{t}_i &{} x_i \vee \bar{t}_{i-1} \vee t_i &{} \bar{x}_i \vee t_{i-1} \vee t_i &{} \bar{x}_i \vee \bar{t}_{i-1} \vee \bar{t}_i \\ &{}&{} t_n \vee z &{} \bar{t}_n \vee \bar{z}&{} \end{array} \end{aligned}$$

As shown in [6], these formulas are hard to refute in $\texttt{QU}\text {-}{\texttt{Res}}$ (and hence also in $\texttt{Q}\text {-}{\texttt{Res}}$ and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$). In [4] it was shown that they have short refutations in $\texttt{QCDCL}$.

It is straightforward to see that $\texttt{D}^{\texttt{rrs}}(\texttt{QParity}) = \texttt{D}^{\texttt{trv}}(\texttt{QParity})$: the last two clauses give the dependence $(z,t_n)$, and this extends to $(z,t_i)$ for all i using the remaining clauses. Hence the $\texttt{QParity}$ formulas are hard to refute in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$ as well.

On the other hand, since these formulas are easy to refute in $\texttt{QCDCL}$ (and hence also in ${\texttt{QCDCL}}^{\texttt{cube}}$), from Proposition 2 it follows that they have short refutations in all three systems: ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$, and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

4.2 The $\texttt{Equality}$ $_n$ Formulas

The next formula we study are another well-known family of QBF formulas, the $\texttt{Equality}$ formulas, first introduced in [5].

Formula 2

($\texttt{Equality}_n$) The $\texttt{Equality}_n$ formula has the prefix $\exists x_1 \cdots x_n \forall u_1 \cdots u_n \exists t_1 \cdots t_n$ and the PCNF matrix

$$\begin{aligned} \underbrace{(\bar{t}_1 \vee \cdots \vee \bar{t}_n)}_{T_n} ~\wedge ~ \bigwedge _{i=1}^n \left[ \underbrace{(x_i \vee u_i \vee t_i)}_{A_i} \wedge \underbrace{(\bar{x}_i \vee \bar{u}_i \vee t_i)}_{B_i} \right] \end{aligned}$$

(In [5], the long clause $T_n$ has positive t literals and the short clauses $A_i,B_i$ have negated t literals; it is straightforward to see that the formulations are equivalent upto renaming of variables. The formulation we define above is as used in [4, Definition 5.6].)

In [5] it was shown that these formulas are hard for $\texttt{QU}\text {-}{\texttt{Res}}$, and hence also for $\texttt{Q}\text {-}{\texttt{Res}}$ and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$. In [4] it was shown that they are hard for $\texttt{QCDCL}$ as well.

However, as shown in [13], they are easy to refute in ${\texttt{QCDCL}}^{\texttt{cube}}$.

Further, as shown in [3], $\texttt{D}^{\texttt{rrs}}(\texttt{Equality}) = \emptyset$, and there are short refutations in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$.

Since $\texttt{D}^{\texttt{rrs}}(\texttt{Equality}) = \emptyset$, no existential variable depends on any universal variable in the entire formula. Hence $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Equality})$ is the propositional formula described below.

$$\begin{aligned} \texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Equality}): \underbrace{(\bar{t}_1 \vee \cdots \vee \bar{t}_n)}_{T_n} \wedge \bigwedge _{i=1}^n \left[ \underbrace{(x_i \vee t_i)}_{A'_i} \wedge \underbrace{(\bar{x}_i \vee t_i)}_{B'_i} \right] \end{aligned}$$

This formula has a short $\texttt{Res}$ refutation (resolve $A_i'$, $B_i'$ to get $t_i$ for all i, and then resolve the $t_i$’s with $T_n$ ). Therefore by Proposition 3, the $\texttt{Equality}$ formulas are easy to refute in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Finally we come to the system ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. It turns out that these formulas are also easy to refute in this system, but this is not so straightforward. In particular, it does not follow merely because $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Equality})$ is easy to refute in $\texttt{Res}$; see Remark 1. We describe the refutation below.

Lemma 1

The $\texttt{Equality}_n$ formulas have $O(n^2)$ refutations in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Proof

Since $\texttt{D}^{\texttt{rrs}}(\texttt{Equality}_n) = \emptyset$, the propagation policy and clause learning always reduce the universal u variables from the corresponding clauses.

We will construct a polynomial size refutation for the $\texttt{Equality}_n$ formulas containing $2(n-1)$ trails. Define the following clauses: For $i\in [n]$, $T_i= \bigvee _{j \le i} \bar{t}_j$; for $i\in [n]{\setminus }\{1\}$, $L_i= \bar{x}_i \vee T_{i-1}$ and $R_i= x_i \vee T_{i-1}$.

We will construct the trails $\mathcal {U}_{n-1}, \mathcal {V}_{n-1}, \mathcal {U}_{n-2}, \mathcal {V}_{n-2}, \ldots , \mathcal {U}_1, \mathcal {V}_1$, and learn clauses $L_{n-1}, R_{n-1}, \ldots L_1, R_1$ corresponding to these trails. The $\mathcal {U}$ trails decide x variables (as many as is possible until conflict) positively; the $\mathcal {V}$ trails decide them negatively. Due to the $\texttt{RED}$ policy, each decision propagates at least one t literal.

The initial trail is

$$\begin{aligned} \mathcal {U}_{n-1}:= (\textbf{x}_\textbf{1},t_1; \textbf{x}_\textbf{2},t_2, \ldots , \textbf{x}_{\textbf{n}-\textbf{1}}, t_{n-1}, \bar{t}_n, x_n, \square ) \end{aligned}$$

and the antecedent clauses are $\texttt{ante}(t_j) = B_j$ for $j\in [n-1]$, $\texttt{ante}(\bar{t}_n) = T_n$, $\texttt{ante}(x_n) = A_n$, and $\texttt{ante}(\square ) = B_n$. From these set of clauses we learn the clause $L_{n-1} = \bar{x}_{n-1} \vee T_{n-2}$.

Restarting, create a symmetric trail to $\mathcal {U}_{n-1}$ flipping each decision:

$$\begin{aligned} \mathcal {V}_{n-1}:= (\bar{\textbf{x}}_\textbf{1},t_1; \bar{\textbf{x}}_\textbf{2},t_2, \ldots , \bar{\textbf{x}}_{\textbf{n}-\textbf{1}}, t_{n-1}, \bar{t}_n, x_n, \square ) \end{aligned}$$

where the antecedent clauses are $\texttt{ante}(t_j) = A_j$ for $j\in [n-1]$, $\texttt{ante}(\bar{t}_n) = T_n$, $\texttt{ante}(x_n) = A_n$, and $\texttt{ante}(\square ) = B_n$. From these set of clauses we learn the clause $R_{n-1} = x_{n-1} \vee T_{n-2}$.

We now go down now from $i=n-2$ down to $i=2$. At stage i, we first construct trail $\mathcal {U}_i$ by deciding x variables positively; we reach a conflict after deciding $x_i$. The trail and antecedent clauses are as follows:

$$\begin{aligned} \mathcal {U}_{i}:= (\textbf{x}_\textbf{1},t_1; \textbf{x}_\textbf{2},t_2,\ldots , \textbf{x}_{\textbf{i}}, t_{i}, x_{i+1}, \square ) \end{aligned}$$

with $\texttt{ante}(t_j)=B_j$ for $j\in [i]$, $\texttt{ante}(x_{i+1}) = L_{i+1}$, $\texttt{ante}(\square ) = R_{i+1}$. From this we learn the clause $L_i$.

Next, we create the symmetrical trail by deciding the x variables negatively

$$\begin{aligned} \mathcal {V}_{i}:= (\bar{\textbf{x}}_\textbf{1},t_1; \bar{\textbf{x}}_\textbf{2},t_2, \ldots , \bar{\textbf{x}}_{i}, t_{i}, x_{i+1}, \square ) \end{aligned}$$

with antecedent clauses $\texttt{ante}(t_j)=A_j$ for $j\in [i]$, $\texttt{ante}(x_{i+1}) = L_{i+1}$, $\texttt{ante}(\square ) = R_{i+1}$. From this we learn the clause $R_i$.

The proof ends with the two trails

$$\begin{aligned} \mathcal {U}_1 = (\textbf{x}_\textbf{1},t_1,x_2,\square ) \end{aligned}$$

with antecedents $\texttt{ante}(t_1)=B_1$, $\texttt{ante}(x_2) = L_2$, $\texttt{ante}(\square ) = R_2$, from which we learn $L_1=\bar{x}_1$, and finally the last trail

$$\begin{aligned} \mathcal {V}_1 = (\bar{x_1}, t_1, x_2, \square ) \end{aligned}$$

with antecedents $\texttt{ante}(\bar{x}_1)=L_1$, $\texttt{ante}(t_1)=B_1$, $\texttt{ante}(x_2) = L_2$, $\texttt{ante}(\square ) = R_2$, from which we learn the empty clause $\square$, completing the refutation.

The ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ refutation we have created has O(n) trails and hence overall size $O(n^2)$. $\square$

Thus the $\texttt{Equality}$ formulas, which are hard for both $\texttt{Q}\text {-}{\texttt{Res}}$ and $\texttt{QCDCL}$, become easy to refute when the power of $\texttt{D}^{\texttt{rrs}}$ is added to these systems. Thus they showcase the power of dependency schemes and discarding spurious dependencies.

4.3 The $\texttt{Trapdoor}$ $_n$ Formulas

The $\texttt{Trapdoor}$ formulas were introduced in [4], in order to compare $\texttt{QCDCL}$ with the variant with the $\mathtt {NO\text {-}RED}$ policy. The idea is to juxtapose two propositional formulas, one hard for $\texttt{Res}$ and one easy for $\texttt{Res}$, and judiciously interject universal and existential variables tying the two together. The tying is done in such a way that QCDCL trails with the $\mathtt {NO\text {-}RED}$ policy can quickly get to the easy part, whereas with $\texttt{RED}$ and the ensuing forced propagations, $\texttt{QCDCL}$ is trapped into refuting the hard part. Thus for QCDCL proof systems, allowing reductions, which force more unit propagations in a trail, is not necessarily a good thing.

Formula 3

($\texttt{Trapdoor}_n$) The $\texttt{Trapdoor}_n$ QBF has the prefix $\exists y_1, \ldots , y_{s_n} \forall w \exists t \exists x_1, \ldots , x_{s_n} \forall u$, where $s_n$ is the number or variables in the propositional pigeonhole principle $\texttt{PHP}^{n+1}_n$, and the following matrix:

$$\begin{aligned} \begin{array}{lc} &{}\texttt{PHP}_n^{n+1}(x_1, \ldots , x_{s_n}) \\ \text {for}\quad i\in [s_n]:&{} \bar{y}_i \vee x_i \vee u, y_i \vee \bar{x}_i \vee u \\ \text {for}\quad i\in [s_n]:&{} y_i \vee w \vee t , y_i \vee w \vee \bar{t} ,\bar{y}_i \vee w \vee t ,\bar{y}_i \vee w \vee \bar{t} \end{array} \end{aligned}$$

In [4], it was shown that these formulas are easy to refute in ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$ and $\texttt{Q}\text {-}{\texttt{Res}}$ (and hence also in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$  and $\texttt{QU}\text {-}{\texttt{Res}}$), but are hard to refute in $\texttt{QCDCL}$ because the reductions force unit propagations in the trails which send the solver down a “trap” of refuting $\texttt{PHP}$.

Clearly, $\texttt{D}^{\texttt{rrs}}(\texttt{Trapdoor}) = \emptyset$ since the universal variables appear in only one polarity. Thus $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Trapdoor})$is the following propositional formula:

$$\begin{aligned} \begin{array}{lc} &{}\texttt{PHP}_n^{n+1}(x_1, \ldots , x_{s_n}) \\ \text {for}\quad i\in [s_n]:&{} \bar{y}_i \vee x_i , y_i \vee \bar{x}_i \\ \text {for}\quad i\in [s_n]:&{} y_i \vee t , y_i \vee \bar{t} , \bar{y}_i \vee t , \bar{y}_i \vee \bar{t} \end{array} \end{aligned}$$

This formula has a very short $\texttt{Res}$ refutation involving the four y, t clauses for any i. Hence by Proposition 3, the $\texttt{Trapdoor}$ formulas are easy to refute in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

We observe below that they are quite easy to refute in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ as well.

Lemma 2

The $\texttt{Trapdoor}_n$ formulas have O(1)-size refutation in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Proof

As seen before, $\texttt{D}^{\texttt{rrs}}(\texttt{Trapdoor}_n) = \emptyset$. Using this fact we can construct a ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ refutation consisting of two trails $T_1$ and $T_2$. The first trail decides $y_1$ and learns $\bar{y}_1$, the second trail has no decisions. More precisely, the first trail is

$$\begin{aligned} T_1 := (\textbf{y}_\textbf{1}, t, \square ) \end{aligned}$$

with $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{ante}(\square )) = \texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\bar{y}_1 \vee w \vee \bar{t}) = (\bar{y}_1 \vee \bar{t})$, and $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{ante}(t)) = \texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\bar{y}_1 \vee w \vee t) =( \bar{y}_1 \vee t)$. This allows us to learn the clause $(\bar{y}_1)$. The second trail begins by propagating $\bar{y}_1$.

$$\begin{aligned} T_2 := (\bar{y}_1,t,\square ) \end{aligned}$$

Here, $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{ante}(\square )) = \texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(y_1 \vee w \vee \bar{t}) = y_1 \vee \bar{t}$, $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{ante}(t)) = \texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(y_1 \vee w \vee t) = y_1 \vee t$ and $\texttt{ante}(\bar{y}_1) = \bar{y}_1$ Therefore, we can learn the empty clause $(\square )$, completing the refutation. $\square$

Thus, we see that the $\texttt{Trapdoor}$ formulas which were hard for $\texttt{QCDCL}$ become easy to refute when the power of $\texttt{D}^{\texttt{rrs}}$ is added to the $\texttt{QCDCL}$ system, be it in preprocessing, unit propagation or both. This is another demonstration of the advantage of discarding spurious dependencies.

4.4 The $\texttt{Dep}\text {-}\texttt{Trap}$ $_n$ Formulas

From the previous sub-sections it may appear that adding $\texttt{D}^{\texttt{rrs}}$ to ${\texttt{QCDCL}}$ only adds to its strength and suggests that the addition of the dependency scheme gives us a strictly stronger proof system as with $\texttt{Q}\text {-}{\texttt{Res}}$. However, this is not the case; ${\texttt{QCDCL}}$’s are tricky proof systems. In the previous sections we discussed the $\texttt{QParity}$ and $\texttt{Trapdoor}$ formulas; these were used in [4], to show that neither of ${{\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}}$ and ${\texttt{QCDCL}}$ simulates the other. For the $\texttt{Trapdoor}$ formulas, the reduction sends the ${\texttt{QCDCL}}$ refutation down a “trap” but not the ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$ refutation. This motivates the idea of designing a formula where adding the dependency scheme enables reductions that send the refutation down a trap into which the seemingly weaker systems do not fall. Based on this idea, we introduce the family $\texttt{Dep}\text {-}\texttt{Trap}$ which is a slight modification of the $\texttt{Trapdoor}$ family, and is defined as follows:

Formula 4

($\texttt{Dep}\text {-}\texttt{Trap}_n$) The $\texttt{Dep}\text {-}\texttt{Trap}_n$ formula has the prefix $\exists y_1, \ldots , y_{s_n} \forall w \exists t \forall u \exists x_1, \ldots , x_{s_n}$, and the matrix is as given below.

$$\begin{aligned} \begin{array}{lc} &{}\texttt{PHP}_n^{n+1}(x_1, \ldots , x_{s_n}) \\ \text {for}\quad i\in [s_n]:&{} \bar{y}_i \vee u \vee x_i , y_i \vee u \vee \bar{x}_i \\ \text {for}\quad i\in [s_n]:&{} y_i \vee w \vee t , y_i \vee w \vee \bar{t} ,\bar{y}_i \vee w \vee t , \bar{y}_i \vee w \vee \bar{t} \\ &{}\bar{w} \vee \bar{t} \end{array} \end{aligned}$$

Note that there are two differences from the $\texttt{Trapdoor}_n$ formulas. Firstly, the universal variable u which was earlier quantified at the end is now quantified just before the existential variables $x_1, \ldots , x_{s_n}$. Secondly, there is an additional clause $\bar{w} \vee \bar{t}$. We will see that these serve a dual purpose: the shifting of the position of u stops ${\texttt{QCDCL}}$ from falling into the trap, making the formulas easy to refute in $\texttt{QCDCL}$, while the additional clause prevents the $\texttt{D}^{\texttt{rrs}}$ scheme from bypassing the trap as it used to in the $\texttt{Trapdoor}_n$ formulas, since now instead of being the empty set, $\texttt{D}^{\texttt{rrs}}(\texttt{Dep}\text {-}\texttt{Trap}) = \{(w,t)\}$. Therefore, $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Dep}\text {-}\texttt{Trap})$ isn’t a propositional formula anymore; in fact it is the following QBF:

$$\begin{aligned} \begin{array}{lc} &{}\texttt{PHP}_n^{n+1}(x_1, \ldots , x_{s_n}) \\ \text {for}\quad i\in [s_n]:&{} \bar{y}_i \vee x_i , y_i \vee \bar{x}_i \\ \text {for}\quad i\in [s_n]:&{} y_i \vee w \vee t , y_i \vee w \vee \bar{t}, \bar{y}_i \vee w \vee t , \bar{y}_i \vee w \vee \bar{t} \\ &{} \bar{w} \vee \bar{t} \end{array} \end{aligned}$$

We observe below that for exactly the same reasons as $\texttt{Trapdoor}$, the $\texttt{Dep}\text {-}\texttt{Trap}$ formulas are easy to refute in ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, and hence also in $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$, and $\texttt{QU}\text {-}{\texttt{Res}}$. Furthermore, the shifting of u to before the $x_i$’s stops $\texttt{QCDCL}$ from going down the “trap”, and hence the formulas are easy to refute in $\texttt{QCDCL}$ (and in ${\texttt{QCDCL}}^{\texttt{cube}}$).

Lemma 3

The $\texttt{Dep}\text {-}\texttt{Trap}$ formulas have polynomial-size refutations in ${\texttt{QCDCL}}$, ${{\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}}$, $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{QU}\text {-}{\texttt{Res}}$ and $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$.

Proof

First we will show that the $\texttt{Dep}\text {-}\texttt{Trap}$ formulas have a linear-size refutation in ${\texttt{QCDCL}}$. We will do so by constructing a complete refutation. The first trail decides all y variables positively, decides w negatively, and then propagates t and a conflict. Unlike $\texttt{Trapdoor}$ we don’t propagate an x after an y decision, since the u cannot be reduced and so blocks unit propagation.

$$\begin{aligned} T_1 := (\textbf{y}_\textbf{1}; \textbf{y}_\textbf{2}; \ldots ; \textbf{y}_{\textbf{s}_\textbf{n}};\bar{\textbf{w}}, t, \square ) \end{aligned}$$

where $\texttt{ante}(\square ) = (\bar{y}_1 \vee w \vee \bar{t})$ and $\texttt{ante}(t) = (\bar{y}_1 \vee w \vee t)$. Hence the set of learnable clauses for this trail is $L_{T_1} = ((\bar{y}_1 \vee w \vee \bar{t}), (\bar{y}_1))$; allowing us to learn the clause $(\bar{y}_1)$. Now the second trail propagates $(\bar{y}_1)$ followed by remaining decisions as before.

$$\begin{aligned} T_2 := (\bar{y}_1; \textbf{y}_\textbf{2}; \ldots ; \textbf{y}_{\textbf{s}_\textbf{n}};\bar{\textbf{w}}, t, \square ) \end{aligned}$$

where $\texttt{ante}(\square ) = (y_1 \vee w \vee \bar{t})$, $\texttt{ante}(t) = (y_1 \vee w \vee t)$, and $\texttt{ante}(\bar{y}_1)=\bar{y}_1$. Therefore, the set of learnable clauses for this trail is $L_{T_2} = ((y_1 \vee w \vee \bar{t}), (y_1), (\square ))$ which allows us to learn the empty clause $(\square )$, completing the refutation. The refutation size is $O(s_n)$, which is linear in the formula size.

Since none of the unit propagations in the two trails above employed a universal reduction, the same refutation is also a valid linear-size refutation in ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$. Since all the other systems mentioned in the lemma simulate ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, $\texttt{Dep}\text {-}\texttt{Trap}$ has polynomial-size refutations in these proof systems as well. $\square$

Next we show that these formulas are hard to refute in $\texttt{QCDCL}$ variants that use $\texttt{D}^{\texttt{rrs}}$.

Lemma 4

Refutations of the $\texttt{Dep}\text {-}\texttt{Trap}_n$ formulas in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ require exponential size.

Proof

$\texttt{D}^{\texttt{rrs}}(\texttt{Dep}\text {-}\texttt{Trap}_n) = \{(w,t)\}$. This means that the universal variable w cannot be reduced from any axiom clause it appears in as they all also contain the variable t, whereas the universal variable u can be reduced from the axiom clauses as no existential variable depends on it.

Let us first see hardness for ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. Since u can be reduced but not w, the proof of hardness of $\texttt{Trapdoor}$ in $\texttt{QCDCL}$ from [4] carries over as is to hardness of $\texttt{Dep}\text {-}\texttt{Trap}$ in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$: the decisions on the y variables propagate x literals, sending the trails down the $\texttt{PHP}$ trap. The additional clause cannot change the course of such trails, because its variables appear after the y part in the prefix and decisions are required to be level-ordered.

Next consider the other two variants. Preprocessing yields the QBF $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Dep}\text {-}\texttt{Trap})$ described above. Now all trails in a refutation of this formula must start with deciding the $y_i$’s; these decisions propagate the $x_i$’s; and w cannot be reduced from the clauses it exists in (irrespective of whether we allowed $\forall (\texttt{D})$-reductions or not) nor decided before all the $y_i$’s are decided. Again, the proof of hardness of $\texttt{Trapdoor}$ in $\texttt{QCDCL}$ from [4] lifts to hardness of $\texttt{Dep}\text {-}\texttt{Trap}$ in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. $\square$

The $\texttt{Dep}\text {-}\texttt{Trap}$ formulas are thus easy for $\texttt{QCDCL}$, but become hard to refute when $\texttt{D}^{\texttt{rrs}}$ is added to the system demonstrating that allowing more reductions and removing spurious dependencies does not necessarily help for the $\texttt{QCDCL}$ system.

4.5 The $\texttt{TwoPHPandCT}$ $_n$ Formulas

The formulas in the previous sections seem to suggest that Proposition 3 could also extend to include ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. We show now that this is not the case. The motivation for defining the following formula also comes from the $\texttt{Trapdoor}$ formulas, using the propositional hardness of $\texttt{PHP}$ and the “easiness” of the (negation of) complete tautology on two variables. The added new element is the use of two disjoint copies of the hard part.

Formula 5

($\texttt{TwoPHPandCT}_n$) The $\texttt{TwoPHPandCT}_n$ formulas have the prefix, $\mathcal {Q}= \forall u \exists x_1\cdots x_{s_n}$ $\exists y_1 \cdots y_{s_n}$ $\forall v \exists z_1,z_2$ and the matrix

$$\begin{aligned}\begin{array}{c} u \vee \texttt{PHP}(x_1, \ldots , x_{s_n}) \\ \bar{u} \vee \texttt{PHP}(y_1, \ldots , y_{s_n}) \\ v \vee z_1 \vee z_2 , v \vee \bar{z}_1 \vee z_2 , v \vee z_1 \vee \bar{z}_2 , v \vee \bar{z}_1 \vee \bar{z}_2 \\ \end{array} \end{aligned}$$

Observe that these formulas are easy to refute in $\texttt{Q}\text {-}{\texttt{Res}}$, using the four $z_1,z_2$ clauses, and hence also easy to refute in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$ and $\texttt{QU}\text {-}{\texttt{Res}}$.

Since v appears in only one polarity and $u, \bar{u}$ appear in clauses with disjoint variables, hence $\texttt{D}^{\texttt{rrs}}(\texttt{TwoPHPandCT}) = \emptyset$ and $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{TwoPHPandCT})$ is the propositional formula

$$\begin{aligned} \begin{array}{c} \texttt{PHP}(x_1, \ldots , x_{s_n}) \\ \texttt{PHP}(y_1, \ldots , y_{s_n}) \\ z_1 \vee z_2 , \bar{z}_1 \vee z_2 , z_1 \vee \bar{z}_2, \bar{z}_1 \vee \bar{z}_2, \end{array} \end{aligned}$$

This formula is easy to refute in $\texttt{Res}$using the $z_1,z_2$ clauses; hence by Proposition 3, the original QBFs are easy to refute in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

The final question arises now as to how hard they are to refute in $\texttt{QCDCL}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$. And the answer is that it is hard for all three systems.

Lemma 5

The QBF formulas $\texttt{TwoPHPandCT}$ $_n$ require exponential size refutations in $\texttt{QCDCL}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$.

Proof

None of the three systems $\texttt{QCDCL}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$or ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$ allow for any preprocessing. Hence the first decision in each of these three systems must be on u, which allows for no propagations in any case. And depending on the choice of u, the next set of decisions are either all on x variables or all on y variables. The variable v could be dropped during unit propagation in the ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ system, but neither $z_1$ or $z_2$ could be decided or propagated before all the y or x variables are decided/propagated. Therefore, all conflicts these trails hit come directly from the $\texttt{PHP}$ clauses. Thus refuting $\texttt{TwoPHPandCT}$ in $\texttt{QCDCL}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ or ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$is equivalent to refuting $\texttt{PHP}$ in CDCL, requiring exponential size. $\square$

These formulas highlight two important facts: firstly that ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ is not the same as $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ or $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and does not simulate them either. And secondly, even in the case when $\texttt{D}^{\texttt{rrs}}= \emptyset$ and reducing the formula by $\texttt{D}^{\texttt{rrs}}$ gives us an easy propositional formula, it can still be hard to refute for ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

4.6 The $\texttt{RRSTrapEq}$ $_n$ Formulas

The next family of formulas are obtained by making a slight modification to the $\texttt{Equality}$ formulas. The motivation to define such formulas comes from trying to ascertain whether after preprocessing with $\texttt{D}^{\texttt{rrs}}$, does allowing reductions using $\texttt{D}^{\texttt{rrs}}$ for unit propagation add any power over trivial universal reductions.

Formula 6

($\texttt{RRSTrapEq}_n$) The $\texttt{RRSTrapEq}_n$ formula has the prefix $\exists a \exists x_1 \cdots x_n \forall u_1 \cdots u_n \exists t_1 \cdots t_n \exists b$ and the PCNF matrix as below:

$$\begin{aligned} \underbrace{(\bar{t}_1 \vee \cdots \vee \bar{t}_n)}_{T_n}&\wedge \bigwedge _{i=1}^n \left[ \underbrace{(x_i \vee u_i \vee t_i \vee b)}_{A_i} \wedge \underbrace{(\bar{x}_i \vee \bar{u}_i \vee t_i \vee b)}_{B_i} \right] \\&\wedge \bigwedge _{i=1}^n \underbrace{(u_i \vee \bar{b})}_{C_i} \wedge (a \vee \bar{b}) \wedge (\bar{a} \vee \bar{b}) \end{aligned}$$

The prefix has the variables of $\texttt{Equality}$ sandwiched between a and b. The underlying idea in the formulation is that unlike $\texttt{D}^{\texttt{rrs}}(\texttt{Equality})$ which is empty, the additional $C_i$ clauses make $\texttt{D}^{\texttt{rrs}}(\texttt{RRSTrapEq})=\{(u_i,b): i \in [n]\}$. Further, adding b to the x, u, t clauses along with that results in $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{RRSTrapEq})= \texttt{RRSTrapEq}$. Now, since preprocessing by $\texttt{D}^{\texttt{rrs}}$ does not change the formula at all, therefore the refutational hardness and in fact the refutation for these two formulas will be exactly the same for the pair of systems $\texttt{QCDCL}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$, and similarly for the pair ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Lemma 6

The $\texttt{RRSTrapEq}$ formulas have polynomial size refutations in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, but require exponential size refutations in $\texttt{QCDCL}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$

Proof

Since, $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{RRSTrapEq})$= $\texttt{RRSTrapEq}$, there is no effect of preprocessing, and all 4 systems start off by refuting the same formula. Now, for any of the four proof systems, if you consider any trail $\mathcal {T}$ of a refutation, the first decision must be on the variable a, and irrespective of the manner of that decision we propagate $\bar{b}$, which satisfies all the $C_i$ clauses and removes the b literal from the $A_i$ and $B_i$ clauses. The remaining formula at this point is exactly the $\texttt{Equality}$ formula, i.e. $\texttt{RRSTrapEq}|_{a=*, b=0} = \texttt{Equality}$, and hence refuting the $\texttt{RRSTrapEq}$ formulas is equivalent to refuting the $\texttt{Equality}$ formulas in $\texttt{QCDCL}$ and ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, which we know are hard and easy respectively.

Therefore, $\texttt{RRSTrapEq}$ formulas have polynomial size refutations in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, but require exponential size refutations in $\texttt{QCDCL}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ $\square$

Additionally, since the $\texttt{Equality}$ formulas are embedded in the $\texttt{RRSTrapEq}$ formula, and since $\texttt{QU}\text {-}{\texttt{Res}}$ is closed under restrictions, the $\texttt{RRSTrapEq}$ formulas are hard for $\texttt{QU}\text {-}{\texttt{Res}}$ and in turn $\texttt{Q}\text {-}{\texttt{Res}}$ and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$. However, they are easily seen to have short refutations in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$: resolve the last two clauses to derive $\bar{b}$, use it to remove b from the $A_i$ and $B_i$, now use $\texttt{D}^{\texttt{rrs}}$ reductions to remove the u literals, resolve on x to derive unit $t_i$ clauses, and remove them from $T_n$ sequentially.

4.7 The $\texttt{PreDepTrap}$ $_n$ Formulas

The previous section underlined that preprocessing by $\texttt{D}^{\texttt{rrs}}$ may not necessarily make $\texttt{D}^{\texttt{rrs}}$ during propagation obsolete and/or give an advantage. It is reasonable to believe that at least it won’t make things worse. But the following example shows that this is not the case: preprocessing before allowing a QCDCL system to refute could in fact make the refutation harder.

The construction of the formula is pretty straightforward. It is the disjoint union of the two formulas $\texttt{Dep}\text {-}\texttt{Trap}$ and $\texttt{Equality}$, connected by a universal quantified right at the beginning, appearing in the two sub-formulas in opposite polarities.

Formula 7

($\texttt{PreDepTrap}_n$) The $\texttt{PreDepTrap}_n$ formula has the prefix $\forall a \exists y_1 \cdots y_{s_n}$ $\forall w \exists t \forall u$ $\exists x_1\cdots x_{s_n} \exists p_1 \cdots p_n \forall q_1 \cdots q_n \exists r_1 \cdots r_n$, and the matrix

$$\begin{aligned} \begin{array}{c} a \vee \texttt{Dep}\text {-}\texttt{Trap}(y_1, \ldots , y_{s_n}, w,t,u, x_1,\ldots ,x_{s_n}) \\ \bar{a} \vee \texttt{Equality}(p_1,\ldots , p_n, q_1, \ldots , q_n, r_1, \ldots , r_n) \end{array} \end{aligned}$$

(Recall that $a \vee \texttt{Dep}\text {-}\texttt{Trap}$ is the disjunction of a with every clause of $\texttt{Dep}\text {-}\texttt{Trap}$, and similarly for $\bar{a} \vee \texttt{Equality}$.)

First consider the ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$ and $\texttt{QCDCL}$ ystems. Since there is no preprocessing, the first decision of every trail must set the variable a. For a trail that starts with the decision $\bar{a}$, the $\texttt{PreDepTrap}$ formula reduces exactly to $\texttt{Dep}\text {-}\texttt{Trap}$ formula which we know is easy to refute in ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$ as well as $\texttt{QCDCL}$ (Sect. 4.4). Therefore, the $\texttt{PreDepTrap}$formulas are easy to refute in $\texttt{QCDCL}$ and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, and as a consequence in $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$, $\texttt{QU}\text {-}{\texttt{Res}}$, and ${\texttt{QCDCL}}^{\texttt{cube}}$.

Next, consider adding $\texttt{D}^{\texttt{rrs}}$. Since the opposite polarities of a appear in clauses with disjoint non-interacting sets of variables, no existential variable depends on a. Since $\texttt{D}^{\texttt{rrs}}(\texttt{Equality}) = \emptyset$, no variable depends on a q variable. Thus $\texttt{D}^{\texttt{rrs}}(\texttt{PreDepTrap}) = \texttt{D}^{\texttt{rrs}}(\texttt{Dep}\text {-}\texttt{Trap})$.

In the ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ system, where there is no preprocessing, the first decision of every trail must again set the variable a. For trails that start with the decison a, the formula immediately reduces exactly to the $\texttt{Equality}$ formulas, which are easy to refute in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, Lemma 1. The refutation in the proof of Lemma 1, preceded by the decision a, gives a valid refutation for the $\texttt{PreDepTrap}$ formulas. Therefore these formulas are easy to refute in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Finally, consider the case when the formula is preprocessed. We show that this makes refutations exponentially long.

Lemma 7

The $\texttt{PreDepTrap}$ formulas require exponential size refutations in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Proof

Since $\texttt{D}^{\texttt{rrs}}(\texttt{PreDepTrap}) = \texttt{D}^{\texttt{rrs}}(\texttt{Dep}\text {-}\texttt{Trap})$, the formula $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}$ $(\texttt{PreDepTrap})$ has the matrix

$$\begin{aligned} \begin{array}{lc} &{}\texttt{PHP}_n^{n+1}(x_1, \ldots , x_{s_n}) \\ \text {for}\quad i\in [s_n]:&{} \bar{y}_i \vee x_i , y_i \vee \bar{x}_i \\ \text {for}\quad i\in [s_n]:&{} y_i \vee w \vee t , y_i \vee w \vee \bar{t} , \bar{y}_i \vee w \vee t , \bar{y}_i \vee w \vee \bar{t} \\ &{}\bar{w} \vee \bar{t} \\ &{}(\bar{r}_1 \vee \cdots \vee \bar{r}_n) \\ \text {for}\quad i\in [n] &{} (p_i \vee r_i) \\ \text {for}\quad i\in [n] &{} (\bar{p}_i \vee r_i) \end{array} \end{aligned}$$

Now the variable a, though still in the quantifier prefix, has no effect on the trails. It can be decided arbitrarily in the beginning, and then the goal is to refute $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{PreDepTrap})$ in $\texttt{QCDCL}$ and ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. At this point, therefore, all trails must start with deciding the $y_i$’s, propagating the $x_i$’s. The only other universal variable w is blocked by t in all clauses where it occurs. Since we use $\texttt{LEV}\text {-}\texttt{ORD}$, it cannot be decided before all the $y_i$’s are decided. Nor can t be propagated before w is decided. Since the $p_i$’s and $r_i$’s also cannot be decided before the $y_i$’s, the trails are led into the trap of refuting $\texttt{PHP}$. The proof of hardness of $\texttt{Trapdoor}$ in $\texttt{QCDCL}$ from [4] carries over exactly as it is to show hardness for $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. $\square$

4.8 The $\texttt{PropDep}\text {-}\texttt{Trap}$ $_n$ Formulas

The previous section illustrated an example where having $\texttt{D}^{\texttt{rrs}}$ as a preprocessing technique was a detriment to refuting it and in fact it was better to use $\texttt{D}^{\texttt{rrs}}$ only in unit propagation, and not also for preprocessing. This leads to the question—could there be a formula where having $\texttt{D}^{\texttt{rrs}}$ only for preprocessing was strictly better than having it for both preprocessing and propagation? Addressing this led to the birth of the following formula which is a slight modification of the $\texttt{Dep}\text {-}\texttt{Trap}$ formulas, and which witnesses that the answer is yes.

Formula 8

($\texttt{PropDep}\text {-}\texttt{Trap}_n$) The $\texttt{PropDep}\text {-}\texttt{Trap}$ $_n$ formulas have the prefix $\exists s \; \exists y_1 \cdots y_{s_n} \forall w \exists t \forall b_1,b_2$ $\exists x_1 \cdots x_{s_n} \; \exists z_1,z_2$ and the matrix as given below.

$$\begin{aligned} \begin{array}{lc} &{}\texttt{PHP}_n^{n+1}(x_1, \ldots , x_{s_n}) \\ \text {for}\quad i\in [s_n]:&{} \bar{y}_i \vee b_1 \vee x_i \vee z_1 , y_i \vee b_2 \vee \bar{x}_i \vee z_2 \\ &{}s \vee w \vee t , s \vee w \vee \bar{t} , \bar{s} \vee w \vee t , \bar{s} \vee w \vee \bar{t} \\ &{}\bar{w} \vee \bar{t} \\ &{}\bar{b}_1 \vee \bar{z}_1, \bar{b}_2 \vee \bar{z}_2, \bar{z}_1, \bar{z}_2 \end{array} \end{aligned}$$

First observe that the presence of the four s, w, t clauses make this formula very easy to refute in $\texttt{Q}\text {-}{\texttt{Res}}$ and hence in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$ and $\texttt{QU}\text {-}{\texttt{Res}}$.

Next, notice that the formulas are also easy to refute in ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, $\texttt{QCDCL}$, and ${\texttt{QCDCL}}^{\texttt{cube}}$ because, after the initial propagation of the unit clauses $\bar{z}_1, \bar{z}_2$ in level 0, there are no propagations possible before a w decision; the decisions on s and all the $y_i$’s cause no propagations. A trail that decides s and $\bar{w}$ quickly reaches a conflict and learns $\bar{s}$; a next trail that propagates $\bar{s}$ and decides $\bar{w}$ then learns the empty clause.

Coming to $\texttt{D}^{\texttt{rrs}}$, it can be seen that $\texttt{D}^{\texttt{rrs}}(\texttt{PropDep}\text {-}\texttt{Trap}) = \{(w,t),(b_1,z_1),(b_2,z_2)\}$. Therefore, $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{PropDep}\text {-}\texttt{Trap})$= $\texttt{PropDep}\text {-}\texttt{Trap}$. This means that a $\texttt{QCDCL}$ refutation is also a $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ refutation, and therefore $\texttt{PropDep}\text {-}\texttt{Trap}$ has short refutations in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$.

We now show that refuting these formulas in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ is hard.

Lemma 8

The $\texttt{PropDep}\text {-}\texttt{Trap}$ formulas require exponential size refutations in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

Proof

Since $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{PropDep}\text {-}\texttt{Trap})$= $\texttt{PropDep}\text {-}\texttt{Trap}$, a $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ refutation in this case is just a ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ refutation, so it suffices to show hardness for the latter. Let us observe how a ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ refutation looks. The two unit clauses $\bar{z}_1, \bar{z}_2$ get propagated initially and then s and the $y_i$’s have to be decided. A decision on s, irrespective of the polarity, causes no further propagations until w is also decided, as every clause containing the variable s also contains the variables w and t, and the reduction of w is blocked by t. Since neither $(b_1,x_i)$ nor $(b_2,x_i)$ is in $\texttt{D}^{\texttt{rrs}}$, a decision on variable $y_i$ propagates either $x_i$ (due to the clause containing $\bar{y}_i$, where $b_1$ can now be reduced), or $\bar{x}_i$ (due to the clause containing $y_i$, where $b_2$ can now be reduced). The propagating of $x_i$ due to $y_i$ sends the ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ refutation down the same “trap” as the $\texttt{Trapdoor}$ formulas for $\texttt{QCDCL}$[4], and thus ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ requires exponential size refutations to refute these formulas. $\square$

4.9 The $\texttt{TwinEq}$ $_n$ Formulas

The $\texttt{TwinEq}$ formulas were introduced in [13] to show hardness in the system ${\texttt{QCDCL}}^{\texttt{cube}}$. They are formally defined as follows:

Formula 9

($\texttt{TwinEq}_n$ [13]) The $\texttt{TwinEq}_n$ formula has the prefix $\exists x_1 \cdots x_n \forall u_1 \cdots u_n, w_1, \ldots , w_n \exists t_1 \cdots t_n$ and the PCNF matrix

$$\begin{aligned} \underbrace{(\bar{t}_1 \vee \cdots \vee \bar{t}_n)}_{T_n}&\wedge \bigwedge _{i=1}^n \left[ \underbrace{(x_i \vee u_i \vee t_i)}_{A_i} \wedge \underbrace{(\bar{x}_i \vee \bar{u}_i \vee t_i)}_{B_i} \right] \\&\wedge \bigwedge _{i=1}^n \left[ \underbrace{(x_i \vee w_i \vee t_i)}_{C_i} \wedge \underbrace{(\bar{x}_i \vee \bar{w}_i \vee t_i)}_{D_i} \right] \end{aligned}$$

These formulas are hard for ${\texttt{QCDCL}}^{\texttt{cube}}$, and hence also for $\texttt{QCDCL}$ and ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$. For the same reason as for $\texttt{Equality}$ (the size-cost-capacity theorem from [5]), they are also hard for $\texttt{QU}\text {-}{\texttt{Res}}$ and $\texttt{Q}\text {-}{\texttt{Res}}$.

It is easy to show that $\texttt{D}^{\texttt{rrs}}(\texttt{TwinEq}) = \emptyset$ (just as $\texttt{D}^{\texttt{rrs}}(\texttt{Equality})$ is shown to be $\emptyset$). Therefore, $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{TwinEq})$ is a propositional formula, and in fact is the same formula as $\texttt{red}\text{- }\texttt{D}^{\texttt{rrs}}(\texttt{Equality})$. Therefore, due to the same argument as for the $\texttt{Equality}$ formulas in Sect. 4.2, the $\texttt{TwinEq}$ formulas are easy to refute in $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$, $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$, $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

5 Relation Between Proof Systems

The previous section saw us study the bounds for known as well as our newly-constructed formulas in a plethora of proof systems. Using these obtained bounds, in this section we look to obtain the relations of our newly defined proof systems using $\texttt{D}^{\texttt{rrs}}$ with $\texttt{QCDCL}$ among themselves, as well as their relation with other QBF proof systems.

First we observe that the four versions of $\texttt{QCDCL}$ that use or do not use $\texttt{D}^{\texttt{rrs}}$ in either of the two ways are all pairwise incomparable.

Theorem 4

The proof systems in $\{ {\texttt{QCDCL}}, {\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}}), \texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}, \texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})\}$ are pairwise incomparable.

Proof

Of the four systems under consideration, the $\texttt{Trapdoor}$ formulas (Sect. 4.3) are hard only for $\texttt{QCDCL}$, and the $\texttt{Dep}\text {-}\texttt{Trap}$ formulas (Sect. 4.4) are easy only in $\texttt{QCDCL}$. Hence $\texttt{QCDCL}$ is incomparable with all three systems obtained by adding $\texttt{D}^{\texttt{rrs}}$.

Among the three systems using $\texttt{D}^{\texttt{rrs}}$, the $\texttt{TwoPHPandCT}$ formulas (Sect. 4.5) are hard only in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, while the $\texttt{PreDepTrap}$ formulas (Sect. 4.7) are easy only in ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$. Hence ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ is incomparable with the systems that use preprocessing.

Finally, the systems $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ are separated by the formulas $\texttt{RRSTrapEq}$ (Sect. 4.6) easy only in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, and the formulas $\texttt{PropDep}\text {-}\texttt{Trap}$ (Sect. 4.8) easy only in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$. $\square$

Next we observe that each of the three new versions of $\texttt{QCDCL}$ is also incomparable with ${\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}$, $\texttt{Q}\text {-}{\texttt{Res}}$, $\texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}$, and $\texttt{QU}\text {-}{\texttt{Res}}$.

Theorem 5

Any two proof systems $\texttt{P}_1 \in \{ {\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}}), \texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}, \texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})\}$, and $\texttt{P}_2 \in \{ {{\texttt{QCDCL}}^{\texttt{LEV}\text {-}\texttt{ORD}}_{\mathtt {NO\text {-}RED}}}, \texttt{Q}\text {-}{\texttt{Res}}, \texttt{Q}(\texttt{D}^{\texttt{rrs}})\text {-}{\texttt{Res}}, \texttt{QU}\text {-}{\texttt{Res}}\}$, are incomparable.

Proof

The $\texttt{QParity}$ formulas (Sect. 4.1) require exponential size refutations in $\texttt{P}_2$ but have polynomial size refutations in $\texttt{P}_1$.

The $\texttt{Dep}\text {-}\texttt{Trap}$ formulas (Sect. 4.4) have constant size refutations in $\texttt{P}_2$ but require exponential size refutations in $\texttt{P}_1$. $\square$

Finally, we observe that even when we add cube-learning to standard $\texttt{QCDCL}$, the system ${\texttt{QCDCL}}^{\texttt{cube}}$ is still incomparable with all the three versions of $\texttt{QCDCL}$ with dependency scheme added.

Theorem 6

Every proof system in $\{ {\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}}), \texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}, \texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})\}$ is incomparable with ${\texttt{QCDCL}}^{\texttt{cube}}$.

Proof

The $\texttt{TwinEq}$ formulas (Sect. 4.9) require exponential size refutations in ${\texttt{QCDCL}}^{\texttt{cube}}$ but have poly-size refutations in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$.

The $\texttt{Dep}\text {-}\texttt{Trap}$ formulas (Sect. 4.4) require exponential size refutations in $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}$, ${\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$ and $\texttt{D}^{\texttt{rrs}}+{\texttt{QCDCL}}(\texttt{D}^{\texttt{rrs}})$, but have short refutations in ${\texttt{QCDCL}}^{\texttt{cube}}$. $\square$

6 Conclusion

We have examined, from a rigourous proof-theoretic viewpoint, the effect of incorporating heuristics based on dependency schemes into QBF solving algorithms based on the conflict-driven clause learning paradigm. Our results show that unlike in the case of the proof system $\texttt{Q}\text {-}{\texttt{Res}}$, where dependency-awareness can shorten but never lengthens refutations, here the picture is much more nuanced, and all kinds of shortenings as well as lengthenings can be observed. Thus the decision of whether or not to make a $\texttt{QCDCL}$ solver account for spurious dependencies is itself a challenging one, and it is likely the domain from where instances are to be solved may indicate what choice is more suitable.

The solver DepQBF uses $\texttt{D}^{\texttt{std}}$ rather than $\texttt{D}^{\texttt{rrs}}$, for decisions and reductions. As far as we are aware, no existing solver uses $\texttt{D}^{\texttt{rrs}}$ with $\texttt{QCDCL}$ in the manner we have introduced. The prepocessor HQSpre [26] does use $\texttt{D}^{\texttt{rrs}}$ in preprocessing but not beyond that. It would be interesting to see how a solver working on these principles would fare against current solvers. The trade-off between the power of $\texttt{D}^{\texttt{rrs}}$ and the restriction of $\texttt{LEV}\text {-}\texttt{ORD}$ would be interesting to observe. Additionally, if $\texttt{D}^{\texttt{rrs}}$ is used instead of $\texttt{D}^{\texttt{std}}$ in DepQBF, the difference in performance would be of interest.

One aspect which is unresolved in our work is the nature of our upper bounds. Since $\texttt{QCDCL}$ is not in itself an algorithm but a template, there are multiple instantiations of it based on the choice of decision heuristics, propagation policy, and learning scheme. We have restricted ourselves here to the decision heuristic and propagation policy used in most state-of-the-art solvers, namely, level-ordered decisions and propagations with reductions. However, we have not specified the learning scheme. Our lower bounds hold for any $\texttt{QCDCL}$-based solver as long as the learning scheme picks a clause only from the learnable-clause sequence as defined in Sect. 2. However, the upper bounds hold for specific choices of learnt clauses, and this, in some sense, reflects a certain non-determinism in the algorithm. (This is somewhat akin to the non-determinism inherent in $\texttt{CDCL}$ algorithms in the statement that $\texttt{CDCL}$ simulates Resolution.) Arguably, the upper bounds will be more meaningful if achieved with actually-used learning schemes. While some of our upper bounds are achieved with such schemes, specifically the UIP policy, some others make ad hoc choices with respect to which clauses to learn. Thus the impact of the learning scheme itself is still improperly understood for dependency-aware $\texttt{QCDCL}$.

In this work, we only consider decisions in $\texttt{LEV}\text {-}\texttt{ORD}$. Whether incorporating dependency schemes in the decision policy itself makes a difference or not is an interesting question. As recent work in [12] shows, other orders are not necessarily unsound, so this can still be meaningful. Formalisation seems tricky as we would like to retain the use of dependency schemes and long-distance resolution in the learning process, while also using dependency schemes in the decision policy and the propagations. The use of most dependency schemes is not yet known to be sound for long-distance cube resolution. (See the Discussion section in [20].) Although in this work we have not considered cube learning, cube learning and cube resolution is implemented in most solvers and so this issue cannot be completely side-stepped. One way out is to disallow long-distance steps when using dependency schemes. This makes proving completeness challenging. Another way is to disallow long-distance only while learning cubes, not clauses. This is a direction worth exploring.

There is also the dependency-learning setup which is quite different: the solver starts off assuming there are no dependencies, and gradually builds up a set of dependencies. (That is, add required dependencies starting from $\emptyset$, rather than remove spurious dependencies starting from $\texttt{D}^{\texttt{trv}}$.) In this approach, explored in [19] and used in the QBF solver Qute, learning dependencies does affect decision order. An in-depth future comparison of these two approaches could be interesting to explore.

Another aspect we have not directly addressed, other than showing soundness and completeness, is the effect of dependency schemes other than $\texttt{D}^{\texttt{rrs}}$. Since $\texttt{D}^{\texttt{rrs}}$ is a well-studied dependency scheme, known to be polytime-computable and for which $\texttt{LDQ}(\texttt{D})\text {-}{\texttt{Res}}$ is known to be sound, this makes it an important candidate whose effects need to be understood first. But there are other schemes: the less (than $\texttt{D}^{\texttt{rrs}}$) general standard dependency scheme $\texttt{D}^{\texttt{std}}$ introduced in [22] and used in DepQBF [16], and more general schemes based on tautology-free and implication-free paths introduced in [7, 8]. It seems reasonable to expect that a similar nuanced picture will present when considering such schemes as well.

Finally, an aspect to our work that is also interesting to investigate, with potential ramifications to practical solvers, is exploring the addition of cube-learning to our dependency-aware QCDCL systems. (As mentioned earlier, all solvers implement cube learning since it is essential for verifying true formulas.) This may be somewhat non-trivial and nuanced, as adding dependency schemes to the formal proof system of long-distance term resolution (the proof system in which proofs can be extracted from runs of solvers on true QBFs, Q-consensus) is not known to be sound (see the Discussion section in [20]).