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.
Proof. Let = (C1, C2,..., Ck C) be a trivial resolution derivation of C from F. Let Ck = (l1 l2 ... lq) and be the partial assignment that sets all li, 1iq, to FALSE. Assume without loss of generality that clauses in are ordered so that all initial clauses precede any derived clause. We give a proof by induction on the number of derived clauses in .
For the base case, has only one derived clause, C Ck, Assume without loss of generality that Ck = (A B) and Ck is derived by resolving two initial clauses (A x) and (B x) on variable x. Since falsifies Ck, it falsifies all literals of A, implying x = TRUE by unit propagation. Similarly, falsifies B, implying x = FALSE and resulting in a conflict.
When has at least two derived clauses, Ck, by triviality of ,
must be derived by resolving
Ck-1 F with a clause in F. Assume
without loss of generality that
Ck-1 (A x) and the
clause from F used in this resolution step is
(B x),
where
Ck = (A B). Since falsifies
C Ck, it
falsifies all literals of B, implying x = FALSE by unit
propagation. This in turn results in falsifying all literals of
Ck-1 because all literals of A are also set to FALSE by
. Now
(C1,..., Ck-1) is a trivial resolution
derivation of
Ck-1 F from F with one less derived clause than
, and all literals of Ck-1 are falsified. By induction, this
must lead to a conflict by unit propagation.
Proof. Let be the cut in a fixed conflict graph associated with the given conflict clause. Let Vconflict() denote the set of variables on the conflict side of , but including the conflict variable only if it occurs both positively and negatively on the conflict side. We will prove by induction on | Vconflict()| the stronger statement that the conflict clause associated with a cut has a trivial derivation from known (i.e. initial or previously derived) clauses resolving precisely on the variables in Vconflict().
For the base case, Vconflict() = and the conflict side contains only and a conflict literal, say x. The cause associated with this cut consists of node x that has an edge to , and nodes l1,l2,...,lk, corresponding to a known clause Cx = (l1 l2 ... lk x), that each have an edge to x. The conflict clause for this cut is simply the known clause Cx itself, having a length zero trivial derivation.
|
When
Vconflict(), 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 = (l1 l2 ... lp) and assume without loss
of generality that the predecessors of y are
l1,l2,...,lk for some kp. By definition of unit
propagation,
Cy = (l1 l2 ... lk y) must
be a known clause. Obtain a new cut from by moving
node y from the conflict side to the reason side. The new associated
conflict clause must be of the form
C' = (y D), where D
is a subclause of C. Now
Vconflict() Vconflict(). Consequently, by induction, C' must have a
trivial resolution derivation from known clauses resolving precisely
upon the variables in
Vconflict(). Recall that no variable
occurs twice in a conflict graph except the conflict variable. Hence
Vconflict() has exactly all variables of
Vconflict() other than y. Using this trivial derivation
of C' and finally resolving C' with the known clause Cy on
variable y gives us a trivial derivation of C from known
clauses. This completes the inductive step.