TAOCP 7.2.2.2 Exercise 273
Let $W_n=waerden(j,k;n)$ denote the clause set expressing that a binary string $x_1,\ldots,x_n$ contains no arithmetic progression of length $j$ consisting entirely of one value or no arithmetic progr...
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: 1m48s
Setup
Let $W_n=waerden(j,k;n)$ denote the clause set expressing that a binary string $x_1,\ldots,x_n$ contains no arithmetic progression of length $j$ consisting entirely of one value or no arithmetic progression of length $k$ consisting entirely of the other value. A learned clause $C$ from Algorithm C for $W_n$ is a logical consequence of $W_n$.
The exercise asks how to use the fact that such a learned clause remains valid for every larger instance $W_{n'}=waerden(j,k;n')$ with $n'>n$, and how the same principle applies to bounded model checking.
Solution
Suppose Algorithm C has learned a clause $C$ while solving $W_n$. Since learned clauses are derived by resolution from clauses already present, we have
$$ W_n\models C. $$
Every clause of $W_n$ is also a clause of $W_{n'}$ restricted to the variables $x_1,\ldots,x_n$. The additional variables $x_{n+1},\ldots,x_{n'}$ create new arithmetic progressions, but they do not change the truth of any clause that only contains literals from the first $n$ variables.
To prove that $C$ remains valid for $W_{n'}$, consider an arbitrary satisfying assignment $\alpha$ of $W_{n'}$. Restrict $\alpha$ to the variables $x_1,\ldots,x_n$. Every forbidden arithmetic progression among these variables is also a forbidden arithmetic progression in $W_{n'}$, so the restricted assignment satisfies $W_n$. Since
$$ W_n\models C, $$
the restriction satisfies $C$. Therefore the original assignment $\alpha$ satisfies $C$, because $C$ contains only literals from the first $n$ variables. Hence
$$ W_{n'}\models C . $$
Now consider a clause $C+i$, obtained by adding $i$ to every literal of $C$, where
$$ 1\le i\le n'-n. $$
The shift operation replaces every variable $x_t$ in $C$ by $x_{t+i}$. Let the shifted clause be denoted by
$$ C+i. $$
The shifted clause corresponds to the same logical relation applied to the block of variables
$$ x_{1+i},x_{2+i},\ldots,x_{n+i}. $$
The clauses of $waerden(j,k;n')$ are translation invariant inside this range: every arithmetic progression of the first $n$ positions has a corresponding arithmetic progression after shifting by $i$. Therefore every assignment satisfying $W_{n'}$ also satisfies the shifted copy of $W_n$ on these variables.
Let $\alpha$ be any satisfying assignment of $W_{n'}$. Define a new assignment $\beta$ on $x_1,\ldots,x_n$ by
$$ \beta(x_t)=\alpha(x_{t+i}). $$
The assignment $\beta$ satisfies $W_n$, because every forbidden progression in the shifted block would otherwise give a forbidden progression in $W_{n'}$. Since
$$ W_n\models C, $$
we have
$$ \beta\models C. $$
By the definition of $\beta$, this means that
$$ \alpha\models C+i. $$
Therefore
$$ W_{n'}\models C+i. $$
This gives a method for speeding up the computation of van der Waerden numbers. Suppose Algorithm C solves $W_n$ and learns a collection of clauses
$$ C_1,C_2,\ldots,C_s . $$
When solving the next larger instance $W_{n+1}$, initialize the clause database with the old learned clauses and their shifts that fit inside the new range. For each learned clause $C_t$, insert
$$ C_t $$
and every translated clause
$$ C_t+i,\qquad 1\le i\le n'-n, $$
that uses only variables up to $n'$. These clauses are already consequences of $W_{n'}$, so Algorithm C begins with information obtained from the previous computation.
For a sequence of increasing instances
$$ waerden(j,k;n),waerden(j,k;n+1),\ldots , $$
this method allows information from smaller instances to accumulate. The solver does not need to rediscover local contradictions that already appeared at smaller values of $n$.
The same idea applies to bounded model checking. In bounded model checking, a transition system is encoded as a Boolean formula describing executions of length $n$. A learned clause obtained while proving that no bad state is reachable within depth $n$ is a consequence of the transition relation together with the initial-state constraints and therefore can remain useful at larger depths when the same portion of the execution is present.
Let $B_n$ denote the bounded model checking formula for depth $n$. If Algorithm C learns
$$ B_n\models C, $$
then the clause can be reused in a larger formula $B_{n'}$ whenever the variables appearing in $C$ have the same interpretation in the larger encoding. If the encoding is time-indexed, the analogous operation is to shift the clause from one time interval to another, exactly as $C+i$ shifts the literals of a $waerden(j,k;n)$ clause.
Thus the learned clauses from earlier bounds become additional constraints for later bounds. They can eliminate repeated searches through executions that were already proved impossible. The method is especially effective when successive bounded model checking formulas differ only by extending the time horizon, because the old constraints remain embedded in the new instance.
Verification
The validity of $C$ for $W_{n'}$ depends only on the fact that every satisfying assignment of $W_{n'}$ restricts to a satisfying assignment of $W_n$. The proof does not depend on the particular derivation used by Algorithm C, only on the soundness of learned clauses.
The validity of $C+i$ follows from the same argument after applying the index translation
$$ t\mapsto t+i . $$
The translation preserves the structure of arithmetic progressions, so every forbidden pattern represented by the smaller instance appears in the corresponding shifted variables of the larger instance.
The reuse strategy cannot make Algorithm C incorrect because every inserted clause is already implied by the current formula. The only change is that the solver begins with additional consequences that it might otherwise rediscover.
This completes the proof.
∎
Notes
The same principle can be extended beyond simple translations. Whenever a family of SAT instances has a symmetry or embedding relation, learned clauses from one instance may be transported through that relation and reused in another instance. Reflection, translation, and other automorphisms of the underlying combinatorial object provide systematic sources of additional learned clauses.