TAOCP 7.2.2.2 Exercise 137
In Algorithm L, the free list contains the variables that have not yet been assigned a value.
Section 7.2.2.2: Satisfiability
Exercise 137. [24] Spell out in detail the processes of (a) removing a variable $X$ from the free list and from all pairs in TIMP lists (step L7 of Algorithm L), and of (b) restoring it again later (step L12). Exactly how do the data structures change?
Verified: no
Solve time: 1m28s
Solution
In Algorithm L, the free list contains the variables that have not yet been assigned a value. The lists $\operatorname{TIMP}(x)$ contain pairs of literals that become relevant when the variable $x$ is assigned. The operation in step L7 removes a variable $X$ from further consideration at the current decision level, while step L12 reverses that operation when the search backtracks.
Suppose that step L7 chooses the variable $X$ and assigns it a value. The free-list entry for $X$ is removed first. The variable can no longer be selected as a branching variable, because its value has been fixed on the current branch of the search tree.
The removal from the $\operatorname{TIMP}$ lists is performed by scanning the entries associated with $X$ and deleting every pair containing $X$ or $\bar X$. If a pair is written as ${l_1,l_2}$, the deletion test is
$$ |l_1|=X\quad\text{or}\quad |l_2|=X . $$
Such a pair cannot participate in future propagation after $X$ has been assigned, because one member of the pair has already been decided. All other pairs remain unchanged. Therefore the operation preserves the invariant that every pair stored in a $\operatorname{TIMP}$ list consists only of literals whose variables are still free.
For every deletion made in L7, the original position must be recorded on the undo stack. The record contains the variable $X$, its former position in the free list, and the locations of all deleted $\operatorname{TIMP}$ entries. If a deleted pair occurred in the $\operatorname{TIMP}(Y)$ list, the record also stores the identity of $Y$, the position of the pair in that list, and the pair itself. The positions are necessary because later restoration must recreate the original lists, not merely equivalent lists.
When step L12 restores the search state, the recorded information is processed in reverse order. The variable $X$ is first returned to the free list at the saved position. Then every deleted $\operatorname{TIMP}$ entry is reinserted into its former list position. Reinserting in reverse order restores the exact previous ordering, because the positions refer to the lists before the deletions occurred.
After restoration, the free list again contains exactly the variables that were free before step L7, and every $\operatorname{TIMP}$ list again contains exactly the same pairs as before the assignment of $X$. Hence the data structures after L12 are identical to those that existed immediately before the corresponding execution of L7.
The two operations are inverses: L7 removes precisely the entries whose literals depend on $X$, and L12 restores precisely those entries from the stored undo information. Therefore backtracking returns Algorithm L to the same state it would have had if the decision on $X$ had never been made.
This completes the proof. ∎