TAOCP 7.2.2.2 Exercise 257

Section 7.2.2.2: Satisfiability

Exercise 257. ▶ [30] (Niklas Sörensson.) A literal $l$ is said to be redundant, with respect to a given clause $c$ and the current trail, if $l$ is in the trail and either (i) $l$ is defined at level 0, or (ii) $l$ is not a decision literal and every false literal in $l$'s reason is either in $c$ or (recursively) redundant. (This definition is stronger than the special cases by which (115) reduces to (116), because $l$ itself needn't belong to $c$.) If, for example, $c = (l^7 \vee b_2 \vee b_2' \vee b_3 \vee b_4)$, let the reason for $l^7$ be $(b_1 \vee b_1' \vee \bar{a_1})$, where the reason for $a_1$ is $(a_1 \vee b_2 \vee \bar{a_2})$ and the reason for $a_2$ is $(a_2 \vee b_3 \vee \bar{b_4})$. Then $b_4$ is redundant, because $a_2$ and $\bar{a_1}$ are redundant.

a) Suppose $c = (l^7 \vee b_1 \vee \cdots \vee b_r)$ is a newly learned clause. Prove that if $b_j \in c$ is redundant, some other $b_i \in c$ became false on the same level as $b_j$ did. b) Devise an efficient algorithm that discovers all of the redundant literals $b_i$ in a given newly learned clause $c = (l^7 \vee b_1 \vee \cdots \vee b_r)$. Hint: Use stamps.

Verified: yes
Solve time: 4m43s

Setup

Let

$$ c=(l^7\vee b_1\vee\cdots\vee b_r) $$

be the newly learned clause produced by conflict analysis. The literal $l^7$ is the asserting literal, and every $b_i$ is false on the current trail. Let $\operatorname{lev}(u)$ denote the decision level at which the literal $u$ was assigned.

A literal $u$ is redundant with respect to $c$ when $u$ occurs in the trail and either $u$ has level $0$, or $u$ is not a decision literal and every false literal in its reason is either a member of $c$ or recursively redundant.

For the stamping algorithm, it is necessary to distinguish two different properties. A literal being in $c$ means that it may terminate a recursive redundancy check. It does not mean that the literal itself is redundant. Therefore we maintain one mark for membership in $c$ and a separate stamp for literals proved redundant.

Solution

(a)

Suppose that $b_j\in c$ is redundant. We prove that there is some $b_i\in c$, $i\ne j$, that became false on the same decision level as $b_j$.

First consider the level of $b_j$. A nonasserting literal of a learned clause is false at the moment of conflict analysis. If it had level $0$, then it would remain false independently of all current decisions. Such a literal would already participate in a conflict before the current search branch, so it cannot occur as one of the nonasserting literals of the learned clause generated from the present conflict. Hence

$$ \operatorname{lev}(b_j)>0 . $$

Because $b_j$ is redundant and has positive level, it is not a decision literal. Let its reason be

$$ (b_j\vee q_1\vee\cdots\vee q_s), $$

where each $q_k$ is false on the current trail.

A CDCL trail has the property that every propagated literal at a positive level has a reason containing a false literal assigned at the same level. To see this, suppose that all false literals in the reason of a propagated literal $u$ at level $d>0$ had levels smaller than $d$. Removing the decision assignment that created level $d$ would leave all literals of the reason except $u$ false, so unit propagation would have forced $u$ before reaching level $d$. This contradicts the definition of the trail level of $u$. Therefore there is some $q_k$ satisfying

$$ \operatorname{lev}(q_k)=\operatorname{lev}(b_j). $$

The literal $q_k$ is one of the false literals in the reason of $b_j$. By redundancy of $b_j$, either

$$ q_k\in c, $$

or $q_k$ is recursively redundant.

If $q_k\in c$, then $q_k=b_i$ for some $i\ne j$, and

$$ \operatorname{lev}(b_i)=\operatorname{lev}(b_j). $$

This gives the required literal.

It remains to consider the case in which $q_k$ is recursively redundant. Since $q_k$ has positive level and is redundant, the same argument applied to $q_k$ gives a false literal in the reason of $q_k$ whose level is

$$ \operatorname{lev}(q_k)=\operatorname{lev}(b_j). $$

If that literal belongs to $c$, it is the desired $b_i$. Otherwise it is recursively redundant, and the argument continues.

