TAOCP 7.2.2.2 Exercise 121

We restate only the pointer-level modifications for binary clauses, making all changes to incidence-list links and clause-cycle links explicit.

taocpmathematicsalgorithmsvolume-4medium

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: 3m53s

We restate only the pointer-level modifications for binary clauses, making all changes to incidence-list links and clause-cycle links explicit. We use the standard representation:

Each literal occurrence node $x$ has two independent link structures:

$$ \mathrm{next}(x), \mathrm{prev}(x) \quad \text{(incidence list of its literal)} $$

$$ \mathrm{next}_C(x), \mathrm{prev}_C(x) \quad \text{(clause-cycle of its clause } C\text{)}. $$

For a binary clause $C = (u \lor v)$, there are exactly two occurrence nodes $x_u, x_v$, and initially:

$$ \mathrm{next}_C(x_u)=x_v,\quad \mathrm{next}_C(x_v)=x_u, \quad \mathrm{prev}_C(x_u)=x_v,\quad \mathrm{prev}_C(x_v)=x_u. $$

Both nodes also belong to their respective incidence lists.

Step A3: satisfy literal $l$

Every clause containing $l$ is deleted. For a binary clause $C=(l \lor l')$ with nodes $x_l, x_{l'}$, both nodes are removed from their incidence lists.

Incidence list updates

$$ \mathrm{next}(\mathrm{prev}(x_l)) \gets \mathrm{next}(x_l), \quad \mathrm{prev}(\mathrm{next}(x_l)) \gets \mathrm{prev}(x_l), $$

$$ \mathrm{next}(\mathrm{prev}(x_{l'})) \gets \mathrm{next}(x_{l'}), \quad \mathrm{prev}(\mathrm{next}(x_{l'})) \gets \mathrm{prev}(x_{l'}). $$

Clause-cycle effect

The entire clause is deleted, so no clause-cycle structure for $C$ remains active. Since both nodes are removed from all active lists, the clause-cycle links are not used further in the forward computation. We leave:

$$ \mathrm{next}_C(x_l), \mathrm{prev}_C(x_l), \mathrm{next}C(x{l'}), \mathrm{prev}C(x{l'}) $$

unchanged for backtracking.

Thus A3 only splices both nodes out of incidence lists; clause-cycle pointers are preserved as saved state.

Step A4: delete $\bar l$ from clauses containing it

Let $C = (\bar l \lor l')$ with nodes $x_{\bar l}$ and $x_{l'}$. We remove the occurrence $x_{\bar l}$.

Incidence list update

$$ \mathrm{next}(\mathrm{prev}(x_{\bar l})) \gets \mathrm{next}(x_{\bar l}), \quad \mathrm{prev}(\mathrm{next}(x_{\bar l})) \gets \mathrm{prev}(x_{\bar l}). $$

Explicit clause-cycle rewiring (critical part)

Initially:

$$ \mathrm{next}C(x{\bar l}) = x_{l'}, \quad \mathrm{prev}C(x{\bar l}) = x_{l'}, \quad \mathrm{next}C(x{l'}) = x_{\bar l}, \quad \mathrm{prev}C(x{l'}) = x_{\bar l}. $$

To remove $x_{\bar l}$ from the clause-cycle, we splice it out:

Redirect the surviving node

$$ \mathrm{next}C(x{l'}) \gets x_{l'}, \quad \mathrm{prev}C(x{l'}) \gets x_{l'}. $$

Isolate the removed node (mark inactive in clause-cycle structure)

$$ \mathrm{next}C(x{\bar l}) \gets x_{\bar l}, \quad \mathrm{prev}C(x{\bar l}) \gets x_{\bar l}. $$

Thus the clause-cycle is transformed from a 2-cycle into a 1-cycle on $x_{l'}$, while preserving all information needed for backtracking.

Step A7: restore clauses deleted in A3

For each binary clause $C=(l \lor l')$ deleted in A3, both nodes $x_l, x_{l'}$ are reinserted into their incidence lists using their stored predecessor and successor pointers:

$$ \mathrm{next}(\mathrm{prev}(x_l)) \gets x_l, \quad \mathrm{prev}(\mathrm{next}(x_l)) \gets x_l, $$

$$ \mathrm{next}(\mathrm{prev}(x_{l'})) \gets x_{l'}, \quad \mathrm{prev}(\mathrm{next}(x_{l'})) \gets x_{l'}. $$

No changes are made to clause-cycle pointers in A7, since A3 did not modify them.

Step A8: restore literals deleted in A4

For each clause $C=(\bar l \lor l')$, we restore $x_{\bar l}$ into its incidence list:

$$ \mathrm{next}(\mathrm{prev}(x_{\bar l})) \gets x_{\bar l}, \quad \mathrm{prev}(\mathrm{next}(x_{\bar l})) \gets x_{\bar l}. $$

Now restore the clause-cycle from the collapsed form.

Before restoration:

$$ \mathrm{next}C(x{l'}) = x_{l'}, \quad \mathrm{prev}C(x{l'}) = x_{l'}. $$

We reconnect the original 2-cycle:

$$ \mathrm{next}C(x{l'}) \gets x_{\bar l}, \quad \mathrm{prev}C(x{\bar l}) \gets x_{l'}, $$

$$ \mathrm{next}C(x{\bar l}) \gets x_{l'}, \quad \mathrm{prev}C(x{l'}) \gets x_{\bar l}. $$

This restores the original circular ordering $x_{\bar l} \leftrightarrow x_{l'}$.

Summary (binary clause behavior)

For a binary clause $C=(u \lor v)$:

In A3, both occurrence nodes are removed from incidence lists, while clause-cycle links are preserved for later restoration.

In A4, one occurrence is removed; its removal is implemented by explicitly splicing it out of the clause-cycle, updating the surviving node into a 1-cycle and isolating the removed node.

In A7, deleted clauses are restored by reinserting both nodes into incidence lists, without touching clause-cycle structure.

In A8, the removed node is reinserted and the clause-cycle is explicitly expanded back from a 1-cycle to the original 2-cycle by restoring both directions of the links.