TAOCP 7.2.2.2 Exercise 269
Let the conflict graph of Algorithm C be viewed as an implication graph.
Section 7.2.2.2: Satisfiability
Exercise 269. [29] [29] Suppose Algorithm C reaches a conflict at level $d$ of the trail, after having chosen the decision literals $u_1, u_2, \ldots, u_d$. Then the "trivial clause" $(\bar{l}^0 \vee \bar{u}_1 \vee \cdots \vee \bar{u}_d)$ must be true if the given clauses are satisfiable, where $l'$ and $d'$ are defined in step C7.
a) Show that, if we start with the clause $(\bar{l}^0 \vee \bar{b}_1 \vee \cdots \vee \bar{b}_r)$ that is obtained in step C7 and keep resolving it against with other already-known clauses, we can always reach a clause that subsumes the trivial clause.
b) Sometimes, as in [115], the clause that is slated to be learned in step C9 is much longer than the trivial clause. Construct an example in which $d = 3$, $d' = 1$, and $r = 10$, yet none of $b_1, \ldots, b_r$ are redundant in the sense of exercise 257.
c) Suggest a way to improve Algorithm C accordingly.
Verified: no
Solve time: 12m17s
Solution
Let the conflict graph of Algorithm C be viewed as an implication graph. The decision literals on the trail are
$$ u_1,u_2,\ldots,u_d . $$
A conflict at level $d$ means that the current trail contains a set of literals whose conjunction implies both $x$ and $\bar x$ for some variable $x$. The clause
$$ (\bar l^0\vee \bar u_1\vee\cdots\vee \bar u_d) $$
is the trivial clause associated with this contradiction: if all decision literals $u_1,\ldots,u_d$ and the literal $l^0$ were true, then the conflict would occur. Hence any satisfying assignment must make at least one of these literals false.
(a)
Step C7 starts conflict analysis from a clause
$$ C_0=(\bar l^0\vee \bar b_1\vee\cdots\vee\bar b_r). $$
The literals $b_i$ are obtained by repeatedly resolving the conflict clause with the reason clauses of literals already implied on the trail. Each resolution step replaces an implied literal by the literals that caused its implication.
Consider the reverse direction of the implication graph. Every nondecision literal on the trail has a reason clause. If a literal $x$ occurs in the current conflict clause, resolving with the reason clause of $x$ removes $x$ and inserts the literals that imply $x$. Repeating this operation eventually reaches only decision literals, because every path in the implication graph terminates at a decision node.
The initial clause $C_0$ is therefore transformed, by a finite sequence of resolution steps, into a clause consisting only of the negations of literals on the decision trail that are responsible for the conflict. The conflict can occur only when
$$ l^0,u_1,\ldots,u_d $$
are simultaneously true. Hence the resulting clause is implied by the formula and must be a subclause of
$$ (\bar l^0\vee\bar u_1\vee\cdots\vee\bar u_d). $$
Equivalently, after continuing the resolutions far enough, we obtain a clause $C$ satisfying
$$ C\subseteq {\bar l^0,\bar u_1,\ldots,\bar u_d}. $$
Therefore $C$ subsumes the trivial clause.
(b)
The point of this example is that the clause produced by C7 need not be close to the shortest possible conflict clause.
Take three decision levels
$$ u_1,\qquad u_2,\qquad u_3 $$
with
$$ d=3. $$
Let $l^0$ be an implied literal at level $3$, and suppose that its reason clause is
$$ (\bar l^0\vee b_1\vee\cdots\vee b_{10}). $$
Assume that each $b_i$ is implied at level $1$ from the decision literal $u_1$ by a separate reason clause
$$ (\bar u_1\vee b_i), \qquad 1\le i\le10 . $$
Let the conflict clause be
$$ (l^0). $$
The implication graph is therefore
$$ u_1\longrightarrow b_1,\ldots,b_{10} \longrightarrow l^0 \longrightarrow \text{conflict}. $$
The first conflict-analysis step produces
$$ (\bar l^0\vee b_1\vee\cdots\vee b_{10}), $$
so here
$$ r=10. $$
All the $b_i$'s are at level $1$, hence
$$ d'=1. $$
The trivial clause is
$$ (\bar l^0\vee\bar u_1\vee\bar u_2\vee\bar u_3). $$
Resolving the ten reason clauses
$$ (\bar u_1\vee b_i) $$
against the learned clause removes the ten $b_i$'s and produces a clause containing $\bar u_1$, which is a subclause of the trivial clause.
However, none of the $b_i$'s is redundant. To see this, fix an index $i$. Assign
$$ b_i=\text{true}, $$
and assign every other $b_j$ with $j\ne i$ false. The clause
$$ (\bar l^0\vee b_1\vee\cdots\vee b_{10}) $$
is then satisfied only because of $b_i$. If $b_i$ is deleted, the remaining literals do not prevent this assignment, and the implication of the conflict is lost. Thus each $b_i$ is essential in the learned clause according to the redundancy criterion of Exercise 257.
Hence the learned clause can have ten essential literals even though the trivial clause has only three decision literals.
(c)
Algorithm C can be improved by performing an additional minimization phase after C7 and before C9.
After obtaining
$$ (\bar l^0\vee\bar b_1\vee\cdots\vee\bar b_r), $$
the solver should attempt to remove literals whose presence is unnecessary. A literal $b_i$ can be tested for redundancy by temporarily assuming
$$ \bar b_1,\ldots,\bar b_{i-1},\bar b_{i+1},\ldots,\bar b_r $$
and checking whether they still imply the conflict. If they do, $b_i$ can be deleted.
Another possibility is to continue the resolution process beyond the first asserting clause until a smaller clause is obtained. The clause found in part (a) is guaranteed to subsume the trivial clause, so this additional resolution can only shorten the learned clause or leave it unchanged.
Therefore a modified version of C7 should include clause minimization, producing a smaller learned clause before the clause is recorded in C9. This reduces memory usage and usually improves later propagation because shorter clauses become unit clauses more often. $\square$