The implication graph is acyclic because every reason of a propagated literal contains only literals assigned earlier on the trail. Therefore this recursive process must terminate. It cannot terminate at a decision literal, because every literal in the chain is redundant and redundant literals at positive levels are not decisions. It cannot terminate at a new positive-level literal outside the chain, because every literal encountered through a redundancy expansion is required to be either in $c$ or redundant. Consequently the process reaches a literal in $c$.

The reached literal cannot be $b_j$ itself, because a reason clause for $b_j$ cannot contain $b_j$ as a false literal. Therefore it is some $b_i$ with

$$ i\ne j. $$

Every step of the chain preserves the decision level because each step chooses a false literal in a reason at the same level as the literal whose reason is being examined. Hence

$$ \operatorname{lev}(b_i)=\operatorname{lev}(b_j). $$

Thus some other literal of the learned clause became false on the same level as $b_j$.

This completes the proof. ∎

(b)

We construct an algorithm using stamps.

Maintain two kinds of information for each literal in the current trail. First, maintain a Boolean flag $\operatorname{inC}(u)$ that is true exactly for literals occurring in the learned clause $c$. Second, maintain a stamp value $\operatorname{stamp}(u)$, initially different from the current search stamp $s$, for literals that have been proved redundant.

The flag $\operatorname{inC}$ is only a terminal test. It is never interpreted as proving redundancy.

The algorithm scans the trail backwards, starting with the assignment immediately preceding the asserting literal $l^7$. For each literal $u$ encountered, perform the following test.

If $\operatorname{lev}(u)=0$, set

$$ \operatorname{stamp}(u)\leftarrow s . $$

This is valid because condition (i) of the definition applies.

If $u$ is a decision literal at positive level, leave it unstamped.

Otherwise inspect the reason clause of $u$. For every false literal $v$ in that reason, check whether either

$$ \operatorname{inC}(v)=1 $$

$$ \operatorname{stamp}(v)=s . $$

If all false literals in the reason satisfy one of these two conditions, set

$$ \operatorname{stamp}(u)\leftarrow s . $$

After the scan finishes, the redundant literals among the nonasserting literals of $c$ are exactly those $b_i$ satisfying

$$ \operatorname{stamp}(b_i)=s . $$

We prove correctness.

First suppose that the algorithm stamps a literal $u$. If $\operatorname{lev}(u)=0$, then $u$ is redundant by condition (i). Otherwise $u$ was not a decision literal, and every false literal in its reason was either in $c$ or had already received the current stamp. Since the scan proceeds backwards through the trail, every already stamped false literal was assigned earlier than $u$. By induction on the reverse trail order, every such stamped literal is redundant. Therefore every false literal in the reason of $u$ is either in $c$ or redundant, so $u$ is redundant by condition (ii).

Now suppose that $u$ is redundant. We prove that the algorithm stamps $u$. If $u$ has level $0$, it is stamped immediately. Otherwise $u$ is not a decision literal, and every false literal in its reason is either in $c$ or recursively redundant. Every recursively redundant literal in the reason occurs earlier on the trail because reasons only contain earlier assignments. By induction on the trail position, each such predecessor has already received the current stamp before $u$ is examined. Hence every false literal in the reason passes the test, and the algorithm stamps $u$.

Therefore the algorithm stamps exactly the redundant literals.

The running time is linear in the part of the implication graph reached by the learned clause. Each trail literal is examined once during the backward scan. Each reason clause is scanned only when its assigned literal is examined, and each false literal occurrence in those reasons is checked once. The membership flags $\operatorname{inC}$ and the redundancy stamps make every recursive dependency test constant time.

This completes the proof. ∎

Verification

The distinction between $\operatorname{inC}$ and $\operatorname{stamp}$ is essential. A literal in the learned clause is an allowed endpoint of a redundancy proof, but it need not itself satisfy the redundancy definition. The algorithm therefore uses clause membership only while checking reasons and uses stamps only for literals that have been independently certified redundant.

The proof of part (a) depends only on the CDCL invariant that a propagated literal at positive level has a reason containing a false literal at the same level. The recursive redundancy definition then forces a same-level path through the implication graph until another literal of the learned clause is reached.

The proof of part (b) establishes both directions. Every stamped literal satisfies the definition of redundancy, and every redundant literal is eventually stamped because all of its recursive dependencies occur earlier on the trail.

Notes

The stamp method is a memoized form of the recursive redundancy definition. The same idea appears in practical CDCL solvers when minimizing learned clauses: literals that can be justified entirely by the learned clause itself or by already certified redundant literals can be removed without changing the clause's asserting behavior.