TAOCP 7.2.2.2 Exercise 276
The statement is true.
Section 7.2.2.2: Satisfiability
Exercise 276. [M15] True or false: If $F$ is a family of clauses and $L$ is a set of strictly distinct literals, then $F \wedge L \vdash_1 \epsilon$ if and only if $(F|L) \vdash_1 \epsilon$.
Verified: yes
Solve time: 1m56s
Solution
The statement is true.
Let $L$ be a set of strictly distinct literals. The expression $F\wedge L$ means that the unit clauses consisting of the literals of $L$ are added to $F$. The expression $F|L$ denotes the formula obtained by applying the partial assignment specified by $L$: every clause containing a literal of $L$ is deleted, and every occurrence of a literal in $\bar{L}$ is removed from the remaining clauses.
The direction
$$ F\wedge L\vdash_1\epsilon \implies (F|L)\vdash_1\epsilon $$
follows by considering a unit propagation derivation from $F\wedge L$. The initial unit clauses are exactly the literals of $L$. After these literals have been assigned, every later propagation step uses a clause of $F$ whose literals from $L$ have been satisfied and whose literals from $\bar L$ have been falsified. The remaining unsatisfied literals are precisely the literals that appear in the corresponding clause of $F|L$. Therefore each propagation step after the initial assignment corresponds to the same unit propagation step in $F|L$.
If the derivation from $F\wedge L$ ends with the empty clause $\epsilon$, then the corresponding derivation in $F|L$ also reaches $\epsilon$. Hence
$$ (F|L)\vdash_1\epsilon . $$
For the reverse direction, suppose that
$$ (F|L)\vdash_1\epsilon . $$
We construct a unit propagation derivation from $F\wedge L$. First propagate the literals of $L$, using the unit clauses that were added to $F$. Consider any unit propagation step in the derivation of $F|L$. Let the propagated clause in $F|L$ be $C|L$. The clause $C|L$ came from a clause $C\in F$ after deleting literals falsified by $L$ and deleting clauses already satisfied by $L$.
The literals deleted from $C$ are exactly the complements of literals already propagated from $L$. Thus, after the literals of $L$ have been assigned in $F\wedge L$, the clause $C$ has the same remaining unassigned literals as $C|L$. A clause that is unit in $F|L$ is therefore unit in $F\wedge L$ after the literals of $L$ have been propagated. The same propagated literal can be derived in $F\wedge L$.
Repeating this correspondence for every propagation step of the derivation of $(F|L)\vdash_1\epsilon$ gives a unit propagation derivation in $F\wedge L$ that reaches the empty clause. Hence
$$ F\wedge L\vdash_1\epsilon . $$
The strict distinctness condition on $L$ guarantees that the literals of $L$ describe a consistent partial assignment. Without this condition, a pair $l,\bar l\in L$ would already make $F\wedge L$ contradictory, while the restriction operation would not have the same interpretation.
Therefore the two unit-refutation conditions are equivalent:
$$ \boxed{F\wedge L\vdash_1\epsilon\iff(F|L)\vdash_1\epsilon}. $$
This completes the proof.
∎