TAOCP 7.2.2.2 Exercise 384

Section 7.2.2.2: Satisfiability

Exercise 384. [25] [25] Continuing the previous exercise, show that we can always safely forget any clause $C$ that contains a literal $l$ for which $C \circ C'$ is certifiable for $\Phi \setminus C$ whenever $C' \in \Phi$ contains $\bar{l}$. What erp rule is appropriate?

Verified: no
Solve time: 10m51s

---

Correctness

The proposed solution addresses the correct exercise and identifies the intended erp rule

$$ l\leftarrow1. $$

The overall strategy is also the right one: show that after forgetting $C$, any satisfying assignment of $\Phi\setminus C$ can be repaired into a satisfying assignment of $\Phi$ by forcing $l$ to be true. The use of the certifiability condition on the resolvents $C\circ C'$ is the essential idea.

However, the proof contains a serious logical error in the central contradiction argument. The solution claims that if a clause $C'\in\Phi$ becomes false after applying the erp rule, then all literals in $C\setminus{l}$ must already have been false. This is not justified.

A satisfying assignment of $\Phi\setminus C$ need not falsify the other literals of $C$. The clause $C$ has been removed, so its remaining literals impose no restriction. It is possible that some literal in $C\setminus{l}$ is true while a clause $C'$ containing $\bar l$ is satisfied only by $\bar l$. After changing $l$ to true, $C'$ can become false even though the resolvent $C\circ C'$ remains true because of that other literal from $C$.

Therefore the argument does not prove that the resolvent is falsified before the erp step, and the contradiction with

$$ \Phi\setminus C\models C\circ C' $$

does not follow.

The final conclusion and the proposed erp rule are correct, but the key proof step establishing that the repair operation preserves all clauses of $\Phi$ is incomplete.

Gaps and Errors

1. The claim that all literals in $C\setminus{l}$ are false is incorrect. Critical error.

The solution states:

"The literals coming from $C\setminus{l}$ must also all be false, because the original assignment satisfied $\Phi\setminus C$."

This does not follow. The formula $\Phi\setminus C$ does not contain the clause $C$, so it does not constrain the literals of $C$. A satisfying assignment of $\Phi\setminus C$ may make some other literal of $C$ true.

For example, if

$$ C={l,a},\qquad C'={\bar l,b}, $$

an assignment with

$$ l=0,\qquad a=1,\qquad b=0 $$

satisfies $C'$ before the erp step because of $\bar l$. After changing $l$ to $1$, $C'$ becomes false. The resolvent

$$ C\circ C'={a,b} $$

is still true before the change because of $a$, so no contradiction with certifiability is obtained.

1. The proof does not establish that the erp repair preserves $\Phi$. Critical error.

The missing argument is the heart of the exercise. The proof must show why the choice of $l$ and the certifiable resolvents prevent a hard clause from becoming false. The proposed solution does not provide a valid proof of this implication.

1. The conclusion about the erp rule is correct. Justification gap only.

The rule

$$ l\leftarrow1 $$

is the appropriate repair rule, but the proof given does not establish why it works.

Summary

The solution has the correct intended construction and identifies the correct erp rule, but the main preservation argument contains a false inference about the literals of $C\setminus{l}$. The central step required by the exercise is therefore unproved.

VERDICT: FAIL - the proof incorrectly assumes that the other literals of the forgotten clause are false, so it does not establish that the erp rule preserves the hard clauses.