TAOCP 7.2.2.2 Exercise 277
A certificate of unsatisfiability $(C_1,\ldots,C_t)$ is a resolution refutation: each $C_i$ is either a clause of $F$ or a clause obtained from earlier clauses by one resolution step, and the final cl...
Section 7.2.2.2: Satisfiability
Exercise 277. [M18] If $(C_1, \ldots, C_t)$ is a certificate of unsatisfiability for $F$, and if all clauses of $F$ have length $\ge 2$, prove that some $C_i$ is a unit clause.
Verified: no
Solve time: 1m50s
Solution
A certificate of unsatisfiability $(C_1,\ldots,C_t)$ is a resolution refutation: each $C_i$ is either a clause of $F$ or a clause obtained from earlier clauses by one resolution step, and the final clause is the empty clause $\epsilon$. Thus $C_t=\epsilon$.
Assume that every clause of $F$ has length at least $2$. Suppose, for contradiction, that no clause in the certificate is a unit clause. Then every clause $C_i$, for $1\le i<t$, has length either $0$ or at least $2$. The only clause of length $0$ in a resolution refutation is the final clause $\epsilon$, because no earlier clause can already certify the contradiction.
Consider the resolution step that produces $C_t=\epsilon$. There must be two earlier clauses $C_a$ and $C_b$ and a literal $l$ such that the resolution of $C_a$ and $C_b$ on $l$ is
$$ (C_a-{l})\cup(C_b-{\bar l})=\epsilon . $$
The union is empty only when both sets are empty. Hence
$$ C_a={l},\qquad C_b={\bar l}. $$
Therefore $C_a$ and $C_b$ are unit clauses. Since $a,b<t$, at least one unit clause occurs among $C_1,\ldots,C_t$.
The assumption that no $C_i$ is a unit clause leads to a contradiction. Hence some $C_i$ in the certificate must be a unit clause.
This completes the proof.
∎