On the Interplay of Cube Learning and Dependency Schemes in QCDCL Proof Systems

In Section 2, we give some basic definitions and describe, in a high-level informal way, the background about known proof systems and dependency schemes. In Section 3, we define the new proof systems, show soundness and completeness, and show that the decision policy $𝙳\text{-}\mathrm{𝙾𝚁𝙳}$ is strictly more powerful than $\mathrm{𝙻𝙴𝚅}\text{-}\mathrm{𝙾𝚁𝙳}$. In Section 4, we briefly discuss preprocessing, we define three new QBF families and show various lower and upper bounds for their proof sizes, and we describe the simulation order among various $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ systems. We conclude with some pointers for further directions of interest. Detailed definitions from prior work, as well as detailed proofs of many new results, appear in the full version of this paper [17].

We assume familiarity with basic concepts from logic and computational complexity: Boolean variables and literals, clauses and cubes/terms, conjunctive normal form (CNF), substitutions, etc. We follow notation from [7, 15]; see also [5]. Selected relevant items are included here.

A literal $\mathrm{\ell }$ is a Boolean variable $x$ or its negation $\overline{x}$, and $\mathrm{𝚟𝚊𝚛}(\mathrm{\ell })$ denotes the associated variable $x$. For a set $S$ of clauses and a literal $\mathrm{\ell }$, we use shorthand $\mathrm{\ell }\vee S$ to denote the set of clauses $\{\mathrm{\ell }\vee C\mid C\in S\}$. The empty clause, denoted $\mathrm{\square }$, is unsatisfiable; the empty cube, denoted $\top$, is always true. A clause (cube) is said to be tautological (contradictory) if for some variable $x$ it contains both $x$ and $\overline{x}$. The resolution rule can be applied to clauses and to cubes. The resolvent of clauses $A^{\prime }=A\vee x$ and $B^{\prime }=B\vee \overline{x}$ is the clause $A\vee B$ denoted as $\mathrm{𝚛𝚎𝚜}(A^{\prime },B^{\prime },x)$ or $\mathrm{𝚛𝚎𝚜}(B^{\prime },A^{\prime },x)$. The resolvent of cubes $A^{\prime }=A\wedge x$ and $B^{\prime }=B\wedge \overline{x}$ is the cube $A\wedge B$, also denoted as $\mathrm{𝚛𝚎𝚜}(A^{\prime },B^{\prime },x)$ or $\mathrm{𝚛𝚎𝚜}(B^{\prime },A^{\prime },x)$.

A Quantified Boolean Formula (QBF) in prenex conjunction normal form (PCNF) is a prefix with a list of variables, each quantified either existentially or universally, and a matrix, which is a set (conjunction) of clauses over these variables. That is, it has the form $\mathrm{\Phi }=𝒬\overrightarrow{x}\cdot \phi =Q_1{x}_1{Q}_2{x}_2\mathrm{\dots }{Q}_n{x}_n\phi (x_1,x_2,\mathrm{\dots },x_n)$ where $\phi$ is a propositional formula in CNF, and each $Q_i$ is in $\{\exists ,\forall \}$. We denote by $X_{\exists }$ ($X_{\forall }$ respectively) the set of all variables quantified existentially (resp. universally). A QBF is true if for each variable $x_i\in X_{\exists }$, there exists a (Skolem) function $s_i$, depending only on variables $x_j\in X_{\forall }$ with , such that substituting these $s_i$ in $\phi$ yields a tautology. Similarly, the formula is false if for each variable $x_i\in X_{\forall }$, there is a (Herbrand) function $h_i$, depending only on variables $x_j\in X_{\exists }$ with , such that substituting $h_i$ in $\phi$ yields an unsatisfiable formula.

The propositional proof system Resolution certifies unsatisfiability of a propositional formula by adding clauses obtaining through resolution until the empty clause is added. This can be lifted to QBFs in many ways. One of the simplest ways is to use the resolution rule along with a universal reduction rule, that allows removing a universal literal $u$ or $\overline{u}$ from a clause if it is not ‘blocked; that is, the clause has no existential literals quantified after $u$ in the prefix. This gives rise to the system $\mathrm{𝚀𝚄}$-$\mathrm{𝚁𝚎𝚜}$; its restriction where resolution is allowed only on existential pivots is the system $𝚀$-$\mathrm{𝚁𝚎𝚜}$. The long-distance resolution rule generalises resolution by permitting seemingly useless universal tautological clauses under certain side-conditions, and gives rise to the system $\mathrm{𝙻𝙳𝚀}$-$\mathrm{𝚁𝚎𝚜}$ that generalises $𝚀$-$\mathrm{𝚁𝚎𝚜}$. Informally, in this system, a resolution on $x$ is permitted even if the resolvent ends up having $u$ and $\overline{u}$ for some universal variable $u$, provided $u$ is quantified to the right of $x$. The presence of $u$ and $\overline{u}$ together, often referred to as a merged literal $u^{\ast }$, is to be interpreted not as a tautology but as a place-holder for a partial strategy for $u$ depending on the value of the pivot $x$.

