TAOCP 7.2.2.2 Exercise 262
In Algorithm C, the heap stores the variables ordered by their current activity values $\operatorname{ACT}(j)$.
Section 7.2.2.2: Satisfiability
Exercise 262. [20] What low-level operations underlie changes to the heap in steps C6–C8?
Verified: no
Solve time: 4m17s
Solution
In Algorithm C, the heap stores the variables ordered by their current activity values $\operatorname{ACT}(j)$. The purpose of steps C6–C8 is to maintain this ordering when activities change, so the heap operations are the standard upward and downward repairs of the heap order.
Suppose that the activity value of a variable $j$ is increased in step C6. The value $\operatorname{ACT}(j)$ may become larger than the value of its parent in the heap. The variable therefore moves upward through the heap. If $j$ is stored at position $p$, its parent is stored at position $\lfloor p/2\rfloor$. The heap is repaired by repeatedly comparing the key at $p$ with the key at $\lfloor p/2\rfloor$. Whenever the child has larger activity, the two heap entries are exchanged, and the position of $j$ is changed to $\lfloor p/2\rfloor$. The process stops when $j$ reaches the root or when its parent has activity at least as large as its own.
When a variable is inserted into the heap, the new item is placed at the next unused heap position. The same upward adjustment is then performed. If the new item is placed at position $p$, its parent positions are
$$ \left\lfloor \frac p2\right\rfloor,\ \left\lfloor \frac p4\right\rfloor,\ \left\lfloor \frac p8\right\rfloor,\ldots , $$
until the heap condition is restored.
In step C7, the activity values are rescaled. The numerical values of the activities change, but their relative order does not change because every activity is multiplied by the same positive factor. Therefore no exchange of heap entries is required. The heap links and the inverse position information remain valid.
In step C8, when the variable with maximum activity is removed or when a heap entry is otherwise replaced, the last item in the heap is moved into the vacated position. This item can violate the heap condition with respect to either its parent or its children. The parent comparison is handled by moving the item upward if its activity is larger than its parent's activity. Otherwise the child comparisons are handled by moving the item downward.
For downward adjustment, if the item is at position $p$, its children are at positions $2p$ and $2p+1$ whenever those positions are within the current heap size. The child with larger activity is selected. If that child's activity exceeds the activity of the item at $p$, the two entries are exchanged and the item continues at the child's former position. The operation ends when both children have activity no larger than the item or when the item reaches a leaf.
Each exchange of two heap entries also requires updating the auxiliary location information that records the heap position of each variable. Thus a heap modification consists of comparisons of activity values, exchanges of heap entries when necessary, and corresponding updates of the position fields. The linked lists used for watches and the trail are not involved in these operations.
Therefore the low-level operations in steps C6–C8 are insertion or deletion of heap entries, multiplication or alteration of activity keys, upward heapification, downward heapification, and the associated changes to the array entries and inverse position records.