TAOCP 7.2.2.2 Exercise 269

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: 6m47s

Setup

Let the clause produced in step C7 be

$$ D=(\bar{l}^{,0}\vee\bar{b}_1\vee\cdots\vee\bar{b}_r). $$

The literals $b_1,\ldots,b_r$ are the literals that remain after the resolution steps of C7 have removed all literals at the current decision level except the literal $l^0$ chosen by the C7 stopping condition. Let

$$ T=(\bar{l}^{,0}\vee\bar{u}_1\vee\cdots\vee\bar{u}_d) $$

be the trivial clause associated with the decisions $u_1,\ldots,u_d$ that produced the conflict.

The proof of part (a) requires showing that the remaining literals in $D$ can always be eliminated or replaced by resolution until a clause contained in $T$ is obtained. Part (b) requires an example where the C7 clause is much larger than $T$, even though none of its remaining literals is redundant according to the criterion of exercise 257. Part (c) asks for a modification of Algorithm C that reduces such clauses.

Solution

(a)

Every literal placed on the trail by propagation, rather than by a decision, has a reason clause stored by Algorithm C. If a propagated literal $a$ was assigned because of a clause

$$ (a\vee C), $$

then every literal of $C$ is false on the trail at the moment when $a$ is propagated. Equivalently, the implication graph contains edges from the literals falsifying $C$ to $a$.

Suppose a nondecision literal $b_i$ occurs in the clause $D$. Since $b_i$ was propagated, its reason clause is available among the already-known clauses. Let that reason clause be

$$ (b_i\vee C_i). $$

The current clause contains $\bar{b}_i$, so resolving $D$ with this reason clause gives

$$ (D-{\bar{b}_i})\cup C_i . $$

The new clause is still implied by the original formula, because resolution preserves logical consequence. The resolution removes the occurrence of $\bar{b}_i$ and replaces it by literals corresponding to the causes of the propagation of $b_i$.

Apply this operation repeatedly. Every nondecision literal remaining in the clause has a reason clause, so every such literal can be resolved away. The only literals that cannot be eliminated in this manner are decision literals, because they have no reason clauses. The only decision literals in the trail are

$$ u_1,u_2,\ldots,u_d . $$

Therefore the repeated resolution process must eventually produce a clause of the form

$$ (\bar{l}^{,0}\vee S), $$

where every literal in $S$ belongs to

$$ {\bar{u}_1,\bar{u}_2,\ldots,\bar{u}_d}. $$

Hence

$$ (\bar{l}^{,0}\vee S) \subseteq (\bar{l}^{,0}\vee\bar{u}_1\vee\cdots\vee\bar{u}_d). $$

Thus a clause subsuming the trivial clause can always be reached by resolving the C7 clause against already-known clauses.

This completes the proof. ∎

(b)

We construct an implication graph with three decision levels and ten independent lower-level causes.

Let the decisions be

$$ u_1,\quad u_2,\quad u_3 $$

at levels $1$, $2$, and $3$, respectively. Introduce a literal $l^0$ at level $3$ with reason clause

$$ (\bar{u}_3\vee l^0). $$

Thus $u_3$ implies $l^0$.

Introduce ten literals

$$ b_1,b_2,\ldots,b_{10} $$

at level $0$. For each $i$, introduce a clause

$$ (\bar{b}_i\vee x_i) $$

where $x_i$ is a level-$0$ variable, and fix the initial level-$0$ assignments so that every $x_i=1$. Therefore each clause forces

$$ b_i=1 . $$

The ten literals $b_i$ are permanent consequences of the level-$0$ assignment and have no decision-level predecessors.

Now add the conflict clause

$$ (\bar{l}^{,0}\vee\bar{b}_1\vee\bar{b}2\vee\cdots\vee\bar{b}{10}). $$

Finally, add the decision chain

$$ (\bar{u}_1\vee u_2),\qquad (\bar{u}_2\vee u_3), $$

and choose

$$ u_1=1 . $$

The first two clauses propagate

$$ u_2=1,\qquad u_3=1, $$

and the reason clause for $l^0$ propagates

$$ l^0=1 . $$

The ten level-$0$ literals already satisfy

$$ b_1=b_2=\cdots=b_{10}=1 . $$

Therefore the conflict clause is falsified.

The trail contains the three decisions $u_1,u_2,u_3$, so

$$ d=3 . $$

The only literal in the conflict clause at the highest active decision level is $l^0$. Consequently the C7 stopping condition is reached immediately after resolving away any other level-$3$ literals, and

$$ d'=1 . $$

The literals $b_1,\ldots,b_{10}$ are already at lower levels and have no reason clauses that involve the other $b_j$. Hence C7 can leave the clause

$$ (\bar{l}^{,0}\vee\bar{b}1\vee\cdots\vee\bar{b}{10}), $$

$$ r=10 . $$

It remains to prove that none of these literals is redundant. Fix $i$. The only way to derive $b_i$ is through its own level-$0$ reason information. None of the literals

$$ l^0,b_1,\ldots,b_{i-1},b_{i+1},\ldots,b_{10} $$

has an implication path to $b_i$, because the ten level-$0$ implications are independent. Therefore the remaining literals of the learned clause do not imply $b_i$.

By the redundancy criterion of exercise 257, $\bar{b}_i$ is not redundant. The same argument applies to every

$$ i=1,2,\ldots,10 . $$

Thus the construction satisfies

$$ d=3,\qquad d'=1,\qquad r=10, $$

while none of

$$ b_1,\ldots,b_{10} $$

is redundant.

(c)

Algorithm C can be improved by inserting a clause-minimization phase between steps C7 and C9.

After C7 produces

$$ (\bar{l}^{,0}\vee\bar{b}_1\vee\cdots\vee\bar{b}_r), $$

each literal $\bar{b}_i$ is examined. If the remaining literals

$$ \bar{l}^{,0},\bar{b}1,\ldots,\bar{b}{i-1},\bar{b}_{i+1},\ldots,\bar{b}_r $$

already imply $\bar{b}_i$ through the implication graph, then $\bar{b}_i$ may be deleted. Otherwise it must remain.

The test uses the reason clauses stored by Algorithm C. A literal is removable precisely when its justification is already represented by other literals in the learned clause, so deleting it preserves the fact that the learned clause is implied by the original formula.

This minimization does not replace the resolution procedure of C7. Step C7 guarantees the asserting property by reducing the number of literals at the current decision level. The additional minimization step removes unnecessary literals at lower decision levels after that property has been obtained.

The modified algorithm therefore learns shorter clauses while preserving all logical consequences used by future conflict analysis.

This completes the proof. ∎

Verification

The argument in part (a) depends only on two properties of Algorithm C: every propagated literal has a recorded reason clause, and resolution with a reason clause eliminates that propagated literal while preserving implication. After all such resolutions, only decision literals can remain.

The construction in part (b) separates the current decision-level conflict analysis from lower-level literals. The three decisions create the conflict situation, the literal $l^0$ is the unique current-level literal, and the ten $b_i$ literals remain because they are independent consequences of level $0$. Their independence prevents any redundancy elimination based on the implication graph.

The modification in part (c) removes only literals whose logical consequences are already represented by the rest of the learned clause, so the learned clause remains valid for all future uses in Algorithm C.

Notes

The trivial clause provides an upper bound on the information needed to describe the conflict, but first-UIP learning does not always discover that smallest description. Clause minimization attempts to close this gap by using the implication graph after conflict analysis has already produced a valid learned clause.