TAOCP 7.2.2.2 Exercise 273
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 273. [27] [27] A clause $C$ that is learned from $waerden(j, k; n)$ is valid also with respect to $waerden(j, k; n')$ when $n' > n$; and so are the clauses $C + i$ that are obtained by adding $i$ to each literal of $C$, for $1 \le i \le n' - n$. For example, the fact that '35' follows from $waerden(3, 3; 7)$ allows us to add the clauses 35, 46, 57 to $waerden(3, 3; 9)$.
a) Exploit this idea to speed up the calculation of van der Waerden numbers.
b) Explain how to apply it also to bounded model checking.
Verified: no
Solve time: 6m01s
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. ∎