TAOCP 7.2.2.2 Exercise 291
Algorithm C maintains a trail of assigned literals together with decision levels and reasons for forced assignments.
Section 7.2.2.2: Satisfiability
Exercise 291. [20] In the text's hypothetical scenario about flushing Table 3 back to level 15, why will 49 soon appear on the trail, instead of $\overline{49}$?
Verified: no
Solve time: 4m45s
Solution
Algorithm C maintains a trail of assigned literals together with decision levels and reasons for forced assignments. A flush operation removes assignments from the end of the trail back to a specified decision level, while preserving the clauses and the activity information used for later choices.
In the scenario described in the text, the trail is flushed back to level $15$. The literal $49$ is not forced immediately by a clause; instead, it is selected again by the branching mechanism after the flush. The reason is that flushing removes the old assignment of variable $49$, so $49$ becomes an unassigned variable. The variable activity values are not erased by the flush, because activity records are global information accumulated from earlier conflicts.
Algorithm C chooses the next decision variable from the unassigned variables with maximum activity, using the HEAP data structure. The variable $49$ has high activity in the hypothetical state shown in Table 3, so after the flush it remains a preferred candidate. Therefore the next branching decision again chooses the variable $49$.
The sign of the new literal is determined by the saved phase information, not by the fact that the opposite literal $\overline{49}$ was removed during the flush. During the previous search, the literal $49$ had been selected as the preferred phase for this variable. Algorithm C preserves that phase information when it flushes the trail. When variable $49$ is selected again, the saved phase causes the algorithm to assign $49$, not $\overline{49}$.
The distinction is that flushing changes the current assignment state, but it does not reset the heuristic state. The variable $49$ is therefore treated as a newly unassigned variable with its previous activity score and preferred phase still available. The next decision reproduces the literal $49$ on the trail.
Hence the literal that soon appears is
$$ \boxed{49} $$
rather than $\overline{49}$, because the flush removes the old trail entry but leaves the activity and phase data that cause Algorithm C to choose the positive literal again.