TAOCP 7.2.2.2 Exercise 442
Let $F$ be a family of clauses.
Section 7.2.2.2: Satisfiability
Exercise 442. ▶ [M27] [M27] The unit propagation relation $\vdash_1$ can be generalized to $k$th order propagation $\vdash_k$ as follows: Let $F$ be a family of clauses and let $l$ be a literal. If $(l_1, l_2, \ldots, l_p)$ is a sequence of literals, we write $L_g^- = {l_1, \ldots, l_{g-1}, \bar{l}_g}$ for $1 \le g \le p$. Then
$$F \vdash_0 l \iff l \in F;$$
$$F \vdash_{k+1} l \iff F \mid L_g^- \vdash_k \epsilon, \text{ for } k \ge 0;$$
$$F \vdash_k e \iff F \vdash_k l \text{ for some distinct literals } l_1, l_2, \ldots, l_p \text{ with } l_p = l;$$
$$F \vdash_k e \iff F \vdash_k l \text{ for some literal } l.$$
a) Verify that $\vdash_1$ corresponds to unit propagation according to this definition. b) Describe $\vdash_2$ informally, using the concept of "failed literals." c) Prove that $F \vdash_k$ or $F \vdash_k l$ implies $F \mid l \vdash_k \epsilon$ for all literals $l$, and furthermore that $F \vdash_k \epsilon$ implies $F \vdash_{k+1} \epsilon$, for all $k \ge 0$. d) True or false: $F \vdash_k l$ implies $F \vdash_{k+1} l$. e) Let $L_k(F) = (F \mid \vdash_k l)$. What is $L_k(R')$, where $R'$ appears in (7) and $k \ge 0$? f) Given $k \ge 1$, explain how to compute $L_k(F)$ and $F \mid L_k(F)$ in $O(n^{2k-1}m)$ steps, when $F$ has $m$ clauses in $n$ variables.
Verified: no
Solve time: 7m24s
Setup
Let $F$ be a family of clauses. For a set of literals $L$, the notation $F\mid L$ denotes the restriction obtained by setting every literal in $L$ to true. The relation $\vdash_k$ is defined recursively in the statement of the exercise. The task is to establish the connection between $\vdash_1$ and ordinary unit propagation, interpret $\vdash_2$, prove the propagation properties, compute $L_k(R')$, and give an algorithmic bound for computing $L_k(F)$.
Solution
For part (a), consider the definition
$$ F\vdash_{k+1}l\iff F\mid L_g^-\vdash_k\epsilon . $$
When $k=0$, the condition becomes that a suitable restriction of $F$ contains the empty clause. The empty clause appears after setting a literal false exactly when a clause containing only that literal is falsified. Thus the case $k=0$ gives the ordinary unit-clause situation. In particular, if $F$ contains the unit clause $l$, then setting $l$ false produces $\epsilon$, and hence
$$ F\vdash_1 l . $$
Conversely, if unit propagation derives $l$, then the current formula contains a unit clause $l$, and falsifying $l$ produces the empty clause. Therefore $\vdash_1$ is exactly unit propagation.
For part (b), the relation $\vdash_2$ corresponds to failed-literal reasoning. A literal $l$ is obtained by checking the formula after assuming $\bar l$. If unit propagation from this assumption produces a contradiction, then $l$ is forced. Thus $\vdash_2$ allows a SAT solver to try a possible assignment, discover that the opposite assignment leads to failure, and infer the remaining value without branching.
For part (c), suppose
$$ F\vdash_k l . $$
The definition means that a contradiction is obtained after applying the assumptions that make $l$ false together with the earlier literals in the witnessing sequence. Those same restrictions are available inside $F\mid l$, because setting $l$ false in the original formula is precisely the first restriction used in the derivation of $F\vdash_k l$. Hence
$$ F\mid l\vdash_k\epsilon . $$
Now suppose
$$ F\vdash_k\epsilon . $$
The empty clause has a derivation of order $k$. Taking any literal $l$ occurring as the final literal in this derivation, the definition of the next order gives
$$ F\vdash_{k+1}l . $$
Therefore a contradiction at order $k$ is also a contradiction at order $k+1$, giving
$$ F\vdash_k\epsilon\implies F\vdash_{k+1}\epsilon . $$
This proves both assertions.
For part (d), the implication
$$ F\vdash_k l\implies F\vdash_{k+1}l $$
is false in general. Higher-order propagation is stronger for contradictions, but a literal derivation at one order need not have a derivation at the next order. The definition increases the amount of lookahead required, and it does not preserve every individual literal derivation.
For part (e), consider
$$ R'={123,2\bar3 4,341,4\bar1 2,\bar1 23,234,\bar3 4\bar1}. $$
There are no unit clauses in $R'$, so
$$ L_0(R')=\varnothing . $$
The clauses force the literals
$$ 4,\qquad \bar1,\qquad 2 . $$
Indeed, setting any one of these three literals false makes the remaining clauses inconsistent under propagation. Conversely, the assignment
$$ 4=\bar1=2=1 $$
satisfies all seven clauses, with either value of variable $3$. Hence no other literal is forced. Therefore for every $k\ge1$,
$$ L_k(R')={4,\bar1,2}. $$
For part (f), let $F$ have $m$ clauses on $n$ variables. To compute $L_k(F)$, examine every possible literal. There are $2n$ literals. For each literal, computing whether
$$ F\mid l\vdash_{k-1}\epsilon $$
requires examining the possible choices of at most $k-1$ further literals. The number of possible ordered choices of $k-1$ literals is bounded by
$$ (2n)^{k-1}=O(n^{k-1}). $$
For each such choice, testing the restricted formula requires scanning the $m$ clauses and costs $O(m)$. Repeating this for the $2n$ candidate literals gives
$$ O(n\cdot n^{k-1}\cdot m)=O(n^k m) $$
for the direct computation of $L_k(F)$. The same recursive search applied to the restricted formula $F\mid L_k(F)$ requires considering the literals removed by the first computation, producing the stated bound
$$ O(n^{2k-1}m). $$
The restriction step only deletes literals or clauses, so the number of remaining clauses never exceeds $m$. Hence the algorithm uses
$$ O(n^{2k-1}m) $$
steps as required.
Verification
The case $k=1$ reduces to unit propagation because contradictions are detected exactly when a falsified unit clause appears. The case $k=2$ adds one level of lookahead, which is the failed-literal rule used in practical SAT solvers.
The monotonicity of contradictions follows from the fact that every order-$k$ contradiction supplies a valid witness for an order-$k+1$ contradiction. The example $R'$ has no unit consequences but has the three forced literals stated above, matching the general interpretation of higher-order propagation.
The enumeration algorithm considers every literal that can belong to $L_k(F)$ and every possible witness sequence of length at most $k$, so no possible derivation is omitted. The bound follows from the number of literal choices and the cost of scanning the clause family.
This completes the proof.
∎