TAOCP 7.2.2.2 Exercise 174
Double lookahead can be disabled by changing the implementation so that the lookahead procedure does not perform a second lookahead after the first forced assignment.
Section 7.2.2.2: Satisfiability
Exercise 174. [15] What's an easy way to accomplish (i) in the previous exercise?
Verified: yes
Solve time: 1m13s
Solution
Double lookahead can be disabled by changing the implementation so that the lookahead procedure does not perform a second lookahead after the first forced assignment.
In Algorithm L, ordinary lookahead tests a candidate literal $l$ by temporarily assigning $l$ and applying the forced consequences produced by unit clauses. Double lookahead repeats this process on the literals that become candidates during that first lookahead. Therefore the modification is to stop the recursive invocation after the first level.
The easiest implementation change is to add a Boolean control variable, say $\mathit{DL}$, initialized to $1$ in the normal algorithm. Whenever the code enters the lookahead routine, the first invocation is performed as before. Before the routine would begin the second lookahead level, test $\mathit{DL}$ and bypass that part when $\mathit{DL}=0$. Equivalently, in an implementation that already has a flag controlling the depth of lookahead, set the maximum lookahead depth from $2$ to $1$.
The resulting behavior preserves all ordinary lookahead effects, because every forced assignment caused directly by the trial literal is still processed. Only the additional tests caused by those forced assignments are removed. Hence this modification accomplishes the disabling required in exercise 173(i) without changing the rest of Algorithm L. $\boxed{\text{set the lookahead depth to one level}}$