3.5 Trivial Resolution and Learned Clauses

Definition 8   A resolution derivation (C₁, C₂,..., C_k) is trivial iff all variables resolved upon are distinct and each C_i, i$\ge$3, is either an initial clause or is derived by resolving C_i-1 with an initial clause.

A trivial derivation is tree-like, regular, linear, as well as ordered. As the following Propositions show, trivial derivations correspond to conflicts in clause learning algorithms.

Proposition 3   Let F be a CNF formula. If there is a trivial resolution derivation of a clause C $\notin$F from F then setting all literals of C to FALSE leads to a conflict by unit propagation.

Proof. Let $\pi$ = (C₁, C₂,..., C_k $\equiv$ C) be a trivial resolution derivation of C from F. Let C_k = (l₁ $\vee$ l₂ $\vee$...$\vee$ l_q) and $\rho$ be the partial assignment that sets all l_i, 1$\le$i$\le$q, to FALSE. Assume without loss of generality that clauses in $\pi$ are ordered so that all initial clauses precede any derived clause. We give a proof by induction on the number of derived clauses in $\pi$.

For the base case, $\pi$ has only one derived clause, C $\equiv$ C_k, Assume without loss of generality that C_k = (A $\vee$ B) and C_k is derived by resolving two initial clauses (A $\vee$ x) and (B $\vee$ $\neg$x) on variable x. Since $\rho$ falsifies C_k, it falsifies all literals of A, implying x = TRUE by unit propagation. Similarly, $\rho$ falsifies B, implying x = FALSE and resulting in a conflict.

When $\pi$ has at least two derived clauses, C_k, by triviality of $\pi$, must be derived by resolving C_k-1 $\notin$F with a clause in F. Assume without loss of generality that C_k-1 $\equiv$ (A $\vee$ x) and the clause from F used in this resolution step is (B $\vee$ $\neg$x), where C_k = (A $\vee$ B). Since $\rho$ falsifies C $\equiv$ C_k, it falsifies all literals of B, implying x = FALSE by unit propagation. This in turn results in falsifying all literals of C_k-1 because all literals of A are also set to FALSE by $\rho$. Now (C₁,..., C_k-1) is a trivial resolution derivation of C_k-1 $\notin$F from F with one less derived clause than $\pi$, and all literals of C_k-1 are falsified. By induction, this must lead to a conflict by unit propagation.$\Box$

Proposition 4   Any conflict clause can be derived from initial and previously derived clauses using a trivial resolution derivation.

Proof. Let $\sigma$ be the cut in a fixed conflict graph associated with the given conflict clause. Let V_conflict($\sigma$) denote the set of variables on the conflict side of $\sigma$, but including the conflict variable only if it occurs both positively and negatively on the conflict side. We will prove by induction on | V_conflict($\sigma$)| the stronger statement that the conflict clause associated with a cut $\sigma$ has a trivial derivation from known (i.e. initial or previously derived) clauses resolving precisely on the variables in V_conflict($\sigma$).

For the base case, V_conflict($\sigma$) = $\phi$ and the conflict side contains only $\Lambda$ and a conflict literal, say x. The cause associated with this cut consists of node $\neg$x that has an edge to $\Lambda$, and nodes $\neg$l₁,$\neg$l₂,...,$\neg$l_k, corresponding to a known clause C_x = (l₁ $\vee$ l₂ $\vee$...$\vee$ l_k $\vee$ x), that each have an edge to x. The conflict clause for this cut is simply the known clause C_x itself, having a length zero trivial derivation.

Figure 3: Deriving a conflict clause using trivial resolution. Resolving C' with C_y on variable y gives the conflict clause C.

When V_conflict($\sigma$)$\ne$$\phi$, pick a node y on the conflict side all whose predecessors are on the reason side (see Figure. 3). Let the conflict clause be C = (l₁ $\vee$ l₂ $\vee$...$\vee$ l_p) and assume without loss of generality that the predecessors of y are $\neg$l₁,$\neg$l₂,...,$\neg$l_k for some k$\le$p. By definition of unit propagation, C_y = (l₁ $\vee$ l₂ $\vee$...$\vee$ l_k $\vee$ y) must be a known clause. Obtain a new cut $\sigma{^\prime}$ from $\sigma$ by moving node y from the conflict side to the reason side. The new associated conflict clause must be of the form C' = ($\neg$y $\vee$ D), where D is a subclause of C. Now V_conflict($\sigma{^\prime}$) $\subset$ V_conflict($\sigma$). Consequently, by induction, C' must have a trivial resolution derivation from known clauses resolving precisely upon the variables in V_conflict($\sigma{^\prime}$). Recall that no variable occurs twice in a conflict graph except the conflict variable. Hence V_conflict($\sigma{^\prime}$) has exactly all variables of V_conflict($\sigma$) other than y. Using this trivial derivation of C' and finally resolving C' with the known clause C_y on variable y gives us a trivial derivation of C from known clauses. This completes the inductive step.$\Box$