In direct analogy to $𝚀$-$\mathrm{𝚁𝚎𝚜}$ and $\mathrm{𝙻𝙳𝚀}$-$\mathrm{𝚁𝚎𝚜}$ are the proof systems $𝚀$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ and $\mathrm{𝙻𝙳𝚀}$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ for certifying truth. Here the resolution is performed on terms, or cubes, with universal pivots, and existential literals can be reduced from a term if not blocked by universal literals quantified after them. The goal is to derive the empty term. A key point of difference is at the start; since the QBF is in PCNF, there are no terms to begin with. The Axiom rule in these systems permits starting with any term that satisfies the matrix.

For formal definitions of these proof systems, see for instance, Figure 2 in [9] (for $𝚀$-$\mathrm{𝚁𝚎𝚜}$,$\mathrm{𝚀𝚄}$-$\mathrm{𝚁𝚎𝚜}$, $\mathrm{𝙻𝙳𝚀}$-$\mathrm{𝚁𝚎𝚜}$), Figure 2, in [29] (for $𝚀$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$).

The notion of blocking, used in the reduction rules, stems from the understanding that if variables $x,y$ are quantified differently with $y$ quantified after $x$, then the value of $y$ in a (counter)model may non-trivially depend on $x$. If there is no literal blocking $x$, then the satisfaction of the clause (falsification of cube) should not rely on the unblocked universal (resp. existential) $x$. The dependency scheme heuristic refines this further. If a syntactic examination of the clause-variable structure can reveal that $y$ does not really depend on $x$, even though it is quantified later, then $x$ can be reduced even in the presence of $y$. This can drive the process towards the empty clause/term faster. Dependency schemes do precisely this. They identify pairs $(x,y)$ where $x$ and $y$ are quantified differently and where $y$ can be safely assumed to be independent of $x$. (Actually, they list pairs where $y$ may depend on $x$; the other pairs can be assumed to be independent.) The trivial dependency scheme associates with each QBF $\mathrm{\Phi }$ the dependency set ${𝙳}^{\mathrm{𝚝𝚛𝚟}}(\mathrm{\Phi })=\{(x,y)\mid y\text{ is quantifed after, and differently from, }x\}$. Other schemes can associate subsets of this set. The schemes relevant to this paper are the standard scheme ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$ (see Def 7 in [26] and Def 9 in [29]), and the reflexive resolution scheme ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ (see Defs 3,4,6 in [29]). For every $\mathrm{\Phi }$, ${𝙳}^{\mathrm{𝚝𝚛𝚟}}(\mathrm{\Phi })\supseteq {𝙳}^{\mathrm{𝚜𝚝𝚍}}(\mathrm{\Phi })\supseteq {𝙳}^{\mathrm{𝚛𝚛𝚜}}(\mathrm{\Phi })$.

When a dependency scheme $D$ is incorporated into any of the preceding proof systems, the reduction rule becomes more generally applicable, and the side-conditions concerning merged literals also become more permissive. This gives rise to the proof systems $𝚀(𝙳)$-$\mathrm{𝚁𝚎𝚜}$, $\mathrm{𝙻𝙳𝚀}(𝙳)$-$\mathrm{𝚁𝚎𝚜}$, $𝚀(𝙳)$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$, $\mathrm{𝙻𝙳𝚀}(𝙳)$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$. See, for instance, Figure 3 and Section 3.3 in [29] (for $𝚀$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ and $𝙳$-reductions), and Figure 1 in [24] (for $\mathrm{𝙻𝙳𝚀}(𝙳)$-$\mathrm{𝚁𝚎𝚜}$). For a clause and a dependency scheme $𝙳$, we denote by $\mathrm{𝚛𝚎𝚍}\text{-}𝙳(C)$ the clause obtained by removing all unblocked universal literals from $C$. Similarly, for a cube $C$, $\mathrm{𝚛𝚎𝚍}\text{-}{𝙳}_{\exists }(C)$ denotes the cube obtained by removing all unblocked existential literals from $C$.

