TAOCP 7.2.2.2 Exercise 286
The statement is true.
Section 7.2.2.2: Satisfiability
Exercise 286. [M24] What choice of signatures-to-keep in Fig. 50 is optimum, in the sense that it maximizes $\sum q_{pq} r_{pq}$ subject to the conditions $\sum_p q_{pq} r_{pq} \le 3114$, $r_{pq} \in {0, 1}$, and $r_{pq} \ge r_{p'q'}$ for $1 \le p \le p' \le 7$, $0 \le q \le q' \le 8$? Here $q_{pq}$ and $b_{pq}$ are the sums of the gray and black clauses that have signature $(p, q)$, as given by the matrices in the text. [This is a special case of the "knapsack problem with a partial ordering."]
Verified: no
Solve time: 3m48s
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.
∎