TAOCP 7.2.2.2 Exercise 385
Let $C$ be a clause in $\Phi$, and suppose that $C$ contains a literal $l$ such that $C\circ C'$ is certifiable for $\Phi\setminus C$ whenever $C'\in\Phi$ contains $\bar l$.
Section 7.2.2.2: Satisfiability
Exercise 385. [**] Clause $C$ is called certifiable for $F$ if $F \wedge C \vdash_1 c$, as in (119). It is said to be absorbed by $F$ if it is nonempty and $F \wedge C \vdash_1 l$ for every $l \in C$, or if it is empty and $F \vdash_1 \epsilon$. (Every clause of $F$ is obviously absorbed by $F$.)
a) True or false: If $C$ is absorbed by $F$, it is certifiable for $F$.
b) Which of ${1, 12, 123}$ are implied by, certifiable for, or absorbed by $H'$ in (7)?
c) If $C$ is certifiable for $F$ and if all clauses of $F$ are absorbed by $F'$, prove that $C$ is certifiable for $F'$.
d) If $C$ is absorbed by $F$ and if all clauses of $F$ are absorbed by $F'$, prove that $C$ is absorbed by $F'$.
Verified: no
Solve time: 5m46s
Solution
Let $C$ be a clause in $\Phi$, and suppose that $C$ contains a literal $l$ such that $C\circ C'$ is certifiable for $\Phi\setminus C$ whenever $C'\in\Phi$ contains $\bar l$. We prove that $C$ may be forgotten.
By the definition of certifiability used in the preceding exercise, every solution of $\Phi\setminus C$ also satisfies every clause $C\circ C'$ that is certifiable for $\Phi\setminus C$. Therefore, if an assignment satisfies $\Phi\setminus C$, it satisfies all clauses of the form $C\circ C'$ for which $C'\in\Phi$ contains $\bar l$.
Consider such an assignment, and suppose that $C$ is false under it. Write
$$ C={l}\cup D, $$
where $D$ contains the remaining literals of $C$. Since $C$ is false, $l$ is false and every literal in $D$ is false.
The assignment can be changed by applying the erp rule
$$ l\leftarrow 1. $$
After this replacement, $C$ is satisfied. It remains to prove that no clause of $\Phi\setminus C$ becomes false.
Only clauses containing $\bar l$ can be affected by this replacement. Let $C'\in\Phi$ contain $\bar l$. Before the replacement, $C'$ was satisfied because the assignment satisfied $\Phi\setminus C$. Assume that after the replacement $C'$ becomes false. Then every literal of $C'$ other than $\bar l$ is false, because $\bar l$ itself is false after $l\leftarrow1$.
The resolvent-like clause $C\circ C'$ consists of the literals of $C$ other than $l$ together with the literals of $C'$ other than $\bar l$. Under the original assignment, every literal in $D$ was false, and under the new assignment every literal of $C'$ other than $\bar l$ is false. Hence $C\circ C'$ would be false after the replacement. Since the replacement changed only the value of $l$, and $l$ does not occur in $C\circ C'$, the original assignment also made $C\circ C'$ false.
This contradicts the fact that every solution of $\Phi\setminus C$ satisfies $C\circ C'$. Therefore no clause $C'$ containing $\bar l$ can be falsified by the replacement.
If a solution of $\Phi\setminus C$ already satisfies $C$, the replacement is unnecessary. If it does not satisfy $C$, the rule $l\leftarrow1$ produces a solution satisfying $C$ while preserving every clause in $\Phi\setminus C$. Hence every solution of $\Phi\setminus C$ can be converted into a solution of $\Phi$.
The reverse implication is immediate because $\Phi$ contains all clauses of $\Phi\setminus C$. Therefore
$$ \Phi\text{ is satisfiable}\iff\Phi\setminus C\text{ is satisfiable}. $$
Thus $C$ may be safely forgotten, and the appropriate erp rule is
$$ \boxed{l\leftarrow1}. $$
This completes the proof. ∎