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: yes
Solve time: 1m02s

Solution

Let $W(l)$ denote the head pointer of the watch list for literal $l$, and let each node of a watch list be a record containing a clause pointer $C$ and a link field $next$. The watch list for $l$ is a singly linked list whose nodes enumerate exactly the clauses currently watching $l$ in Algorithm D.

“Clearing the watch list for $\bar{x}_k$” in step D6 means processing every node in $W(\bar{x}_k)$ so that no clause remains watching $\bar{x}_k$ after the assignment of $x_k$. This requires traversing the entire linked list and, for each clause encountered, removing its node from $W(\bar{x}_k)$ and reinserting the clause into a suitable alternative watch list.

Let $p \leftarrow W(\bar{x}_k)$ be the initial pointer to the first node. Each iteration processes one node and advances to the next node saved before any modification. The traversal uses the standard pattern of loading a link field, preserving it, and relinking pointers.

For a node $p$ with clause $C$, let $q \leftarrow next(p)$ be computed before any pointer updates. The node $p$ is then removed from $W(\bar{x}_k)$ by updating the predecessor link or, if $p$ is the head node, by setting $W(\bar{x}_k) \leftarrow q$. After removal, the clause $C$ must be assigned a new watched literal $l'$ different from $\bar{x}_k$. This requires scanning the literals of $C$ until a literal $l'$ is found such that $|l'| \ne k$ or the current assignment does not falsify $l'$. The clause node is then inserted into the watch list $W(l')$ by linking its $next$ field to the previous head of $W(l')$ and updating $W(l') \leftarrow p$.

The process continues by setting $p \leftarrow q$ and repeating until $p = \text{nil}$.

The low-level list processing operations required are therefore exactly those needed for pointer-based traversal and modification of singly linked lists together with cross-list relocation of nodes. These consist of reading the head pointer $W(\bar{x}_k)$, reading and storing a node link field $next(p)$ before modification, updating $W(\bar{x}_k)$ when the removed node is the head, changing the $next$ field of a node to perform insertion at the head of another watch list $W(l')$, and repeated pointer advancement $p \leftarrow next(p)$ using the saved successor pointer. Each clause relocation additionally requires updating the clause’s internal record of which literal it watches, but this is an internal field update rather than a list operation.

This completes the list of operations needed to clear the watch list for $\bar{x}_k$ in step D6. ∎