TAOCP 7.2.2.2 Exercise 172

The corrected solution is below.

Section 7.2.2.2: Satisfiability

Exercise 172. [21] Explain why '+LO[j]' appears in step Y2's formula for BT.

Verified: no
Solve time: 2m45s


The corrected solution is below.

Edit

Solution

In step Y2, Algorithm Y sets

[ DT\leftarrow LBASE+LO[j]. ]

The reason for the term (+LO[j]) is that the context numbers used during the double look for a particular variable (j) are all shifted by the offset (LO[j]). The cutoff value (DT) must be in the same context-numbering class as those contexts.

Step Y3 makes the offset explicit. For the variable (j) currently being examined, it sets

[ T\leftarrow BASE+LO[j]. ]

Thus the initial context from which the lookahead procedure operates is not simply (BASE), but the context obtained by adding the position-dependent offset (LO[j]). Every context belonging to this particular double look is numbered relative to this same offset.

The purpose of (DT) is seen in step Y8. There the algorithm tests whether a conflict context satisfies

[ T<DT. ]

If this is true, the conflict is still inside the context range belonging to the current double look, so the algorithm continues the double-look processing. Otherwise, the conflict is returned to the ordinary search procedure at step X13. Therefore (DT) must be the upper limit that corresponds to the same shifted context range used by the current value of (j).

The value (LBASE) alone does not have this property. It is computed by

[ LBASE\leftarrow BASE+2SY, ]

and provides a base value in the context-numbering scheme before the offset associated with the current (j) is applied. It is not, by itself, the boundary for the contexts used in the current double look. Since the contexts for (j) begin at

[ BASE+LO[j], ]

the corresponding boundary must also be shifted by (LO[j]). Hence the correct cutoff is

[ DT=LBASE+LO[j]. ]

If the term (+LO[j]) were omitted, the algorithm would use

[ DT=LBASE ]

for every (j). Then the comparison in Y8 would compare a context number belonging to the (LO[j])-shifted numbering scheme against an unshifted boundary. The test would no longer correctly distinguish conflicts that are internal to the current double look from conflicts that belong to the surrounding search.

Therefore the appearance of (+LO[j]) in step Y2 is forced by the invariant that all context numbers associated with the current variable (j), including both the starting context in Y3 and the recovery limit used in Y8, must use the same offset. The formula is

[ \boxed{DT=LBASE+LO[j]}. ]

The term (LBASE) gives the base cutoff in Algorithm Y's context allocation, and (LO[j]) shifts that cutoff into the context range belonging to the particular look currently being performed.