TAOCP 7.2.2.2 Exercise 264
The purpose of the move codes is to expose the progress of Algorithm C without changing its behavior.
Section 7.2.2.2: Satisfiability
Exercise 264. [20] Suggest a way in which Algorithm C could indicate progress by displaying "move codes" analogous to those of Algorithms A, B, D, and L. (See exercise 142.)
Verified: no
Solve time: 2m50s
Solution
The purpose of the move codes is to expose the progress of Algorithm C without changing its behavior. The search process of Algorithm C consists of decisions in steps C6 through C8, followed by unit propagation in steps C3 and C4, and conflict analysis followed by backtracking when a contradiction is reached. A useful move-code system should therefore record the events that alter the search tree rather than the internal pointer operations of the watch lists.
A compact encoding is obtained by assigning one code to each kind of event that changes the current state of the search. The assignment of a literal at a decision level can be represented by a code containing the chosen variable and its polarity. Thus, when step C6 selects an unassigned variable $v$ and step C7 chooses a polarity, the move code can display either $v$ or $\bar v$ according to the value being tentatively assigned. The current depth of the search tree is the number of such decision codes that have not yet been undone.
The assignments forced by unit propagation in steps C3 and C4 can be distinguished from decisions by using a different prefix. If the clause causing the implication is $C$, the move code can display the literal $l$ forced by $C$ together with a marker indicating that $l$ was derived rather than chosen. This distinguishes a branch of the search tree from the deterministic consequences produced by that branch.
When step C8 detects a conflict, the move code can display a conflict symbol together with the clause responsible for the contradiction. The subsequent backtracking operation can be represented by a sequence of deletion codes that remove the trail entries made after the new backtracking level. If a learned clause is produced by step C7, a separate code can display its insertion and the literals that it contains.
A possible notation is therefore
$$ \begin{array}{c|c} \text{event} & \text{move code}\ \hline \text{decision assigning }v & Dv\ \text{decision assigning }\bar v & D\bar v\ \text{unit propagation assigning }v & Pv\ \text{unit propagation assigning }\bar v & P\bar v\ \text{conflict in clause }C & XC\ \text{backtrack removing a trail entry} & B \end{array} $$
The code sequence produced by Algorithm C is then read as a record of the evolving trail. A $D$ code increases the current decision level by one, a $P$ code records an implication at the current level, an $X$ code marks the end of the current branch, and $B$ codes undo assignments until the level selected by conflict analysis is reached.
This representation is analogous to the move codes of Algorithms A, B, D, and L because each code describes one meaningful transition in the state space. The internal changes to MEM, the watch lists, and the heap are omitted because they do not represent progress through the search tree. The displayed sequence therefore gives a human-readable trace of Algorithm C while preserving the same information needed to reconstruct the decisions, propagations, conflicts, and backtracks.