TAOCP 7.2.2.2 Exercise 124

Exercise 124. ▶ [21] Spell out the low-level link field operations that are sketched in step B3.

Verified: no
Solve time: 2m40s

Solution

In Algorithm B, the watch lists are not linked through clause numbers. The nodes of the lists are the literal occurrences themselves. If clause $C_j$ is currently watched by its first literal, then the node representing $C_j$ in the watch list is the position

$$ p=START(j). $$

The link field $LINK(p)$ gives the next literal position in the same watch list, and $W_l$ gives the first literal position whose stored literal is $l$.

Suppose that step B3 is processing a clause $C_j$ whose watched literal is

$$ L(p)=\bar l , $$

where $p=START(j)$. The purpose of B3 is to change the watched literal from $\bar l$ to another literal $u$ in the clause that is not currently false.

Let $q$ be the position of such a literal $u$ in the clause. The watched literal is moved to the first position of the clause by interchanging the literal fields:

$$ L(p)\leftarrow L(q), $$

$$ L(q)\leftarrow \bar l . $$

After this operation, position $p$ is still the node that represents the clause in the watch lists, but its literal value has changed from $\bar l$ to $u$. Thus the node at position $p$ must be removed from the watch list for $\bar l$ and inserted into the watch list for $u$.

Let

$$ s=W_{\bar l}. $$

$$ s=p, $$

then $p$ is the first node in the $\bar l$-list. The deletion is performed by the single assignment

$$ W_{\bar l}\leftarrow LINK(p). $$

Otherwise, there is a predecessor position $r$ in the same list such that

$$ LINK(r)=p . $$

The deletion operation is then

$$ LINK(r)\leftarrow LINK(p). $$

In either case, the value formerly in $LINK(p)$ is no longer needed as a link from the old list. The node at $p$ is now inserted at the front of the list for its new watched literal $u$. The old first node of that list is $W_u$, so the insertion operations are

$$ LINK(p)\leftarrow W_u, $$

$$ W_u\leftarrow p . $$

These are the complete low-level link-field operations. They use literal positions as list nodes throughout. No field $LINK(j)$ exists in the representation; the correct fields are $LINK(START(j))$ and, when a predecessor is needed, the link field of the predecessor literal occurrence.

The reason that the literal swap does not require moving the node itself is that the node of the watch list is the first literal position of the clause. After the swap, that same position $p$ now contains the new watched literal $u$, so only its membership in the linked watch lists changes. The deletion removes the position $p$ from the list headed by $W_{\bar l}$, and the insertion places the same position at the head of the list headed by $W_u$. Therefore every watch list continues to contain exactly the literal positions whose current first literal has the corresponding value.