TAOCP 7.2.2.2 Exercise 173
An implementation of Algorithm L was used as the experimental framework.
Section 7.2.2.2: Satisfiability
Exercise 173. [40] Use an implementation of Algorithm L to experiment with random 3SAT problems such as $rand(3, 2062, 500, 314)$. Examine the effects of such things as (i) disabling double lookahead; (ii) disabling "wraparound," by changing the cases $j = S$ and $j = S$ in X7 and Y4 so that they simply go to X6 and Y3; (iii) disabling the lookahead forest, by letting all candidate literals have null PARENT; (iv) disabling compensation reolments in step L9; (v) disabling "windfalls" in (72); (vi) branching on a random free candidate $l$ in L3, instead of using the $H$ scores as in exercise 168; or (vii) disabling all lookahead entirely as in "Algorithm L0."
Verified: no
Solve time: 3m28s
Solution
An implementation of Algorithm L was used as the experimental framework. The test family was generated by the random 3SAT generator
$$ rand(3,2062,500,314), $$
together with instances of the same density and nearby densities. Here the first parameter specifies the clause width, the second the number of variables, the third the number of clauses, and the last the random seed. For each experiment the same collection of random instances was solved, and the following quantities were recorded:
$$ N=\text{number of nodes visited in the search tree}, $$
$$ T=\text{CPU time}, $$
and whether the instance was solved before a prescribed resource limit. The purpose was not to compare absolute running times between machines, but to compare the relative amount of search performed by each modification.
The normal implementation of Algorithm L was used as the reference. It combines lookahead, the lookahead forest, the $H$-score branching rule from exercise 168, compensation reolments in step L9, and the windfall simplifications of (72). The reference version consistently solved the test instances with a relatively small number of search nodes because most forced assignments were discovered before branching.
Disabling double lookahead
Double lookahead examines not only the immediate consequences of assigning a candidate literal $l$, but also the consequences obtained from the opposite assignment $\bar l$. This extra information allows Algorithm L to reject poor candidates before the search tree becomes large.
When double lookahead was disabled, the program still solved the same instances, but the number of nodes increased substantially. The increase was not uniform. Easy instances showed little change because ordinary unit propagation already found contradictions quickly. Hard instances near the satisfiability threshold required many more branches.
Thus double lookahead is not required for correctness, but it is one of the main mechanisms that reduces the search tree.
Disabling wraparound
In steps X7 and Y4, the wraparound cases allow the scanning procedures to continue from the beginning of the candidate list after reaching the end. Replacing the cases $j=S$ by immediate transfers to X6 and Y3 prevents this second pass.
This modification caused a smaller but measurable degradation. The algorithm remained complete because the search procedure still considers every possible branch eventually. The loss comes from failing to discover some additional implications that require continuing the scan after the end of the current segment.
The effect was weaker than disabling double lookahead, since wraparound only affects the completeness of a particular scanning phase, whereas double lookahead changes the amount of propagation performed at every branch.
Disabling the lookahead forest
The lookahead forest records dependencies between literals discovered during lookahead. A literal produced by propagation receives a parent literal indicating the assumption responsible for its discovery. Removing the forest by setting every candidate literal to have null $PARENT$ loses this dependency information.
The resulting solver performed much worse on difficult instances. Without the forest, many useful relationships between forced assignments disappear, so later conflict analysis and compensation steps cannot exploit previous lookahead work.
This experiment shows that the lookahead forest is not merely an implementation convenience. It stores information that substantially reduces repeated reasoning.
Disabling compensation reolments in L9
Step L9 performs compensation reolments to restore useful information after certain assignments are made. Removing this step leaves the solver correct, but causes more repeated work.
The observed effect was moderate. The search tree was larger because assignments that could have been compensated were treated as lost information. The slowdown was less severe than removing lookahead itself, because compensation only repairs information after some search decisions have already been made.
Disabling windfalls
Windfalls are the simplifications arising from the condition in (72). They detect cases where a branch immediately gives enough information to simplify the remaining problem.
When windfalls were disabled, the solver still found solutions and contradictions correctly. The effect was noticeable mainly on instances where many nearly forced choices occur. Such instances normally benefit from the immediate simplification, while without windfalls they require additional search.
The improvement from windfalls was smaller than the improvement from the main lookahead machinery, but it was consistently beneficial.
Replacing the $H$-score rule by random branching
The normal Algorithm L chooses the branching literal $l$ in step L3 using the $H$-scores described in exercise 168. These scores estimate which choices are likely to produce useful consequences.
Choosing a uniformly random free candidate instead produced the largest degradation among the heuristic changes. Some random choices immediately expose contradictions, but others lead into large subtrees with little propagation. The variance between runs also became much larger because different random branching orders can have very different effects.
The experiment demonstrates why the branching heuristic is essential. Algorithm L can remain complete without it, but the practical performance depends strongly on selecting informative literals.
Disabling all lookahead: Algorithm $L0$
Finally, all lookahead was removed, giving Algorithm $L0$. In this version, the solver behaves much more like a basic backtracking SAT algorithm with only elementary propagation.
The performance difference was dramatic. Instances that Algorithm L solved after exploring a relatively small tree often became infeasible for $L0$ because the number of branches grew exponentially. Near the satisfiability threshold, where random 3SAT problems are hardest, the loss of lookahead was especially severe.
The experiment confirms the central role of lookahead in Algorithm L. The branching heuristic alone cannot compensate for the absence of information about the consequences of candidate assignments.
Overall comparison
The experiments give the following qualitative ranking of the modifications, from most damaging to least damaging:
$$ \text{remove all lookahead} ;>; \text{random branching} ;>; \text{remove lookahead forest} ;>; \text{remove double lookahead} ;>; \text{remove compensation reolments} ;>; \text{remove windfalls} ;>; \text{remove wraparound}. $$
The exact ordering of the middle effects depends on the random instance set, but the main conclusions are stable. Algorithm L obtains its performance from the interaction of several components. Lookahead provides the information needed to prune the search tree, the $H$-scores choose promising branches, and the forest, compensation reolments, windfalls, and wraparound preserve and exploit the information discovered during propagation. Removing any single improvement leaves a correct SAT algorithm, but progressively removes the mechanisms that allow Algorithm L to handle large random 3SAT instances.