An important subclass of dependency schemes are the so-called normal dependency schemes, which have the property of being “monotone” and “simple”. See Def. 7 in [24] for the precise definition. The dependency schemes ${𝙳}^{\mathrm{𝚝𝚛𝚟}}$, ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$, ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ are all normal. This class of schemes is of interest to us because it is known that for normal dependency schemes, $𝚀(𝙳)$-$\mathrm{𝚁𝚎𝚜}$ and $\mathrm{𝙻𝙳𝚀}(𝙳)$-$\mathrm{𝚁𝚎𝚜}$ are sound and refutationally complete [24]. The system $𝚀(𝙳)$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ is known to be sound and complete on true formulas for $𝙳\in \{{𝙳}^{\mathrm{𝚝𝚛𝚟}},{𝙳}^{\mathrm{𝚛𝚛𝚜}}\}$ (in [29], soundness is shown for a stronger dependency scheme, ${𝙳}^{\mathrm{𝚛𝚎𝚜}}$, implying soundness for ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ as well). However the soundness of $\mathrm{𝙻𝙳𝚀}(𝙳)$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ is not known for dependency schemes other than ${𝙳}^{\mathrm{𝚝𝚛𝚟}}$.

We say proof system ${𝙿}_1$ simulates a proof system ${𝙿}_2$ if some computable function transforms proofs in ${𝙿}_2$ into proofs in ${𝙿}_1$ with at most polynomial blow-up in proof size. If this function is also computable in polynomial time (in the given proof size), we say that ${𝙿}_1$ $p$-simulates ${𝙿}_2$. Two systems are said to be incomparable if neither simulates the other.

By definition $\mathrm{𝙻𝙳𝚀}(𝙳)$-$\mathrm{𝚁𝚎𝚜}$ $p$-simulates $\mathrm{𝙻𝙳𝚀}$-$\mathrm{𝚁𝚎𝚜}$ and $𝚀(𝙳)$-$\mathrm{𝚁𝚎𝚜}$, both of which $p$-simulate $𝚀$-$\mathrm{𝚁𝚎𝚜}$. Similarly, both $\mathrm{𝙻𝙳𝚀}$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ and $𝚀(𝙳)$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$ $p$-simulate $𝚀$-$\mathrm{𝚃𝚎𝚛𝚖𝚁𝚎𝚜}$. It is also known that $𝚀(𝙳)$-$\mathrm{𝚁𝚎𝚜}$ is exponentially stronger than $𝚀$-$\mathrm{𝚁𝚎𝚜}$ for $𝙳={𝙳}^{\mathrm{𝚛𝚛𝚜}}$; [10, 11].

The proof system for $\mathrm{𝚀𝙲𝙳𝙲𝙻}$, as defined in [7], formalizes reasoning in QCDCL algorithms operating on false formulas without cube learning. These algorithms construct trails or partial assignments in a specific way – decide values of variables according to some policy, propagate values of existential variables that appear in clauses which become unit after restriction by the trail so far and by universal reduction (call such a clause the antecedent of the propagated literal) – trying to satisfy the matrix. If a conflict is reached, then the trail is inconsistent with any Skolem function. Conflict analysis is performed, and a new clause is learnt and added to the matrix. If the empty clause is learned, the formula is deemed false. The corresponding refutation in the proof system $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ consists of the sequence of constructed trails, and for each trail the sequence of long-distance resolution steps performed in conflict analysis to learn a clause. The full definition can be found in [7] (Def. 3.5).

The above formulation of the $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ system only considers 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. However, from satisfying assignments, solvers can and do learn cubes (or terms), and this is necessary to prove true QBFs true. In [15] it was shown that even while refuting false QBFs, allowing cube learning from satisfying assignments can be advantageous. This led to the definition of the proof system ${\mathrm{𝚀𝙲𝙳𝙲𝙻}}^{\mathrm{𝚌𝚞𝚋𝚎}}$, and in [15], it was shown to be strictly stronger than the standard $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ system. The main idea in cube learning systems is to consider satisfying assignments also as conflicts, albeit of a different kind, and to learn cubes from these conflicts. (The algorithm learns that such a trail is inconsistent with any Herbrand function.) Learnt cubes are added disjunctively to the matrix, which thus at intermediate stages is not necessarily in CNF but is the disjunction of a CNF formula and some cubes. With the augmented CNF matrices, cubes that become unit after existential reduction can now propagate universal variables in a way that falsifies the cube. Also, with the augmented CNF matrices, a trail may end up satisfying a cube rather than the CNF; this too is now a conflict, and conflict analysis involving term-resolution can be performed to learn a new cube. For formal details, see Section 3 in [15].

