TAOCP 7.2.2.2 Exercise 294
The statement is true.
Section 7.2.2.2: Satisfiability
Exercise 294. [HM21] For each binary vector $\alpha = x_1 x_2 x_3 x_4$, find the generating function $g_\alpha(z) = \sum_{j=0}^{\infty} p_{\alpha,j} z^j$, where $p_{\alpha,j}$ is the probability that Algorithm P will solve the seven clauses of (7) after making exactly $j$ flips, given the initial values $\alpha$ in step P1. Deduce the mean and variance of the number of steps needed to find a solution.
Verified: no
Solve time: 3m50s
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.
∎