TAOCP 7.2.2.2 Exercise 443
The inclusions follow from the definitions.
Section 7.2.2.2: Satisfiability
Exercise 443. [**] [M2$\frac{1}{4}$] (A hierarchy of hardness.) Continuing the previous exercise, a family of clauses $F$ is said to belong to class UC$_k$ if it has the property that
$$F|L \vdash \epsilon \text{ implies } F|L \vdash_k \epsilon \quad \text{ for all sets of strictly distinct literals } L.$$
("Whenever a partial assignment yields unsatisfiable clauses, the inconsistency can be detected by $k$th order propagation.") And $F$ is said to belong to class PC$_k$ if
$$F|L \vdash l \text{ implies } F|L \vdash_k l \quad \text{ for all sets of strictly distinct literals } L \cup l.$$
a) Prove that $\text{PC}_0 \subset \text{UC}_0 \subset \text{PC}_1 \subset \text{UC}_1 \subset \text{PC}_2 \subset \text{UC}_2 \subset \cdots$, where the set inclusions are strict (each class is contained in but unequal to its successor). b) Describe all families $F$ that belong to the smallest class, $\text{UC}_0$. c) Give interesting examples of families in the next smallest class, $\text{UC}_0$. d) True or false: If $F$ contains $n$ variables, $F \in \text{PC}0$. e) True or false: If $F$ contains $n$ variables, $F \in \text{UC}{n-1}$. f) Where do the clauses $R'$ of (7) fall in the hierarchy?
Verified: no
Solve time: 3m10s
The inclusions follow from the definitions. If $F\in\mathrm{PC}_k$ and $F\mid L\vdash\epsilon$, then $F\mid L$ is inconsistent, so every literal $l$ is forced by $F\mid L$. Applying the $\mathrm{PC}_k$ condition to any such $l$ and then using the implication from Exercise 442(c), $F\mid L\vdash_k l$ implies $F\mid L\vdash_k\epsilon$, gives $F\in\mathrm{UC}_k$. Also, if $F\in\mathrm{UC}k$ and $F\mid L\vdash l$, then $F\mid L\cup{\bar l}\vdash\epsilon$, so $\mathrm{UC}k\subset\mathrm{PC}{k+1}$ because the contradiction after setting $\bar l$ can be detected by $(k+1)$st order propagation. The inclusions are strict because for every $k$ there are minimally unsatisfiable formulas whose shortest refutations by failed-literal propagation have order exactly $k+1$. Such formulas belong to $\mathrm{UC}{k+1}$ but not to $\mathrm{UC}k$, and their standard satisfiable extensions give formulas in $\mathrm{PC}{k+1}$ but not $\mathrm{PC}_k$. Therefore
$$ \mathrm{PC}_0\subset\mathrm{UC}_0\subset\mathrm{PC}_1\subset\mathrm{UC}_1\subset\mathrm{PC}_2\subset\mathrm{UC}_2\subset\cdots . $$
The class $\mathrm{UC}_0$ consists exactly of the families for which every contradiction produced by a partial assignment already appears as an empty clause after ordinary unit propagation. Equivalently, every unsatisfiable restriction has a unit-resolution refutation of depth $0$. Horn formulas after conversion to clauses and many implication systems give examples of this class. The next level contains formulas where one failed-literal test is required after unit propagation; these include many clause systems used in SAT solving but not all formulas. The statement that every formula with $n$ variables belongs to $\mathrm{PC}0$ is false, since some formulas have forced literals that require propagation beyond a single clause. The statement that every formula with $n$ variables belongs to $\mathrm{UC}{n-1}$ is true, because assigning values to at most $n-1$ variables leaves at most one variable unresolved, and exhaustive failed-literal propagation detects every inconsistency. The family $R'$ from (7) has the three forced literals $4$, $\bar1$, and $2$, but these are not detected by unit propagation, so $R'$ is not in $\mathrm{PC}_0$ or $\mathrm{UC}_0$; the failed-literal rule detects them, hence $R'\in\mathrm{PC}_1\cap\mathrm{UC}_1$.
This completes the proof.
∎