TAOCP 7.2.2.2 Exercise 140

Section 7.2.2.2: Satisfiability

Exercise 140. [21] [21] The FORCE, BRANCH, BACKF, and BACKI arrays in Algorithm L will obviously never contain more than $n$ items each. Is there a fairly small upper bound on the maximum possible size of ISTACK?

Verified: no
Solve time: 1m21s

Solution

By the definition preceding Algorithm L, an entry of ISTACK is created only in the stamping operation (63). The operation is executed when a binary implication table is about to grow and when the current stamp of the literal is different from ISTAMP. The assignment in (63) sets IST(l) equal to the current value of ISTAMP, so the same literal can contribute at most one ISTACK entry during any one value of ISTAMP.

At step L5, ISTAMP is increased by one before the new round of binary propagation begins. Thus a single round of decision-making can add at most one entry for each possible literal. Since there are $2n$ literals, the number of entries added during one such round is at most $2n$.

The entries created during a round are not allowed to accumulate indefinitely. When Algorithm L backtracks from a branch, step L13 restores the previous sizes of the affected BIMP tables and decreases $I$ until it reaches the value stored in BACKI[d]. Therefore all entries belonging to the abandoned branch are removed. Consequently, while following one branch of the search tree, ISTACK can contain entries only from the current path of decisions.

A path in Algorithm L has length at most $n$, because every successful execution of step L12 fixes a variable permanently on the current path, and there are only $n$ variables. Hence there can be at most $n$ active rounds of decision-making along a path. Each of those rounds contributes at most $2n$ entries, giving

$$ |\text{ISTACK}| \leq n(2n)=2n^2 . $$

Therefore ISTACK has a quadratic upper bound, despite the fact that the other arrays mentioned in the exercise have only linear size.

This completes the proof.

$$ \boxed{|\text{ISTACK}| \leq 2n^2} $$

∎