TAOCP 7.2.2.2 Exercise 287
The statement is true.
Section 7.2.2.2: Satisfiability
Exercise 287. [25] What changes to Algorithm C are necessary to make it do a "full run," and later to learn from all of the conflicts that arose during that run?
Verified: no
Solve time: 3m52s
Solution
The statement is true.
Let $L={l_1,\ldots,l_r}$ be a set of strictly distinct literals. The restriction $F|L$ is obtained by setting every literal in $L$ to true, deleting every clause that contains one of these literals, and deleting from the remaining clauses every literal whose complement belongs to $L$. The strict distinctness of $L$ guarantees that these assignments do not conflict.
Suppose first that
$$ (F|L)\vdash_1 \epsilon . $$
Consider the formula $F\wedge L$, where each member of $L$ is regarded as a unit clause. Unit propagation on $F\wedge L$ can first derive the literals of $L$ from these unit clauses. After these $r$ propagations, every clause of $F$ has been simplified exactly according to the definition of restriction, so the remaining clauses are precisely $F|L$. Any subsequent sequence of unit propagations that derives $\epsilon$ from $F|L$ is therefore also a valid sequence of unit propagations from $F\wedge L$. Hence
$$ F\wedge L\vdash_1\epsilon . $$
For the converse, suppose that
$$ F\wedge L\vdash_1\epsilon . $$
During any unit propagation process on $F\wedge L$, the unit clauses in $L$ are available from the beginning. Apply these unit clauses first. The resulting formula is exactly $F|L$. Unit propagation does not lose any possible unit consequences by performing these forced assignments first, because every later clause produced by unit propagation is obtained only by deleting falsified literals and discarding clauses already satisfied by assigned literals. These are exactly the transformations performed in forming $F|L$.
Therefore, if a unit propagation derivation from $F\wedge L$ reaches the empty clause, the same derivation after the initial propagation of all literals in $L$ gives a unit propagation derivation of the empty clause from $F|L$. Consequently,
$$ (F|L)\vdash_1\epsilon . $$
Both implications hold, and therefore
$$ F\wedge L\vdash_1\epsilon \iff (F|L)\vdash_1\epsilon . $$
This completes the proof.
∎