TAOCP 7.2.2.2 Exercise 284

Section 7.2.2.2: Satisfiability

Exercise 284. [23] Given $F$ and $(C_1, \ldots, C_t)$, a certificate-checking program tests condition (119) by verifying that $F$ and clauses $C_1, \ldots, C_{i-1}$ will force a conflict when they are augmented by the unit literals of $\bar{C}i$. While doing this, it can mark each clause of $F \cup {C_1, \ldots, C{i-1}}$ that was reduced to a unit during the forcing process; then the truth of $C_i$ does not depend on the truth of any unmarked clause.

In practice, many clauses are never marked. Removing all clause $F$ will remain unsatisfiable even if we leave them out. Furthermore, many clauses $C_i$ are not marked during the verification of any of their successors, ${C_{i+1}, \ldots, C_t}$; such clauses $C_i$ needn't be verified, nor need we mark any of the clauses on which they depend.

Therefore we can save work by checking the certificate backwards: Start by marking the final clause $C_t$, which is $\epsilon$ and clearly needs to be verified. Then, for $i = t, t-1, \ldots$, check $C_i$ only if it has been marked.

The unit propagations can all be done without recording the "reason" $R_l$ that has caused any literal $l$ to be forced. In practice, however, many of the forced literals don't actually contribute to the conflicts that arise, and we don't want to mark any clauses that aren't really involved.

Explain how to use reasons, as in Algorithm C, so that clauses are marked by the verifier only if they actually participate in the proof of a marked clause $C_i$.

Verified: no
Solve time: 3m47s

Solution

The statement is true.

Let $L={l_1,\ldots,l_r}$ be a set of strictly distinct literals. The restriction $F|L$ is obtained by setting every literal in $L$ to true, deleting every clause that contains one of these literals, and deleting from the remaining clauses every literal whose complement belongs to $L$. The strict distinctness of $L$ guarantees that these assignments do not conflict.

Suppose first that

$$ (F|L)\vdash_1 \epsilon . $$

Consider the formula $F\wedge L$, where each member of $L$ is regarded as a unit clause. Unit propagation on $F\wedge L$ can first derive the literals of $L$ from these unit clauses. After these $r$ propagations, every clause of $F$ has been simplified exactly according to the definition of restriction, so the remaining clauses are precisely $F|L$. Any subsequent sequence of unit propagations that derives $\epsilon$ from $F|L$ is therefore also a valid sequence of unit propagations from $F\wedge L$. Hence

$$ F\wedge L\vdash_1\epsilon . $$

For the converse, suppose that

$$ F\wedge L\vdash_1\epsilon . $$

During any unit propagation process on $F\wedge L$, the unit clauses in $L$ are available from the beginning. Apply these unit clauses first. The resulting formula is exactly $F|L$. Unit propagation does not lose any possible unit consequences by performing these forced assignments first, because every later clause produced by unit propagation is obtained only by deleting falsified literals and discarding clauses already satisfied by assigned literals. These are exactly the transformations performed in forming $F|L$.

Therefore, if a unit propagation derivation from $F\wedge L$ reaches the empty clause, the same derivation after the initial propagation of all literals in $L$ gives a unit propagation derivation of the empty clause from $F|L$. Consequently,

$$ (F|L)\vdash_1\epsilon . $$

Both implications hold, and therefore

$$ F\wedge L\vdash_1\epsilon \iff (F|L)\vdash_1\epsilon . $$

This completes the proof.

∎