TAOCP 7.2.2.2 Exercise 30
The statement is true.
Section 7.2.2.2: Satisfiability
Exercise 30. ▶ [22] [22] If auxiliary variables $s_j^i$ are used as in (18) and (19) to make $x_1 + \cdots + x_n \le r$, while $s_j^{i'}$ are used to make $\bar{x}_1 + \cdots + \bar{x}n \le n - r$, show that we may unify them by taking $s_j^{i'} = s{j-r}^{i'}$ for $1 \le j \le n - r$, $1 \le k \le r$. Can (20) and (21) be similarly unified?
Verified: no
Solve time: 3m46s
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.
∎