TAOCP 7.2.2.2 Exercise 274
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 274. [35] Algorithm C sets the "reason" for a literal $l$ as soon as it notices a clause that forces $l$ to be true. Later on, other clauses that force $l$ are often encountered, in practice; but Algorithm C ignores them, even though one of them might be a "better reason." (For example, another forcing clause might be significantly shorter.) Explore a modification of Algorithm C that tries to improve the reasons of non-decision literals.
Verified: no
Solve time: 5m42s
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. ∎