TAOCP 7.2.2.2 Exercise 141
Algorithm L uses the standard timestamp technique in which a global counter $\mathrm{ISTAMP}$ is incremented whenever a new marking phase begins, and each literal $l$ stores a value $\mathrm{IST}(l)$...
Section 7.2.2.2: Satisfiability
Exercise 141. [18] [18] Algorithm L might increase ISTAMP so often that it overflows the size of the IST($l$) fields. How can the mechanism of (63) avoid bugs in such a case?
Verified: yes
Solve time: 1m17s
Solution
Algorithm L uses the standard timestamp technique in which a global counter $\mathrm{ISTAMP}$ is incremented whenever a new marking phase begins, and each literal $l$ stores a value $\mathrm{IST}(l)$ indicating the most recent stamp at which $l$ was visited. A test of the form $\mathrm{IST}(l)=\mathrm{ISTAMP}$ determines whether $l$ has already been marked in the current phase, so correctness depends only on equality comparisons between $\mathrm{ISTAMP}$ and entries of $\mathrm{IST}(\cdot)$.
Let $M$ denote the largest integer representable in the field used for $\mathrm{IST}(l)$ and for $\mathrm{ISTAMP}$. If $\mathrm{ISTAMP}$ is incremented repeatedly, it will eventually reach $M$ and then overflow, producing a value that is no longer consistent with previous comparisons. After overflow, there exist literals $l$ and $l'$ and phases $p < p'$ such that $\mathrm{IST}(l)=\mathrm{IST}(l')$ while $\mathrm{ISTAMP}$ no longer reflects the intended temporal ordering, so the test $\mathrm{IST}(l)=\mathrm{ISTAMP}$ may accept or reject a literal incorrectly.
Mechanism (63) prevents this situation by ensuring that the meaning of the equality test is preserved whenever $\mathrm{ISTAMP}$ is about to overflow. When $\mathrm{ISTAMP}$ reaches its maximum admissible value, the algorithm performs a complete reinitialization of the timestamp structure: every field $\mathrm{IST}(l)$ is reset to a fixed baseline value, and $\mathrm{ISTAMP}$ is reset to a small initial value consistent with that baseline. After this global reset, all previous markings become irrelevant, since every literal satisfies $\mathrm{IST}(l)\ne \mathrm{ISTAMP}$ except those re-marked in the current phase.
The correctness of this repair follows from the fact that Algorithm L never uses the absolute magnitude of $\mathrm{ISTAMP}$, only equality with stored values. After reinitialization, all historical distinctions between earlier phases are discarded simultaneously, so no comparison can mix pre-reset and post-reset stamps. Each phase after the reset proceeds exactly as if execution had begun anew with empty $\mathrm{IST}(\cdot)$ fields, preserving all invariants used by step L9 and related marking operations.
Since the reset is performed only when $\mathrm{ISTAMP}$ is about to overflow, and since the reset restores a consistent global state in which all $\mathrm{IST}(l)$ values are synchronized, overflow cannot produce a spurious equality or inequality test. The mechanism therefore eliminates any possibility of incorrect behavior due to wrap-around of the timestamp field.
This completes the solution. ∎