TAOCP 7.2.2.2 Exercise 142
Edit The sequence can be produced directly in step L2 by adding an output operation whenever Algorithm L extends its current partial assignment.
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: no
Solve time: 2m
Edit
Solution
The sequence can be produced directly in step L2 by adding an output operation whenever Algorithm L extends its current partial assignment.
Recall that Algorithm L proceeds by assigning values to literals in the current search state. Whenever L2 assigns the next literal, it can determine whether the assignment is a decision made by the search procedure or whether it is a forced assignment discovered during propagation. The output sequence is then extended by one move code at that moment.
For assignments that correspond to choices in the search tree, Algorithm L uses exactly the move codes of Algorithm D. Thus, if the assignment made in L2 is the result of the same branching action that Algorithm D would record, the corresponding code from Algorithm D is printed.
The remaining assignments are forced ones. If the literal (R_{j-1}) that is being assigned is true because its value has been forced by Algorithm X, L2 prints
[ m_j=6 . ]
If (R_{j-1}) is false because its value has been forced by Algorithm X, L2 prints
[ m_j=7 . ]
The same convention is used when the forcing comes from a unit clause that was already present in the input. Such a literal is not a branch choice, but a value that is already determined, so it receives the corresponding forced-assignment code according to its truth value.
The important point is that L2 does not need to record a unique logical reason for a forced assignment. A literal may be implied by several clauses, but Algorithm L only needs to recognize that the assignment was obtained by forcing rather than by making a new decision. The move code records the type of progress made, not the complete proof of the implication.
Therefore, if L2 outputs the appropriate code each time it assigns a literal, the resulting sequence
[ m_1,\ldots,m_p ]
has the same purpose as the progress sequences displayed by Algorithms A, B, and D. The ordinary Algorithm D codes display the branching decisions, while the additional codes (6) and (7) display forced true and forced false assignments. Hence Algorithm L can print an analogous progress sequence in step L2.