TAOCP 7.2.2.2 Exercise 271
Let $C_{i-1}$ be the learned clause that is currently the last clause in MEM, and let $C_i$ be the next learned clause produced by step C9.
Section 7.2.2.2: Satisfiability
Exercise 271. ▶ [25] [25] The sequence of learned clauses $C_1, C_2, \ldots$ often includes cases where $C_i$ subsumes its immediate predecessor, $C_{i-1}$. In such cases we might as well discard $C_{i-1}$, which appears at the very end of MEM, and store $C_i$ in its place, unless $C_{i-1}$ is still in use as a reason for some literal on the trail. (For example, more than 8,600 of the 52,000+ clauses learned during the solution of Langford(7) by Algorithm C can be discarded in this way. Such discards are different from the on-the-fly subsumptions considered in exercise 270, because the subsumed $C_{i-1}$ includes only one literal from its original conflict level; furthermore, learned clauses have usually been significantly simplified by the procedure of exercise 257, unless they're trivial.)
Design an efficient way to discover when $C_{i-1}$ can be safely discarded.
Verified: no
Solve time: 4m23s
Solution
Let $C_{i-1}$ be the learned clause that is currently the last clause in MEM, and let $C_i$ be the next learned clause produced by step C9. We need to detect whether
$$ C_i \subseteq C_{i-1}. $$
If this inclusion holds, $C_{i-1}$ is unnecessary unless some literal on the current trail still has $C_{i-1}$ as its reason.
The data structure needed is a temporary occurrence mark for the literals of $C_i$. During step C9, after the new learned clause $C_i$ has been constructed, mark every literal occurring in $C_i$. The number of marks made is exactly $|C_i|$, because each learned clause contains strictly distinct literals. The old clause $C_{i-1}$ can then be tested by scanning its literals once. If every literal of $C_{i-1}$ is marked, then
$$ C_{i-1}\subseteq C_i. $$
For the required direction, however, we need the opposite containment. Therefore the test must instead mark the literals of $C_{i-1}$ before the new clause is written into MEM. After marking the literals of $C_{i-1}$, scan $C_i$. If every literal of $C_i$ is marked, then
$$ C_i\subseteq C_{i-1}. $$
The marking operation is performed only on the last learned clause, so it requires time proportional to the length of the clauses involved.
The remaining condition concerns whether $C_{i-1}$ is still used as a reason. Each propagated literal on the trail stores a pointer to its reason clause. During the same test, keep a count of trail literals whose reason pointer equals the address of $C_{i-1}$. If this count is nonzero, $C_{i-1}$ cannot be removed because deleting it would leave a trail literal without its justification.
If the containment test succeeds and the reason count is zero, the old clause can be discarded. Since $C_{i-1}$ is the last clause in MEM, no relocation of later clauses is needed. The new clause $C_i$ is stored at the location occupied by $C_{i-1}$, and all references to the old end of MEM continue to refer to the replacement clause.
The complete modification of step C9 is therefore as follows. After constructing the learned clause $C_i$, mark all literals of the preceding learned clause $C_{i-1}$. Scan $C_i$ and reject the replacement if a literal of $C_i$ is unmarked. Otherwise inspect the reason pointers on the trail. If none points to $C_{i-1}$, replace $C_{i-1}$ by $C_i$ in its MEM location; otherwise append $C_i$ normally.
The marking test is correct because it accepts exactly when every literal of $C_i$ occurs in $C_{i-1}$, which is the definition of subsumption by $C_i$. The reason-pointer test is correct because a clause with no remaining reason references has no active dependency from the current implication trail. The replacement preserves every clause required by the solver, and it removes precisely those learned clauses that are immediately subsumed and no longer needed.
This completes the proof. ∎