TAOCP 7.2.2.2 Exercise 271
Let $C_{i-1}$ denote the clause currently at the end of MEM when the new learned clause $C_i$ has been produced.
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: 8m45s
Solution
Let $C_{i-1}$ denote the clause currently at the end of MEM when the new learned clause $C_i$ has been produced. The only possible replacement is
$$ C_{i-1}\leftarrow C_i, $$
and this replacement is valid exactly when
$$ C_i\subseteq C_{i-1} $$
and no literal on the trail has $C_{i-1}$ as its reason.
The first condition can be tested without comparing every previously learned clause. Since only the immediate predecessor is involved, we need only inspect the literals in $C_i$ and $C_{i-1}$.
Assign a temporary integer label to each possible literal. When $C_i$ is generated, increase a global counter $s$ and set
$$ \operatorname{mark}(l)\leftarrow s $$
for every literal $l\in C_i$. Then scan the literals of $C_{i-1}$. The clause $C_i$ subsumes $C_{i-1}$ precisely when every literal of $C_i$ is also found in $C_{i-1}$. Equivalently, after marking $C_{i-1}$ instead, the test is
$$ \operatorname{mark}(l)=s \qquad\text{for every }l\in C_i . $$
The marking can be done in time proportional to the lengths of the two clauses:
$$ O(|C_i|+|C_{i-1}|). $$
No search through the rest of MEM is necessary.
The second condition is checked by keeping a count
$$ \operatorname{use}(C) $$
for each learned clause $C$. Whenever a trail literal receives a reason pointer to $C$, increment $\operatorname{use}(C)$. Whenever that reason pointer is removed during backtracking, decrement it. The clause $C_{i-1}$ is not removable while
$$ \operatorname{use}(C_{i-1})>0 . $$
When $C_i$ has been learned, the solver performs the following test:
If
$$ C_i\subseteq C_{i-1} $$
and
$$ \operatorname{use}(C_{i-1})=0, $$
then the old clause is discarded and the space at the end of MEM is reused for $C_i$. Otherwise $C_i$ is stored normally.
The correctness follows from the subsumption property. If
$$ C_i\subseteq C_{i-1}, $$
then every assignment satisfying $C_i$ also satisfies $C_{i-1}$, because $C_i$ has fewer literals and is therefore the stronger clause. Hence deleting $C_{i-1}$ preserves the set of satisfying assignments. The only obstruction is a trail reason pointer, because the conflict analysis and propagation procedures may still need the old clause as an explanation. The condition
$$ \operatorname{use}(C_{i-1})=0 $$
removes exactly this obstruction.
Therefore the solver can detect safe discards by a linear-time subset test on the two consecutive learned clauses together with a constant-time check of the reason-use counter. This gives an efficient implementation of the optimization described in the exercise. ∎