TAOCP 7.2.2.2 Exercise 130

Section 7.2.2.2: Satisfiability

Exercise 130. [22] What low-level list processing operations are needed to "clear the watch list for $\bar{x}_k$" in step D6?

Verified: no
Solve time: 2m27s

Corrected solution:

Edit

Solution

In Algorithm D, the watch list for a literal is a linked list of clauses that are currently watching that literal. Step D6 asks to clear the watch list for $\bar{x}_k$, so the list associated with $\bar{x}_k$ must be transformed into the empty list.

In the list-processing framework of Section 2.2.6, this requires the standard operations for emptying a linked list. First, the list header for the watch list of $\bar{x}_k$ must be accessed. If its first link is not $\lambda$, the nodes in the list must be visited one at a time. For each node, its link field is read so that the next node can be reached, and the current node is deleted from the list. The deletion operation updates the appropriate predecessor and successor links, and the list header is updated so that, after the last deletion, it denotes the empty list.

Equivalently, the required low-level operations are:

1. Locate the list header corresponding to $\bar{x}_k$.
2. Inspect the header link to determine whether the list is empty.
3. Repeatedly follow the link fields to access each list node.
4. Delete each accessed node from the linked list, updating the neighboring links and the header as required by the list representation.
5. Leave the watch-list header in the empty state.

No changes are made to the watch lists of any other literals. The operation is therefore not merely an assignment that abandons the old first pointer. It is the application of the list deletion operations needed to remove every element of the watch list for $\bar{x}_k$ and restore that list to the empty-list representation.