TAOCP 7.2.2.2 Exercise 127
In the computation displayed in (59), Algorithm D is applied to the clauses of the unsatisfiable instance (9).
Section 7.2.2.2: Satisfiability
Exercise 127. [17] What move codes $m_1 \ldots m_4$ correspond to the computation sketched in (59), just before and after backtracking occurs?
Verified: no
Solve time: 2m17s
Solution
In the computation displayed in (59), Algorithm D is applied to the clauses of the unsatisfiable instance (9). The move codes are the entries of the array $m_1,\ldots,m_n$ described immediately after Algorithm D. The relevant meanings are that $m_j=1$ denotes the first attempt with $x_{h_j}=0$, $m_j=2$ denotes the second attempt with $x_{h_j}=1$ after the value $0$ has failed, and $m_j=4$ denotes a forced assignment $x_{h_j}=1$ arising from a unit clause.
Immediately before the backtracking shown in the row labeled “Backtrack” in (59), the first four assignments are
$$ x_1=0,\qquad x_2=0,\qquad x_3=1,\qquad x_4=0. $$
The first assignment is the choice $\bar{1}$, so $m_1=1$. The second assignment is the choice $\bar{2}$, so $m_2=1$. The third assignment comes from the unit clause $3$, so it is a forced positive assignment and $m_3=4$. The fourth assignment is the choice $\bar{4}$, so $m_4=1$. Therefore, immediately before backtracking,
$$ m_1m_2m_3m_4=1141. $$
During backtracking, Algorithm D discards the later forced assignments until it reaches the most recent unresolved two-way branch. The first four entries remain unchanged until the algorithm reaches the choice $\bar{4}$. Step D8 then changes the move code of that branch from the first attempt to the second attempt by replacing $m_d$ with $3-m_d$. Since $m_4=1$, this gives
$$ m_4\leftarrow 3-1=2. $$
The earlier entries $m_1$, $m_2$, and $m_3$ are not altered by this backtracking operation. Hence immediately after backtracking,
$$ m_1m_2m_3m_4=1142. $$
Thus the requested move-code strings are
$$ \boxed{\text{before backtracking: }1141} $$
and
$$ \boxed{\text{after backtracking: }1142}. $$