TAOCP 7.2.2.2 Exercise 143

We restart the construction so that the definition of “big clause” is enforced consistently at every stage of the algorithm.

taocpmathematicsalgorithmsvolume-4hard

Section 7.2.2.2: Satisfiability

Exercise 143. ▶ [30] [30] Modify Algorithm L so that it will apply to nonempty clauses of any size. Call a clause big if its size is greater than 2. Instead of TIMP tables, represent every big clause by KINX and CSIZE codes: every literal $l$ has a sequential list KINX($l$) of big clause numbers; every big clause $c$ has a sequential list CINX($c$) of literals; $c$ is in KINX($l$) if and only if $l$ is in CINX($c$). The current number of active clauses containing $l$ is indicated by KSIZE($l$); the current number of active literals in $c$ is indicated by CSIZE($c$).

Verified: no
Solve time: 3m47s

We restart the construction so that the definition of “big clause” is enforced consistently at every stage of the algorithm.

A clause is big iff its current size is greater than $2$. Therefore every clause with current size $0,1,2$ must not reside in the big-clause subsystem. The data structure must maintain this invariant at all times.

1. Data structures

We maintain only big clauses in the incidence structure:

  • $\mathrm{KINX}(l)$: list of all active big clauses containing literal $l$,
  • $\mathrm{CINX}(c)$: list of literals in big clause $c$,
  • $\mathrm{KSIZE}(l)$: number of active big clauses containing $l$,
  • $\mathrm{CSIZE}(c)$: number of currently un-falsified literals in big clause $c$.

A clause is represented in this structure if and only if it is active and $\mathrm{CSIZE}(c) > 2$.

2. Invariants

At all times:

  1. $\mathrm{KSIZE}(l)$ equals the number of active big clauses containing $l$.
  2. For every active big clause $c$, $\mathrm{CSIZE}(c)$ equals the number of literals in $c$ not yet set to false.
  3. Every clause with $\mathrm{CSIZE}(c) \le 2$ is not stored in $\mathrm{KINX}, \mathrm{CINX}$.
  4. Every stored clause satisfies $\mathrm{CSIZE}(c) > 2$.

3. Initialization

For each input clause $c$:

  • If $|c| > 2$:

  • set $\mathrm{CINX}(c) := c$,

  • set $\mathrm{CSIZE}(c) := |c|$,

  • for each $l \in c$, insert $c$ into $\mathrm{KINX}(l)$,

  • increment $\mathrm{KSIZE}(l)$ accordingly.

  • If $|c| \le 2$:

  • store $c$ in the original Algorithm L structure only,

  • do not place $c$ in the big-clause system.

4. Assignment updates

We describe the two cases.

4.1 Case: $l := \mathrm{true}$

Every clause containing $l$ is satisfied.

For each big clause $c \in \mathrm{KINX}(l)$:

  1. Remove $c$ from all $\mathrm{KINX}(l')$ for $l' \in \mathrm{CINX}(c)$.
  2. Decrement $\mathrm{KSIZE}(l') := \mathrm{KSIZE}(l') - 1$ for all such $l'$.
  3. Delete $c$ from the big-clause system.

This preserves the invariant since $c$ no longer contributes to any incidence count.

4.2 Case: $l := \mathrm{false}$

For each active big clause $c \in \mathrm{KINX}(\bar l)$:

  1. Decrement

$$ \mathrm{CSIZE}(c) := \mathrm{CSIZE}(c) - 1. $$

  1. Now consider the resulting value.

(a) $\mathrm{CSIZE}(c) = 0$

All literals in $c$ are false. A contradiction occurs and backtracking is triggered.

(b) $\mathrm{CSIZE}(c) = 1$

Let $l^*$ be the unique remaining un-falsified literal in $c$.

We must first remove $c$ from the big-clause system, because it is no longer big.

  1. For each $l' \in \mathrm{CINX}(c)$:
  • remove $c$ from $\mathrm{KINX}(l')$,
  • decrement $\mathrm{KSIZE}(l')$.
  1. Delete $c$ from $\mathrm{CINX}, \mathrm{CSIZE}$.
  2. Force assignment $l^* := \mathrm{true}$.
  3. Propagate this assignment using Algorithm L.

This corrects the previously missing migration step: unit clauses are immediately removed from the big-clause subsystem before further propagation.

(c) $\mathrm{CSIZE}(c) = 2$

Let the remaining literals be $l_1, l_2$. Since $c$ is no longer big, it must be migrated.

  1. For each $l' \in \mathrm{CINX}(c)$:
  • remove $c$ from $\mathrm{KINX}(l')$,
  • decrement $\mathrm{KSIZE}(l')$.
  1. Delete $c$ from the big-clause system.
  2. Insert binary clause $(l_1 \lor l_2)$ into the original Algorithm L structure.

5. Correctness argument

Preservation of the big-clause invariant

A clause is present in the big system iff its current size exceeds 2.

  • When $\mathrm{CSIZE}(c)$ becomes 2 or 1, we explicitly remove $c$ from all $\mathrm{KINX}$ lists and decrement all corresponding $\mathrm{KSIZE}$ values.
  • Hence no clause with size $\le 2$ remains in the system.

Thus the definition of “big” is enforced exactly.

Preservation of $\mathrm{KSIZE}$

Each big clause contributes exactly once to each $\mathrm{KSIZE}(l)$ for its literals. Whenever a clause is removed (due to satisfaction or size reduction to $\le 2$), it is removed from all incidence lists and each $\mathrm{KSIZE}$ is decremented exactly once per contained literal. Therefore $\mathrm{KSIZE}(l)$ always equals the number of active big clauses containing $l$.

Preservation of $\mathrm{CSIZE}$

$\mathrm{CSIZE}(c)$ tracks exactly the number of literals not yet falsified while $c$ remains in the big system. Once it drops to $\le 2$, the clause is removed, so no inconsistent state persists.

Soundness of propagation

  • If $\mathrm{CSIZE}(c)=1$, the clause becomes unit and forces its remaining literal, exactly as in Algorithm L.
  • If $\mathrm{CSIZE}(c)=2$, the clause becomes binary and is handled by the original mechanism.
  • Big clauses are reduced only while they remain structurally big.

No clause is double-counted or omitted.

6. Conclusion

The modified Algorithm L correctly replaces TIMP tables by incidence lists $\mathrm{KINX}, \mathrm{CINX}$ together with counters $\mathrm{KSIZE}, \mathrm{CSIZE}$, provided that clauses are removed from the big-clause subsystem whenever their size becomes $2$ or $1$. This ensures exact maintenance of the “big clause” invariant and yields a correct implementation of the required modification. ∎