TAOCP 7.2.2.2 Exercise 155

Exercise 155. [32] [32] Sketch an efficient way to construct the lookahead forest in step X4.

Verified: yes
Solve time: 1m10s

Setup

Let $F = {C_1,\dots,C_m}$ be a formula in CNF over variables ${x_1,\dots,x_n}$, and let literals be ordered by variable index with complements $\bar{l}$. In step X4 a lookahead forest is constructed in order to record consequences of tentative assignments, using unit propagation as in Section 7.2.2.2.

A forest node is a literal that becomes assigned true either by a decision or by forced propagation. A directed edge $l \to l'$ records that assignment of $l$ forces $l'$. Each connected component is a tree rooted at a decision literal.

The task is to construct this forest efficiently without recomputing clause status from scratch for each tentative assignment.

Solution

The construction uses an incremental clause-maintenance structure that supports unit propagation under temporary assignments.

For each clause $C \in F$, maintain a counter

$\mu(C) = #{l \in C : l \text{ is currently unassigned or currently true is unknown}}$

together with a distinguished pointer to the unique literal in $C$ that is still unassigned when $\mu(C)=1$.

Maintain also, for each literal $l$, the list $\mathrm{occ}(l)$ of clauses containing $l$.

A depth-first procedure builds one tree at a time. For a chosen decision literal $l_0$, start a new root node labeled $l_0$ and assign $l_0 := 1$. A stack $S$ stores the current propagation trail.

When a literal $l$ is set to true, every clause in $\mathrm{occ}(l)$ is marked satisfied and removed from further consideration in this branch. For each clause $C \in \mathrm{occ}(\bar{l})$, the value $\mu(C)$ is decreased by $1$. If $\mu(C)=1$, the remaining unassigned literal $l_C$ in $C$ is forced true, and an edge $l \to l_C$ is inserted into the forest. The literal $l_C$ is then pushed onto $S$.

Propagation continues until $S$ becomes empty, at which point the entire closure under unit clauses has been generated for the root $l_0$.

To avoid recomputing clause states from scratch for each root, all updates are made reversible. Each modification of a counter $\mu(C)$ and each clause-satisfaction marking is recorded on $S$ as a trail entry. When backtracking from a root, all changes are undone by popping $S$, restoring previous counters and clause statuses.

The full forest is obtained by repeating this procedure for each decision literal that is not yet assigned and not already contained in a previously constructed tree. Each repetition reuses the same clause incidence structure and only resets state via the recorded trail, rather than rebuilding counters.

This yields an incremental construction in which each clause-to-literal inspection is performed only when a literal is newly assigned true, and each propagation step creates exactly one edge in the forest.

This completes the construction.

∎

Verification

Each edge $l \to l'$ is created only when $l'$ becomes the unique unassigned literal in some clause $C$ after setting $l := 1$, so $l'$ is logically implied by $l$ under unit propagation.

Every forced assignment appears because it is the only remaining literal in some clause, since $\mu(C)=1$ is the only triggering condition.

No clause is processed more than once per literal assignment, since each occurrence in $\mathrm{occ}(l)$ is handled only when $l$ becomes true, and counters are updated in constant time per occurrence.

Backtracking correctness follows from recording every decrement and clause-status change on the trail stack, so restoration reproduces exactly the previous clause configuration before the next root is explored.

Thus the constructed directed edges represent exactly the implication relation induced by unit propagation in step X4, and the forest contains precisely the reachable forced assignments under each decision literal.