The $\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢}$ formulas, first defined in [6], show that the proof system $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ with cube learning is stronger than $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ without [15]. We wish to show that cube-learning offers a similar advantage for systems with ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$. The $\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢}$ formulas cannot show this because ${𝙳}^{\mathrm{𝚛𝚛𝚜}}(\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢})=\mathrm{\varnothing }$; so using ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ in any way makes them easy to refute irrespective of cube-learning. To achieve the desired separation, we modify the $\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢}$ formula by adding two clauses that make ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ and ${𝙳}^{\mathrm{𝚝𝚛𝚟}}$ identical. These new formulas, called $\mathrm{𝙳𝚘𝚞𝚋𝚕𝚎𝙻𝚘𝚗𝚐𝙴𝚚}$, maintain the separation without altering the hardness of $\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢}$.

(Note: deleting the clauses $U{T}_n$ and $U{T}_n^{\prime }$ gives the $\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢}$ formulas.)

This makes the usage of the dependency schemes ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ or ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$ completely useless. We now show that the formulas are easy to refute with cube-learning, but hard if cube-learning is switched off. Both these results closely mirror the corresponding results for $\mathrm{𝙴𝚚𝚞𝚊𝚕𝚒𝚝𝚢}$ shown in [7] and [15] respectively.

The next formula is designed to explore how adding ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ in different ways affects the system. It sends $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ trails into a “trap” (of refuting the hard existential Pigeonhole Principle $\mathrm{𝙿𝙷𝙿}$; see Example 3.6) if ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ is not used in propagation, but allows a short refutation (a contradiction on two variables) when ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ is used. This leads to the definition of a formula inspired by the $\mathrm{𝚃𝚛𝚊𝚙𝚍𝚘𝚘𝚛}$ and $\mathrm{𝙳𝚎𝚙}\text{-}\mathrm{𝚃𝚛𝚊𝚙}$ formulas from [7](Def. 4.5) and [16](Def. 4.4) respectively.

This formula has an unsatisfiable matrix (due to the presence of $\mathrm{𝙿𝙷𝙿}$).

The variable “$w$” is not necessary for the lower or upper bounds proved for this formula. Initialising ${\mathrm{𝙿𝚛𝚎𝚁𝚁𝚂𝚃𝚛𝚊𝚙𝚍𝚘𝚘𝚛}|}_{w=0}$ or removing the variable “$w$” entirely affects neither the bounds nor their proofs. However we keep it in because the $\mathrm{𝙿𝚛𝚎𝚁𝚁𝚂𝚃𝚛𝚊𝚙𝚍𝚘𝚘𝚛}$ formulas are defined to extend the $\mathrm{𝚃𝚛𝚊𝚙𝚍𝚘𝚘𝚛}$ formula (defined in [7]) which has the “$w$” variable. Also, it shows that even if the preprocessing step (by ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$) is non-trivial and changes the formula, addition of ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ in propagation can still make a difference.

Hence $\mathrm{𝚛𝚎𝚍}\text{-}{𝙳}^{\mathrm{𝚛𝚛𝚜}}(\mathrm{𝙿𝚛𝚎𝚁𝚁𝚂𝚃𝚛𝚊𝚙𝚍𝚘𝚘𝚛})$= ${\mathrm{𝙿𝚛𝚎𝚁𝚁𝚂𝚃𝚛𝚊𝚙𝚍𝚘𝚘𝚛}|}_{w=0}$. That is, if we preprocess using ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$, everything stays the same except that the variable $w$ “disappears”.

However, just preprocessing by ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ is not enough to make this formula easy to refute. The following lemmas shows that the presence of ${𝙳}^{\mathrm{𝚛𝚛𝚜}}$ during propagation is crucial to achieving polynomial sized refutations; its absence forces exponential size.

The third new formula $\mathrm{𝚂𝚝𝚍𝙳𝚎𝚙𝚃𝚛𝚊𝚙}$ we introduce shows the advantage of using ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$ in propagation and learning. The goal is to create clauses that can be learnt easily with ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$, but are hard to learn without it. These learned clauses enable a quick refutation in $\mathrm{𝚀𝙲𝙳𝙲𝙻}$ with ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$, but without them, one is stuck refuting something hard.

The variables $w_1,w_2,u$ are essentially “separators”, putting existential variables into different levels. The variables $e_1,e_2,x$ are blockers, ensuring that the separators do not get reduced too early in the trail.

When ${𝙳}^{\mathrm{𝚜𝚝𝚍}}$ is used in propagation, we show that these formulas have short refutations.