TAOCP 7.2.2.2 Exercise 120
Let $F$ be a family of clauses and $L$ a set of literals.
Section 7.2.2.2: Satisfiability
Exercise 120. [M20] [M20] True or false: $F|L = (C \setminus \bar{L} \mid C \in F \text{ and } C \cap L = \emptyset)$, if $\bar{L} = {\bar{l} \mid l \in L}$.
Verified: yes
Solve time: 1m33s
Solution
Let $F$ be a family of clauses and $L$ a set of literals. The reduction $F|l$ for a single literal $l$ is defined in Section 7.2.2.2 as follows: every clause $C$ containing $l$ is deleted, and from every remaining clause $C$ the literal $\bar{l}$ is removed.
For a set $L$, the reduction $F|L$ is obtained by applying this operation successively for each $l \in L$. Since literals in $L$ are assumed strictly distinct, no variable occurs in both positive and negative form inside $L$, so the successive reductions are consistent.
Consider the right-hand expression
$$ F^\star := (C \setminus \bar{L} \mid C \in F \text{ and } C \cap L = \emptyset), $$
where $\bar{L} = {\bar{l} \mid l \in L}$.
The condition $C \cap L = \emptyset$ selects exactly those clauses that contain no literal in $L$. For such a clause $C$, forming $C \setminus \bar{L}$ removes all literals $\bar{l}$ with $l \in L$, while leaving all other literals unchanged.
We compare this construction with $F|L$.
A clause $C$ is removed in $F|L$ if and only if some literal $l \in L$ belongs to $C$, since in the first step at which such an $l$ is processed, $C$ is satisfied and deleted. This matches the condition $C \cap L = \emptyset$ for survival in $F^\star$.
Now assume $C \cap L = \emptyset$. In $F|L$, each step corresponding to $l \in L$ removes $\bar{l}$ from every remaining clause. Since no literal of $L$ lies in $C$, the only possible deletions are precisely the literals $\bar{l}$ for $l \in L$. After all reductions, the remaining clause is exactly $C \setminus \bar{L}$.
Thus every clause that survives $F|L$ appears in $F^\star$ with exactly the same set of literals, and every clause in $F^\star$ survives all reductions defining $F|L$ and undergoes the same deletions.
The two constructions therefore produce identical families of clauses.
This completes the proof. ∎