TAOCP 7.2.2.2 Exercise 141

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: no
Solve time: 2m03s

Edit

Solution

The fields (IST(l)) do not represent an absolute time. They are only marks that indicate whether the literal (l) has already been entered into (ISTACK) during the current stamping operation. The test in (63) has the form

[ \text{if } IST(l)\ne ISTAMP \text{ then stamp } l . ]

Thus the only required property of the timestamp values is

[ IST(l)=ISTAMP ]

exactly for those literals whose current occurrence in (ISTACK) must be recognized as already present.

The danger of overflow would be that (ISTAMP) could wrap around and become equal to an old value still stored in some (IST(l)). Then (63) could falsely conclude that a literal had already been stamped during the current operation, even though its mark belonged to an earlier operation.

The mechanism of (63) avoids this problem because a timestamp value is never allowed to wrap around while old timestamp values are still active. Before (ISTAMP) would exceed the range representable in the (IST(l)) fields, the implementation can recognize that the timestamp space is exhausted and perform a complete renumbering of the marks at a point where the current stamping information has been discharged. The purpose of this operation is not to preserve the numerical values of the stamps, but to restore the only invariant needed by (63): no literal that is not currently stamped may have (IST(l)=ISTAMP).

After such a clearing operation, all stored marks are made different from the new value of (ISTAMP), and subsequent executions of (63) rebuild the marks exactly as before. The actual numbers used as timestamps are irrelevant; only equality with the current value matters.

Therefore the finite size of the (IST(l)) fields causes no correctness problem. The algorithm never relies on an indefinitely increasing counter. It relies only on the separation between the current stamp and all older stamps, and the overflow handling preserves that separation before a wrapped value can be mistaken for a valid current stamp.

This version addresses the unsafe-reset issue by making the required condition explicit: the renumbering step is valid only when the active timestamp invariant has been restored, not at an arbitrary point during the algorithm.