TAOCP 7.2.2.2 Exercise 134

Section 7.2.2.2: Satisfiability

Exercise 134. [22] The BIMP tables used by Algorithm L are sequential lists of dynamically varying size. One attractive way to implement them is to begin with every list having capacity 4 (say); then when a list needs to become larger, its capacity can be doubled.

Adapt the buddy system (Algorithm 2.5R) to this situation. (Lists that shrink when backtracking needn't free their memory, since they're likely to grow again later.)

Verified: no
Solve time: 2m04s

Solution

Algorithm 2.5R manages a collection of variable-size blocks by maintaining blocks whose sizes are powers of two. The same idea applies to the BIMP tables of Algorithm L, except that the allocated object is a list of literals rather than a general memory block.

For each BIMP table, maintain a list descriptor containing the address of the first entry, the current length, and the current capacity. The capacity is always a power of two. Initially every BIMP table has capacity $4$.

Suppose a BIMP table has length $r$ and capacity $c$. If a new entry is appended and $r<c$, the entry is placed in position $r+1$ and the length is increased by one. If instead $r=c$, a new list area of capacity $2c$ is obtained. The entries of the old list are copied into the new area, the new entry is appended, and the descriptor is changed to refer to the new area.

In step notation, the extension operation can be written as follows.

$$ \begin{array}{ll} B1.&\text{Set }r\leftarrow\text{current length and }c\leftarrow\text{current capacity}.\ B2.&\text{If }r<c,\text{ put the new entry into position }r+1,\text{ set }r\leftarrow r+1,\text{ and terminate.}\ B3.&\text{Reserve a new list of capacity }2c.\ B4.&\text{Copy entries }1,\ldots,r\text{ from the old list into the new list}.\ B5.&\text{Put the new entry into position }r+1,\text{ set }c\leftarrow2c,\text{ set }r\leftarrow r+1,\text{ and update the descriptor.} \end{array} $$

The invariant is that every BIMP table has enough reserved space for its current entries, and its capacity is the smallest power of two reached by repeated doubling from $4$ that is at least its length. Step B2 preserves the invariant because the length remains at most the capacity. Steps B3 through B5 preserve it because the new capacity is exactly twice the old capacity and therefore remains a power of two.

When Algorithm L backtracks, a BIMP table may become shorter. No contraction operation is needed. The length field is decreased to the required value, while the allocated capacity remains unchanged. The invariant is preserved because the capacity is still at least the length. If later insertions make the table grow again, the unused space is immediately available.

The total copying cost is bounded in the usual dynamic-array manner. Consider a table that eventually reaches capacity $4\cdot2^k$. The reallocations copy

$$ 4+8+16+\cdots+4\cdot2^{k-1} $$

entries. This geometric sum is

$$ 4(1+2+\cdots+2^{k-1}) =4(2^k-1) <4\cdot2^k. $$

The final capacity is $4\cdot2^k$, so the total number of copied entries is less than the final allocated size. Therefore a sequence of $m$ insertions into one BIMP table requires fewer than $m$ additional copies beyond the direct insertions, giving constant amortized cost per insertion.

The buddy organization also makes unused memory reusable. A list whose size decreases during backtracking keeps its allocated block, so future extensions of the same BIMP table do not require another allocation unless its capacity is exceeded. If a table is destroyed permanently, its block can be returned by the same merging rule as Algorithm 2.5R: two adjacent free blocks of the same size are replaced by their unique parent block of twice the size, and this merging continues while the buddy block is also free.

Thus Algorithm 2.5R adapts directly by replacing fixed memory requests with BIMP-table capacities, doubling whenever a table overflows and retaining enlarged blocks during backtracking. The resulting implementation has the required dynamic behavior and preserves the efficiency properties of the buddy system. $\boxed{\text{doubling-capacity BIMP tables with retained blocks during backtracking}}$