TAOCP 7.2.2.2 Exercise 250
For $R'$ in equation (7), the solution requires the literals $4$, $\bar{1}$, and $2$.
Section 7.2.2.2: Satisfiability
Exercise 250. [**] [§5] Since the clauses $R'$ in (7) are satisfiable, Algorithm I might discover a solution without ever reaching step I4. Try, however, to make the choices in steps I2, I3, and I4 so that the algorithm takes as long as possible to discover a solution.
Verified: no
Solve time: 1m17s
For $R'$ in equation (7), the solution requires the literals $4$, $\bar{1}$, and $2$. To delay discovery of this solution, the choices in steps I2 and I3 should avoid these literals as long as possible. A longest unsuccessful branch can be obtained by repeatedly choosing the opposite polarity before the forced choices are reached, for example by taking the branch assignments
$1 \leftarrow 1,\qquad 2 \leftarrow \bar{2},\qquad 3 \leftarrow 3,\qquad 4 \leftarrow \bar{4}.$
Under these choices the clauses $4\bar{1}2$ and $\bar{3}4\bar{1}$ cannot be satisfied, so step I4 is eventually reached and the branch is rejected. Backtracking then changes the most recent choice, and the next surviving branch forces the necessary literals $4$, $\bar{1}$, and $2$; the algorithm finds a satisfying cover. The displayed branch contains four assignments, and each assignment is one replacement operation, so this trial uses exactly $4$ replacement operations before failure. The delayed solution is obtained by taking the forced literals ${4,\bar{1},2}$, together with either $3$ or $\bar{3}$.