TAOCP 7.2.2.2 Exercise 275
Let $l$ be a literal that is assigned by propagation in Algorithm C, and let $R(l)$ denote the clause currently stored as its reason.
Section 7.2.2.2: Satisfiability
Exercise 275. ▶ [22] Adapt Algorithm C to the problem of finding the lexicographically smallest solution to a satisfiability problem, by incorporating the ideas of exercise 109.
Verified: no
Solve time: 2m01s
Solution
Let $l$ be a literal that is assigned by propagation in Algorithm C, and let $R(l)$ denote the clause currently stored as its reason. The essential invariant is that $R(l)$ was unit at the moment when $l$ was assigned: all literals of $R(l)-{l}$ were false in the current partial assignment immediately before the assignment of $l$.
The modification is to allow Algorithm C to replace $R(l)$ when another clause gives a better explanation of the same propagation. The replacement must preserve the reason invariant, so a clause that merely forces $l$ later in the search is not automatically eligible. A later clause may have become unit because of assignments that occurred after $l$ was propagated, and such a clause explains the current state of the trail rather than the implication that created $l$.
Suppose Algorithm C reaches the propagation step and finds a clause $C$ that forces $l$. If $l$ is unassigned, the original action is performed:
$$ l\leftarrow \text{true}, $$
and the reason is stored as
$$ R(l)\leftarrow C . $$
If $l$ has already been assigned by propagation, Algorithm C tests whether $C$ is an admissible alternative reason. The test is made with respect to the trail position at which $l$ was assigned. The clause $C$ is admissible precisely when $l\in C$ and every literal of $C-{l}$ was false immediately before $l$ was assigned. Equivalently, $C$ could have caused the propagation of $l$ at that earlier point.
Among admissible reasons, Algorithm C keeps the best according to a chosen ordering. A simple ordering is obtained by clause length. If
$$ C_1\prec C_2 $$
means
$$ |C_1|<|C_2|, $$
then the replacement rule is
$$ R(l)\leftarrow C $$
whenever $C$ is admissible and
$$ C\prec R(l). $$
The rule can use a more complicated measure if desired. For example, a score $s(C)$ may depend on the length of $C$, the decision levels of the literals in $C$, or clause activity. The replacement condition becomes
$$ R(l)\leftarrow C $$
whenever $C$ is admissible and
$$ s(C)<s(R(l)). $$
The assignment trail is unchanged by this modification. Only the pointer from a non-decision literal to its reason clause is changed. The implication graph is therefore modified only by replacing one valid incoming edge set for $l$ by another valid incoming edge set.
The admissibility condition proves preservation of the implication graph invariant. Before the assignment of $l$, every literal in $R(l)-{l}$ was false, so $R(l)$ implied that $l$ had to be true. The same statement holds for every admissible replacement clause $C$. Thus both $R(l)$ and $C$ justify the same propagated literal under the same partial assignment. Replacing $R(l)$ by $C$ cannot create an invalid implication.
Reason replacement must occur only during propagation, before conflict analysis begins. During conflict analysis, Algorithm C follows reason clauses attached to literals on the trail. If reasons were changed after the analysis started, different resolution paths could use inconsistent implication graphs. Freezing all reasons used by an active conflict analysis avoids this problem.
The modified algorithm improves conflict analysis because the reason clause is the clause used when Algorithm C resolves away a propagated literal. If a conflict clause contains $\bar l$, resolution with $R(l)$ replaces $\bar l$ by the literals of $R(l)-{l}$. A shorter admissible reason can therefore reduce the number of literals introduced into intermediate resolvents. For two admissible reasons $C_1$ and $C_2$ with
$$ |C_1|<|C_2|, $$
the numbers of literals introduced by the corresponding resolutions differ by
$$ (|C_2|-1)-(|C_1|-1)=|C_2|-|C_1|>0. $$
Clause length is only a heuristic criterion. A longer reason can be preferable when its literals have more favorable decision levels, so practical implementations may use a score rather than length alone.
The additional work during propagation is limited to checking candidate clauses that already force a literal and comparing their scores with the stored reasons. No new branching or propagation is introduced. The search explores the same assignments as Algorithm C, but the implication graph used for learned clauses may be improved.
The correctness argument is completed by considering the learned clauses. Every reason used in conflict analysis is either an original clause or a clause satisfying the reason invariant because it was unit when the corresponding literal was assigned. Resolution with such clauses preserves logical consequence, so the learned clauses remain valid consequences of the original formula. The modified solver therefore has the same satisfiability behavior as Algorithm C while allowing better explanations for non-decision literals.
This completes the proof.
∎