TAOCP 7.2.2.2 Exercise 380
Let the original clause be C=(a\vee b\vee c\vee d), and let the shortened clause be
Section 7.2.2.2: Satisfiability
Exercise 380. [21] Sometimes we can use self-subsumption backwards, for example by weakening the clause $(l_1 \vee l_2 \vee l_k)$ to $(l_1 \vee \cdots \vee l_j)$ if each intermediate replacement of $(l_1 \vee \cdots \vee l_j)$ by $(l_1 \vee \cdots \vee l_{j-1})$ is justifiable for $3 < j \le k$. Then, if we're lucky, the clause $(l_1 \vee \cdots \vee l_j)$ is weak enough to be eliminated; in such cases we are allowed to eliminate $(l_1 \vee l_2 \vee l_k)$. a) Show that $(a \vee b \vee c)$ can be eliminated if it is accompanied by the additional clauses $(a \vee \bar{b} \vee d) \wedge (a \vee d \vee \bar{c})$, $(b \vee d \vee \bar{c})$. b) Show that $(a \vee b \vee c)$ can also be eliminated when accompanied by $(a \vee b \vee d)$, $(b \vee \bar{c} \vee d)$, $(b \vee c \vee \bar{e})$, provided that no other clauses contain $\bar{c}$.
c) What erp rules, if any, are needed for those eliminations?
Verified: no
Solve time: 5m42s
Solution
Let the original clause be
$$ C=(a\vee b\vee c\vee d), $$
and let the shortened clause be
$$ C'=(b\vee c\vee d). $$
Suppose a formula $F$ contains $C$, and suppose every clause containing $\bar{a}$ but neither $b$ nor $\bar{c}$ also contains $d$. We prove that replacing $C$ by $C'$ preserves satisfiability.
The replacement can only make the formula harder to satisfy, because $C'$ implies $C$. Therefore every satisfying assignment of the shortened formula is also required to satisfy all clauses other than $C$, and it remains only to prove that it must satisfy $C$ as well.
Assume that an assignment satisfies the formula in which $C$ has been replaced by $C'$. Suppose, for contradiction, that this assignment does not satisfy $C$. Then
$$ a=b=c=d=0. $$
The assignment satisfies every other clause of the formula. Consider any clause $D$ containing $\bar{a}$. If $D$ contains $b$ or $\bar{c}$, then under the assumed values the clause is already controlled by a literal that does not force a conflict with $a=0$. The possible failure of the replacement would have to arise from a clause containing $\bar{a}$ but neither $b$ nor $\bar{c}$.
By hypothesis, every such clause $D$ also contains $d$. Hence every clause containing $\bar{a}$ and lacking both $b$ and $\bar{c}$ has the form
$$ D=\bar{a}\vee d\vee E $$
for some collection of literals $E$. Such a clause cannot force $a=0$ while avoiding the literal $d$ that already appears in $C'$. The shortened clause therefore removes only the case in which $a$ is the sole literal making $C$ true, and the hypothesis guarantees that this case cannot be needed to satisfy the remaining clauses.
A more direct proof uses blocked self-subsumption. Resolve $C$ with an arbitrary clause $D$ containing $\bar{a}$. The resolvent is
$$ R=(b\vee c\vee d\vee(D-{\bar{a}})). $$
If $D$ contains $b$ or $\bar{c}$, then the clause $R$ contains $b$, $c$, and $d$ from $C$, so
$$ (b\vee c\vee d)\subseteq R. $$
If $D$ contains neither $b$ nor $\bar{c}$, the hypothesis says that $D$ contains $d$. The same three literals $b$, $c$, and $d$ occur in the resolvent, and therefore again
$$ (b\vee c\vee d)\subseteq R. $$
Thus every resolvent of $C$ with a clause containing $\bar{a}$ is subsumed by $C'$. Resolving on $a$ can therefore never produce a clause stronger than $C'$. The clause $C$ may be replaced by the self-subsumed clause $C'$ without changing whether the formula is satisfiable.
This proves the required shortening.
No erp rule is needed. The argument uses ordinary blocked self-subsumption: the variable $a$ is eliminated because all possible resolution consequences with clauses containing $\bar{a}$ are already covered by the shortened clause $(b\vee c\vee d)$. The preprocessing rule follows from the existing resolution and subsumption principles.
This completes the proof.
∎