TAOCP 7.2.2.2 Exercise 160

Section 7.2.2.2: Satisfiability

Exercise 160. [18] [18] (Black and white principle.) Consider any rule by which literals have been colored white, black, or gray in such a way that $l$ is white if and only if $\bar{l}$ is black. (For example, we might say that $l$ is white if it appears in fewer clauses than $\bar{l}$.)

a) Suppose every clause of $F$ that contains a white literal also contains a black literal. Prove that $F$ is satisfiable if and only if its all-gray clauses are satisfiable.

b) Explain why this metaphor is another way to describe the notion of an autarky.

Verified: yes
Solve time: 1m33s

Solution

Let $F_{\mathrm{g}}$ denote the set of all-gray clauses of $F$. The coloring rule gives

$$ l\text{ is white}\iff \bar l\text{ is black}. $$

Hence a non-gray variable has exactly one white literal and one black literal, while a gray variable has two gray literals.

Suppose first that $F$ is satisfiable. Any satisfying assignment for $F$ also satisfies every clause in the subset $F_{\mathrm{g}}$, so $F_{\mathrm{g}}$ is satisfiable.

For the converse, suppose that $F_{\mathrm{g}}$ is satisfiable. Choose an assignment satisfying all all-gray clauses. Extend this assignment to the remaining variables by making every black literal true. This is a consistent assignment, because for each non-gray variable exactly one of its two literals is black.

Consider a clause $C$ of $F$ that is not all-gray. If $C$ contains a black literal, then $C$ is satisfied by the extension. If $C$ contains a white literal, the hypothesis of the problem states that $C$ also contains a black literal, so $C$ is again satisfied. Every non-gray clause is therefore satisfied. The gray clauses are satisfied by the original assignment, so the extended assignment satisfies all of $F$.

Therefore,

$$ F\text{ is satisfiable}\iff F_{\mathrm{g}}\text{ is satisfiable}. $$

This proves part (a).

For part (b), the coloring describes an autarky in another form. The non-gray variables can be assigned independently of the gray variables by making all black literals true. Every clause involving any of these variables is satisfied by this partial assignment: a clause containing a black literal is satisfied directly, and a clause containing a white literal must also contain a black literal by the hypothesis. Thus the assignment on the non-gray variables satisfies every clause that it touches, which is precisely the defining property of an autarky.

After applying this autarky, only the all-gray clauses remain relevant. The black and white colors therefore represent the part of the formula that can be satisfied and discarded independently, while the gray clauses contain the remaining unsolved core. This is the same reduction expressed by the notion of an autarky.

This completes the proof. ∎