TAOCP 7.2.2.2 Exercise 142
Let Algorithm L run and consider the chronological sequence of assignments to literals, written in the order in which each literal first receives a truth value.
Section 7.2.2.2: Satisfiability
Exercise 142. [24] [24] Algorithms A, B, and D can display their current progress by exhibiting a sequence of move codes $m_1 \ldots m_q$ such as (58) and (60); but Algorithm L has no such codes. Show that an analogous sequence $m_1 \ldots m_p$ could be printed in step L2, if desired. Use the codes of Algorithm D; but extend them to show $m_j = 6$ (or 7) if $R_{j-1}$ is a true (or false) literal whose value was found to be forced by Algorithm X, or forced by being a unit clause in the input.
Verified: yes
Solve time: 1m02s
Solution
Let Algorithm L run and consider the chronological sequence of assignments to literals, written in the order in which each literal first receives a truth value. Let this sequence be $R_0, R_1, \ldots, R_{p-1}$, so that $R_j$ is the literal whose value becomes fixed immediately after step $j$ of the execution of L.
At each step, the assignment of $R_j$ arises in exactly one of three mutually exclusive ways: it is introduced by a branching decision in L, it is forced by a unit clause in the current formula, or it is forced by implication propagation in Algorithm X triggered by previously assigned literals.
Extend the move-code system of Algorithm D as follows. All move codes used in D for branching and backtracking steps are kept unchanged. In addition, assign the code $6$ to any literal $R_j$ whose value is forced by a unit clause of the input or by a unit clause generated during the run, and assign the code $7$ to any literal $R_j$ whose value is forced by Algorithm X propagation rather than by a unit clause.
Now define $m_j$ to be the code assigned to $R_j$ under this convention. This defines a sequence $m_1 m_2 \ldots m_p$ that can be printed in step L2 by outputting $m_j$ exactly when $R_{j-1}$ becomes fixed.
The correspondence with Algorithm D follows from the fact that every assignment in L occurs either as a decision assignment or as a forced consequence of earlier decisions, and Algorithm D represents the same search process without propagation. Each decision in L corresponds to the same branching event in D and therefore uses the same D move code. Every remaining assignment in L is uniquely determined by the current partial assignment and the implication rules of unit clauses or Algorithm X; since these assignments are not represented as explicit moves in D, they are recorded by the auxiliary codes $6$ and $7$ without altering the underlying D move sequence.
Thus the augmented sequence $m_1 \ldots m_p$ records a faithful linearization of the computation history of Algorithm L using the move-code alphabet of Algorithm D with two additional symbols distinguishing forced assignments by unit propagation and by Algorithm X. This completes the construction of the required sequence. ∎