TAOCP 7.2.2.2 Exercise 274
Algorithm C maintains a trail of literals that have been assigned by decisions or by unit propagation.
Section 7.2.2.2: Satisfiability
Exercise 274. [35] Algorithm C sets the "reason" for a literal $l$ as soon as it notices a clause that forces $l$ to be true. Later on, other clauses that force $l$ are often encountered, in practice; but Algorithm C ignores them, even though one of them might be a "better reason." (For example, another forcing clause might be significantly shorter.) Explore a modification of Algorithm C that tries to improve the reasons of non-decision literals.
Verified: yes
Solve time: 3m20s
Setup
Algorithm C maintains a trail of literals that have been assigned by decisions or by unit propagation. Every non-decision literal $l$ on the trail has a stored reason clause $R(l)$, namely a clause that was unit at the time $l$ was assigned and whose remaining unassigned literal was $l$. Thus $R(l)$ contains $l$, and every other literal of $R(l)$ was false when $l$ was propagated.
The exercise asks for a modification of Algorithm C that improves the reasons of non-decision literals when additional forcing clauses are encountered later. The modification must preserve the invariant that every stored reason is a valid explanation of the corresponding propagation step.
The difficulty is that a clause which forces $l$ under the current trail need not have been responsible for the earlier assignment of $l$. A valid replacement reason must therefore satisfy a temporal condition.
Let the trail position of a literal $l$ be the moment when $l$ was assigned. A clause $C$ is an admissible replacement reason for $l$ if $C$ contains $l$ and all literals of $C-{l}$ were false at the trail position of $l$. Equivalently, $C$ was unit at the time when $l$ was propagated. Such a clause gives a valid implication edge ending at $l$ in the implication graph.
Solution
Modify the propagation part of Algorithm C as follows. Whenever Algorithm C finds a clause $C$ that becomes unit and forces a literal $l$, it first performs the ordinary propagation if $l$ is currently unassigned. The algorithm assigns $l$ and stores
$$ R(l)\leftarrow C . $$
This is the original behavior of Algorithm C.
The modification concerns later encounters with clauses that could also explain $l$. Suppose $l$ is already assigned and is not a decision literal. When a clause $C$ containing $l$ is encountered, Algorithm C tests whether $C$ is an admissible replacement reason for $l$. If $C$ was not unit at the trail position of $l$, it is ignored as a reason candidate. If $C$ was unit at that position, then $C$ is a valid alternative explanation for the same implication edge.
Among all admissible reasons encountered for $l$, the algorithm keeps the one that minimizes a chosen quality measure. The simplest choice is clause length. Define
$$ C_1\prec C_2 $$
if
$$ |C_1|<|C_2|, $$
where $|C|$ is the number of literals in $C$. When an admissible candidate $C$ is found, replace the current reason exactly when
$$ C\prec R(l). $$
The modified rule is therefore
$$ R(l)\leftarrow C $$
only if both conditions hold: $C$ was unit when $l$ was propagated, and $C\prec R(l)$.
The reason for requiring the first condition is that the reason data structure represents the implication graph, not merely a clause that happens to be satisfied by the current assignment. A clause discovered later may depend on literals that were assigned after $l$. Such a clause explains a consequence of the current trail, but it does not explain the earlier propagation of $l$ and cannot replace $R(l)$.
The replacement is safe because both the old reason and the new reason describe valid implication edges. At the time of $l$'s assignment, the clause $R(l)$ had all literals other than $l$ false. The candidate clause $C$ has the same property. Therefore both clauses imply that $l$ must be true under the partial assignment existing at that trail position. Replacing one by the other preserves the meaning of the implication graph.
The choice of clause length is only a heuristic. A more refined score may depend on the variables appearing in the clause and their decision levels. For example, one may define a score $s(C)$ and replace $R(l)$ by $C$ whenever
$$ s(C)<s(R(l)). $$
A useful score can favor clauses with fewer literals, fewer literals from the current decision level, or higher activity. The correctness condition remains unchanged: only clauses that were valid reasons at the propagation point of $l$ may compete for replacement.
The modification affects only reason storage. The assignments produced by the search are unchanged because propagation still occurs exactly when a clause becomes unit. The only difference is which valid explanation is retained for a literal already assigned.
The modification must not change a reason while a conflict is being analyzed. During conflict analysis, Algorithm C may follow reason pointers from literals on the trail. Therefore reason replacement is performed only during the ordinary propagation phase before conflict analysis begins. Once conflict analysis starts, all reason pointers used in that analysis remain fixed.
The resulting algorithm has the following behavior. A literal $l$ receives its first valid reason when it is propagated. Later propagations may discover additional valid reasons for $l$. Each such reason is compared with the stored reason, and the better one replaces it. The trail itself is unchanged, while the implication graph is improved.
The benefit appears during conflict analysis. Suppose the current conflict clause contains $\bar l$. Resolution with the reason of $l$ replaces $\bar l$ by the other literals of the reason clause. If the new reason has fewer literals, then this resolution step introduces fewer candidates into the learned clause. For two reasons $C_1$ and $C_2$ with
$$ |C_1|<|C_2|, $$
the number of literals introduced by resolving with them differs by
$$ (|C_2|-1)-(|C_1|-1)=|C_2|-|C_1|>0. $$
Thus a shorter admissible reason can reduce the size of intermediate resolvents. The reduction is not guaranteed for every conflict because the final learned clause also depends on decision levels and later resolution steps, but the modification gives Algorithm C a better implication graph on which to perform conflict analysis.
Verification
The reason invariant is preserved. Initially, every propagated literal receives a clause that was unit at the moment of propagation. The only later replacements allowed are clauses that satisfy the same property. Therefore every stored reason remains a clause that justifies the corresponding trail assignment.
The search space is unchanged. Decisions are selected exactly as before, and propagation assigns the same forced literals because the set of clauses is unchanged. Replacing $R(l)$ by another valid reason changes only the explanation of an already determined assignment.
Conflict analysis remains sound. Every resolution step uses either an original clause or a reason clause stored in the implication graph. Since every stored reason is an original clause that was unit when it implied its literal, it is a valid premise for resolution. Hence every learned clause remains a logical consequence of the original formula.
The modification cannot incorrectly install a clause that became unit only after $l$ was assigned. Such a clause fails the admissibility test because its other literals were not all false at the trail position of $l$. Therefore the principal danger in replacing reasons is excluded by construction.
The extra cost is limited. The propagation procedure already identifies clauses that become unit. For each such clause, the modified algorithm only checks whether the clause was unit at the propagation level of $l$ and, if so, compares its score with the stored reason. No additional search through the formula is required.
This completes the proof.
∎
Notes
The modification can be combined with clause-learning heuristics. A solver may prefer a reason that is not merely short but also produces favorable resolution behavior, for example by avoiding literals from the current conflict level or by using clauses with high activity.
Another implementation strategy is to keep a small number of admissible candidate reasons for each propagated literal and choose among them immediately before conflict analysis. The same validity condition applies: every retained candidate must have been a legitimate reason at the time of the literal's propagation.