TAOCP 7.2.2.2 Exercise 155

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

Verified: no
Solve time: 2m08s

Setup

Step X4 constructs the lookahead forest used by Algorithm X after step X3 has selected the candidate literals. The forest is stored in the arrays LL[j] and LO[j], together with PARENT pointers, and it must order the selected candidates so that step X6 can traverse them while maintaining the truth levels $T=BASE+LO[j]$.

Let the selected candidates be the literals in CAND, and let $S$ be their number. The purpose of the forest is not to represent the implication graph completely, but to organize the candidate literals by the levels at which they become relevant during lookahead. A literal $l$ is placed below a parent literal $p$ when the propagation caused by assuming $p$ leads naturally to the candidate $l$.

Solution

A direct construction of the lookahead forest is obtained by building it incrementally from the candidate list. First initialize an empty forest, with no roots and with every entry of PARENT undefined. Process the candidates in the order produced by the ranking in step X3.

For each candidate literal $l$, perform a shallow implication search beginning with the assumption that $l$ is true. The search follows only forced binary implications. If a forced implication reaches another candidate literal $q$, then $q$ belongs below $l$ in the forest, and we set

$$ PARENT(q)\leftarrow l . $$

If several candidate literals are reached from $l$, they become children of $l$. If a candidate literal is reached from two different ancestors, the first ancestor encountered in the breadth-first implication search is used, because only one parent pointer is required for the forest representation.

Candidates that are never reached from any other candidate become roots. Their relative order is chosen by the existing candidate order from step X3. A preorder traversal of the resulting forest gives the sequence

$$ LL[0],LL[1],\ldots,LL[S-1]. $$

For each position $j$, define

$$ LO[j] $$

to be the number of implication levels between the root of the corresponding tree and the literal $LL[j]$. Thus a root has

$$ LO[j]=0, $$

its children have

$$ LO[j]=1, $$

and so on. The pair of arrays $LL$ and $LO$ is therefore obtained from the forest by a single traversal.

The construction can be implemented efficiently by maintaining, for every candidate literal, the first level at which it is discovered during the implication search. Each binary implication edge is examined only when its source literal is removed from the search queue. If a literal has already received a parent pointer, later discoveries of that literal are ignored. Hence each implication relation is processed a constant number of times.

The resulting structure has the required property for step X6. When step X6 selects

$$ l\leftarrow LL[j], $$

the quantity

$$ T=BASE+LO[j] $$

is exactly the truth level at which the lookahead for $l$ begins. The parent pointer supplies the preceding level through

$$ H(l)\leftarrow H(PARENT(l)), $$

with the convention

$$ H(\Lambda)=0 . $$

Therefore the forest records precisely the nesting information needed by the later exploration steps.

The construction requires one implication search for each selected root and only extends searches through literals that can actually be reached from the candidates. If $S$ candidates are retained and $E$ binary implication relations are present among them, the total work is

$$ O(S+E), $$

after the implication lists have been prepared. The storage consists of the arrays LL, LO, and PARENT, each having at most $S$ entries.

Verification

Every nonroot node receives a parent exactly when it is first discovered by a forced implication from an earlier candidate. Hence every nonroot node has one parent, and every node has a unique path to a root. The structure is therefore a forest rather than a graph containing cycles.

The value of $LO[j]$ equals the number of parent links on the path from the root of the tree to $LL[j]$, because the traversal assigns level $0$ to roots and increases the level by one whenever it descends through a parent-child relation.

The preorder listing places every parent before all of its descendants. Consequently, when step X6 examines a candidate literal, all information needed from its ancestors has already been established through the PARENT links.

Thus the arrays LL and LO, together with PARENT, provide an efficient representation of the lookahead forest required by step X4.

$$ \boxed{\text{Construct the forest by linking each candidate to the first candidate that forces it, then store a preorder traversal in }LL\text{ and the corresponding depths in }LO.} $$

This completes the proof.

∎