TAOCP 7.2.2.2 Exercise 121
Algorithm A maintains, for each literal $l$, a linked list of active clauses containing $l$.
Section 7.2.2.2: Satisfiability
Exercise 121. [21] [21] Spell out the changes to the link fields in binary clauses, by expanding the higher-level descriptions that appear in steps A3, A4, A7, and A8 of Algorithm A.
Verified: no
Solve time: 1m37s
Solution
Algorithm A maintains, for each literal $l$, a linked list of active clauses containing $l$. The operation $C(l)$ in steps A3 and A7 refers to this list. A binary clause $C={l,l'}$ has two literal occurrences, one linked into the list for $l$ and the other linked into the list for $l'$. The special case of binary clauses arises because suppressing or restoring one literal occurrence changes the availability of the other occurrence immediately.
For a binary clause $C={l,l'}$, let the occurrence of $l$ have link fields $\operatorname{LINK}(l,C)$ and $\operatorname{BACK}(l,C)$, and let the occurrence of $l'$ have the corresponding fields. The two occurrences are adjacent in their respective literal lists. Removing the occurrence of $l'$ from the list for $l'$ requires the two assignments
$$ \operatorname{LINK}(\operatorname{BACK}(l',C))\leftarrow \operatorname{LINK}(l',C), $$
and
$$ \operatorname{BACK}(\operatorname{LINK}(l',C))\leftarrow \operatorname{BACK}(l',C). $$
Restoring the occurrence reverses these assignments:
$$ \operatorname{LINK}(\operatorname{BACK}(l',C))\leftarrow l', $$
and
$$ \operatorname{BACK}(\operatorname{LINK}(l',C))\leftarrow l'. $$
The same two assignments are performed with $l$ and $l'$ interchanged whenever the other occurrence is the one being removed or restored.
In step A3, the operation “remove $\bar l$ from all active clauses containing it” is applied to every clause in $C(\bar l)$. For a binary clause $C={\bar l,l'}$, the occurrence of $\bar l$ is deleted from the $\bar l$ list by
$$ \operatorname{LINK}(\operatorname{BACK}(\bar l,C)) \leftarrow \operatorname{LINK}(\bar l,C), $$
and
$$ \operatorname{BACK}(\operatorname{LINK}(\bar l,C)) \leftarrow \operatorname{BACK}(\bar l,C). $$
The saved values of these two links are recorded so that step A8 can restore them.
In step A4, the operation “suppress all clauses that contain $l$” is applied to every clause in $C(l)$. For a binary clause $C={l,l'}$, the occurrence of $l'$ must also be removed from the list of active clauses containing $l'$, because the clause is no longer active. The changes are
$$ \operatorname{LINK}(\operatorname{BACK}(l',C)) \leftarrow \operatorname{LINK}(l',C), $$
and
$$ \operatorname{BACK}(\operatorname{LINK}(l',C)) \leftarrow \operatorname{BACK}(l',C). $$
The occurrence of $l$ is treated as the occurrence that caused the suppression and is already being processed by the traversal of $C(l)$.
In step A7, the operation “unsuppress all clauses that contain $l$” reverses step A4. For each binary clause $C={l,l'}$, the removed occurrence of $l'$ is inserted again between its former neighbors:
$$ \operatorname{LINK}(\operatorname{BACK}(l',C)) \leftarrow l', $$
and
$$ \operatorname{BACK}(\operatorname{LINK}(l',C)) \leftarrow l'. $$
After this insertion, $C$ again appears in both literal lists, namely $C(l)$ and $C(l')$.
In step A8, the operation “reinstate $\bar l$ in all active clauses that contain it” restores the literal occurrences removed in step A3. For a binary clause $C={\bar l,l'}$, the occurrence of $\bar l$ is reinserted by
$$ \operatorname{LINK}(\operatorname{BACK}(\bar l,C)) \leftarrow \bar l, $$
and
$$ \operatorname{BACK}(\operatorname{LINK}(\bar l,C)) \leftarrow \bar l. $$
Thus every higher-level deletion in steps A3 and A4 consists of two link changes for the other occurrence of a binary clause, while every corresponding restoration in steps A7 and A8 consists of the inverse two link changes. These assignments are precisely the low-level list operations required to maintain the invariant that the active occurrence lists contain exactly the literals belonging to unsuppressed clauses.
This completes the proof.
∎