TAOCP 7.2.2.2 Exercise 137

We restate the operations in the exact structure of Algorithm L, making explicit only the mechanisms actually available in the data structures: circular doubly linked free list of variables, and for e...

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 137. [24] Spell out in detail the processes of (a) removing a variable $X$ from the free list and from all pairs in TIMP lists (step L7 of Algorithm L), and of (b) restoring it again later (step L12). Exactly how do the data structures change?

Verified: yes
Solve time: 2m27s

We restate the operations in the exact structure of Algorithm L, making explicit only the mechanisms actually available in the data structures: circular doubly linked free list of variables, and for each variable $X$, a circular doubly linked list $\mathrm{TIMP}(X)$ of pair-nodes containing exactly the pairs in which $X$ participates.

Each pair-node $p$ corresponds to an ordered pair $(X,Y)$ and contains two independent pairs of links, one for its position in $\mathrm{TIMP}(X)$ and one for its position in $\mathrm{TIMP}(Y)$. No external incidence table is assumed.

(a) Step L7: removing $X$

Removal from the free list

The free list is a circular doubly linked list. Let

$$ L = \mathrm{pred}(X), \qquad R = \mathrm{succ}(X). $$

Step L7 removes $X$ by local splicing:

$$ \mathrm{succ}(L) \leftarrow R, \qquad \mathrm{pred}(R) \leftarrow L. $$

Crucially, the fields $\mathrm{pred}(X)$ and $\mathrm{succ}(X)$ are not overwritten. They remain stored in $X$ so that restoration is possible later.

Traversal of all TIMP nodes containing $X$

The only structure that enumerates all pair-nodes involving $X$ is the list $\mathrm{TIMP}(X)$ itself. This is a circular doubly linked list whose elements are exactly the nodes $p$ such that $p$ corresponds to a pair $(X,Y)$ for some $Y$.

Thus enumeration is performed by:

$$ p \leftarrow \mathrm{succ}(X), \quad \text{repeatedly following successors in } \mathrm{TIMP}(X) \text{ until returning to } X. $$

To avoid losing the traversal during deletions, the algorithm always stores the next node before unlinking:

$$ q \leftarrow \mathrm{succ}_X(p), $$

where $\mathrm{succ}_X$ denotes successor in the $\mathrm{TIMP}(X)$ list.

Deletion of a TIMP node

Let $p\in \mathrm{TIMP}(X)$ correspond to the pair $(X,Y)$. The node $p$ simultaneously lies in two circular lists: $\mathrm{TIMP}(X)$ and $\mathrm{TIMP}(Y)$.

  1. Remove $p$ from $\mathrm{TIMP}(X)$ by splicing:

$$ \mathrm{succ}_X(\mathrm{pred}_X(p)) \leftarrow \mathrm{succ}_X(p), \qquad \mathrm{pred}_X(\mathrm{succ}_X(p)) \leftarrow \mathrm{pred}_X(p). $$

  1. Remove $p$ from $\mathrm{TIMP}(Y)$ analogously:

$$ \mathrm{succ}_Y(\mathrm{pred}_Y(p)) \leftarrow \mathrm{succ}_Y(p), \qquad \mathrm{pred}_Y(\mathrm{succ}_Y(p)) \leftarrow \mathrm{pred}_Y(p). $$

  1. Push $p$ onto the backtracking stack $S(X)$, which records all deletions caused by choosing $X$.

After both splices, $p$ is completely excised from all TIMP structure but retains all of its internal pointer fields unchanged.

Completion of L7

After all nodes in $\mathrm{TIMP}(X)$ have been processed in this way, the list $\mathrm{TIMP}(X)$ becomes empty (except for the header $X$ itself), and $X$ is removed from the free list.

No auxiliary “incidence record” is required: enumeration is entirely by traversal of $\mathrm{TIMP}(X)$.

(b) Step L12: restoring $X$

Restoration reverses the above operations using only stored pointers and the stack $S(X)$.

Restoring TIMP nodes

The stack $S(X)$ contains exactly the nodes removed in L7, in reverse order of deletion. While the stack is nonempty, pop a node $p$, corresponding to some pair $(X,Y)$, and reinsert it into both lists it originally belonged to.

Because $p$ still stores its predecessor and successor pointers at the time of deletion, these pointers identify its former neighbors in each list.

Reinsertion into $\mathrm{TIMP}(X)$

Let $a = \mathrm{pred}_X(p)$, $b = \mathrm{succ}_X(p)$ be the stored neighbors. Restore by:

$$ \mathrm{succ}_X(a) \leftarrow p, \qquad \mathrm{pred}_X(b) \leftarrow p. $$

Reinsertion into $\mathrm{TIMP}(Y)$

Similarly, using stored $\mathrm{pred}_Y(p)$ and $\mathrm{succ}_Y(p)$:

$$ \mathrm{succ}_Y(\mathrm{pred}_Y(p)) \leftarrow p, \qquad \mathrm{pred}_Y(\mathrm{succ}_Y(p)) \leftarrow p. $$

Thus each node is restored to exactly the same position in both circular lists it occupied before L7.

Restoring $X$ to the free list

Finally, restore $X$ itself. Since L7 did not modify $\mathrm{pred}(X)$ and $\mathrm{succ}(X)$, these fields still contain the former neighbors $L$ and $R$.

Hence we reconnect:

$$ \mathrm{succ}(L) \leftarrow X, \qquad \mathrm{pred}(R) \leftarrow X. $$

This completes reinsertion of $X$ into the free list.

Conclusion

Step L7 performs a local deletion of $X$ from the free list and a complete removal of all nodes in $\mathrm{TIMP}(X)$ by traversal of that list, with each removed node pushed onto a stack. No external incidence structure is required, and no pointer information is lost because all list pointers remain stored inside each node.

Step L12 restores the exact previous state by popping nodes from the stack and reinserting them into their two TIMP lists using stored predecessor and successor pointers, followed by reinserting $X$ into the free list using its preserved neighbors.

All changes are therefore purely local pointer splices, and the transformation is exactly reversible.