TAOCP 7.2.2.2 Exercise 284
During the verification of condition (119), the verifier performs unit propagation on $F \cup {C_1,\ldots,C_{i-1}}$ after adding the unit literals of $\bar{C}_i$.
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: 2m19s
Solution
During the verification of condition (119), the verifier performs unit propagation on $F \cup {C_1,\ldots,C_{i-1}}$ after adding the unit literals of $\bar{C}_i$. For every literal $l$ that becomes forced, associate a reason $R_l$. The reason is a clause that became unit and forced $l$ during the propagation, exactly as in Algorithm C.
The initial unit literals coming from $\bar{C}_i$ have no reason. Their status is different from propagated literals, because they are assumptions used to test whether $C_i$ follows from the preceding clauses. Thus the verifier stores $R_l=\varnothing$ for these literals.
Suppose a clause $D$ becomes unit after some literals have already been assigned. If the only unassigned literal in $D$ is $l$, then the propagation step forces $l$, and the verifier sets
$$ R_l \leftarrow D . $$
The set of reasons therefore forms a directed dependency structure: every propagated literal points to the clause that forced it, and every such clause points to the literals whose assignments reduced it to a unit clause.
When a conflict is reached, the conflicting clause $D$ has every literal falsified. The verifier does not mark every clause encountered during propagation. Instead, it traces dependencies backward from $D$. If a falsified literal $l$ in $D$ was an assumption from $\bar{C}_i$, the trace stops at that literal. If $l$ was propagated, the verifier marks $R_l$ and recursively traces the literals of $R_l$ that caused $R_l$ to become unit.
More explicitly, define a recursive marking procedure $\operatorname{mark}(D)$ for a clause $D$ participating in the conflict. The procedure first marks $D$. For every literal $l$ of $D$, if $R_l\ne\varnothing$, it applies $\operatorname{mark}(R_l)$, and otherwise no predecessor clause is marked. The recursion terminates because every reason clause was created earlier in the propagation process, so the dependency relation follows the order in which literals were forced and cannot contain a cycle.
After this backward traversal, exactly the clauses that contribute to the derivation of the conflict are marked. A clause is marked only if it is either the conflict clause itself or a reason needed to derive a literal that appears in a marked clause. Hence every marked clause lies on a dependency path from the conflict to the assumptions $\bar{C}_i$.
Conversely, consider any clause that actually participates in the proof of the conflict. If it is the final conflicting clause, it is marked initially. Otherwise it forced a literal $l$ that is needed by a later marked clause. Its identity is therefore stored as $R_l$, and the recursive procedure reaches it when tracing that later clause. Hence it is marked.
The verifier can therefore replace the previous rule, which marked every clause reduced to a unit during propagation, by reason-based marking. The resulting marked set is precisely the set of clauses that participate in the proof of the marked clause $C_i$.
This completes the proof. ∎