5 Clause Learning and General Resolution

We begin this section by showing that CL proofs, irrespective of the learning scheme, branching strategy, or restarts used, can be efficiently simulated by RES. In the reverse direction, we show that CL, with a slight variation and with unlimited restarts, can efficiently simulate RES in its full generality. The variation relates to the variables one is allowed to branch upon.

Lemma 3   For any formula F over n variables and CL using any learning scheme and any number of restarts, $\mathcal {C}$_{$\mathsf {\scriptstyle RES}$}(F)$\le$n ^. $\mathcal {C}$_{$\mathsf {\scriptstyle CL}$}(F).

Proof. Given a CL proof $\pi$ of F, a RES proof can be constructed by sequentially deriving all clauses that $\pi$ learns, which includes the empty clause $\Lambda$. From Proposition 4, all these derivations are trivial and hence require at most n steps each. Consequently, the size of the resulting RES proof is at most n ^. size($\pi$). Note that since we derive clauses of $\pi$ individually, restarts in $\pi$ do not affect the construction.$\Box$

Definition 13   Let CL- denote the variation of CL where one is allowed to branch on a literal whose value is already set explicitly or because of unit propagation.

Of course, such a relaxation is useless in ordinary DPLL; there is no benefit in branching on a variable that doesn't even appear in the residual formula. However, with clause learning, such a branch can lead to an immediate conflict and allow one to learn a key conflict clause that would otherwise have not been learned. We will use this property to show that RES can be efficiently simulated by CL- with enough restarts.

We first state a generalization of Lemma 3. CL- can, by definition, do all that usual CL can, and is potentially stronger. The simulation of CL by RES can in fact be extended to CL- as well. The proof goes exactly as the proof of Lemma 3 and uses the easy fact that Proposition 4 doesn't change even when one is allowed to branch on variables that are already set. This gives us:

Proposition 5   For any formula F over n variables and CL- using any learning scheme and any number of restarts, $\mathcal {C}$_{$\mathsf {\scriptstyle RES}$}(F)$\le$n ^. $\mathcal {C}$_{$\mathsf {\scriptstyle CL\mbox{{-}-}}$}(F).

Lemma 4   For any formula F over n variables and CL using any non-redundant scheme and at most $\mathcal {C}$_{$\mathsf {\scriptstyle RES}$}(F) restarts, $\mathcal {C}$_{$\mathsf {\scriptstyle CL\mbox{{-}-}}$}(F)$\le$n ^. $\mathcal {C}$_{$\mathsf {\scriptstyle RES}$}(F).

Proof. Let $\pi$ be a RES proof of F of size s. Assume without loss of generality as in the proof of Lemma 1 that $\pi$ does not contain a derived clause C_i whose strict subclause C'_i can be derived by resolving two clauses occurring previously in $\pi$. The proof of this Lemma is very similar to that of Lemma 1. However, since we do not have trace variable to allow us to simulate each resolution step individually and independently, we use explicit restarts.

Viewing $\pi$ as a sequence of clauses, its last two elements must be a literal, say v, and $\Lambda$. Let S = $\pi$ $\setminus$ (F $\cup$ {v,$\Lambda$}). Let (C₁, C₂,..., C_k) be the subsequence of $\pi$ that has precisely the clauses in S. Note that C_i $\equiv$ $\neg$v for some i, 1$\le$i$\le$k. For convenience, define an extended branching sequence to be a branching sequence in which certain places, instead of being literals, can be marked as restart points. Let $\sigma$ be the extended branching sequence consisting of all literals of C₁, followed by a restart point, followed by all literals of C₂, followed by a second restart point, and so on up to C_k. We claim that $\sigma$ induces a CL- proof of F using any non-redundant learning scheme. To prove this, we show by induction that after the i^th restart point in $\sigma$, the CL- procedure has learned clauses C₁, C₂,..., C_i and is at decision level zero.

The base case for induction, i = 0, is trivial. No clauses have been learned and the clause learning procedure is at decision level zero. Suppose the inductive claim holds after the (i - 1)^st restart point in $\sigma$. Let C_i = (x₁ $\vee$ x₂ $\vee$...$\vee$ x_l). C_i must have been derived in $\pi$ by resolving two clauses (A $\vee$ y) and (B $\vee$ $\neg$y) coming from F $\cup$ {C₁, C₂,..., C_i-1}, where C_i = (A $\vee$ B). Continuing to branch according to $\sigma$ till before the i^th restart point makes the CL- procedure set all if x₁, x₂,..., x_l to FALSE. Note that when all literals appearing in A and B are distinct, the last branch on x_l here is on a variable that is already set because of unit propagation. CL-, however, allows this. At this stage, unit propagation using (A $\vee$ y) and (B $\vee$ $\neg$y) implies y as well as $\neg$y, leading to a conflict. The conflict graph consists of $\neg$x_j's, 1$\le$j$\le$l, as the decision literals, y and $\neg$y as implied literals, and $\Lambda$. The only new conflict clause that can learned from this very simple conflict graph is C_i. Thus, C_i is learned using any non-redundant learning scheme and the i^th restart executed, as dictated by $\sigma$. At this stage, the CL- procedure has learned clauses C₁, C₂,..., C_i, and is at decision level zero. This completes the inductive step.

The inductive proof above shows that when the CL- procedure has finished with the k^th restart in $\sigma$, it will have learned all clauses in S. Adding to this the initial clauses F that are already known, the procedure will have as known clauses $\neg$v as well as the two unit or binary clauses used to derive v in $\pi$. These immediately generate $\Lambda$ in the residual formula by unit propagation using variable v, leading to a conflict at decision level zero, thereby concluding the clause learning procedure and finishing the CL- proof. The bounds on the size of this proof and the number of restarts needed immediately follow from the definition of $\sigma$.$\Box$

Combining Lemma 4 with Proposition 5, we get

Theorem 2   CL- with any non-redundant scheme and unlimited restarts is polynomially equivalent to RES.

Note that Baptista and Silva (2000) showed that CL together with restarts is complete. Our theorem makes a much stronger claim about a slight variation of CL, namely, with enough restarts, this variation can always find proofs that are as short as those of RES.