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: 1m12s

Solution

Let literals be colored white, black, or gray, with the constraint that a literal $l$ is white if and only if $\bar{l}$ is black. Hence each variable contributes either a white–black pair $(v,\bar v)$, a black–white pair, or a gray–gray pair.

Assume every clause containing a white literal also contains a black literal.

(a)

Construct a partial assignment $\alpha$ by setting every black literal to $1$, every white literal to $0$, and leaving gray variables unassigned.

Consider any clause $C$ of $F$.

If $C$ contains a white literal $l$, then $C$ also contains a black literal $l'$. Under $\alpha$, $l'$ has value $1$, hence $C$ is satisfied.

If $C$ contains no white literal, then all its literals are either black or gray. Every black literal in $C$ has value $1$ under $\alpha$, so such clauses are already satisfied whenever they contain a black literal.

The only clauses not automatically satisfied by this argument are those containing no black literals. Such clauses cannot contain white literals either, since white literals always force the presence of a black literal in the same clause. Hence these clauses consist entirely of gray literals and form exactly the all-gray subfamily.

Let $F_{\mathrm{gray}}$ denote the set of all-gray clauses. Any satisfying assignment of $F$ must satisfy $F_{\mathrm{gray}}$, since these clauses depend only on gray variables. Conversely, if $F_{\mathrm{gray}}$ is satisfiable, extend a satisfying assignment by fixing all black literals to $1$ and all white literals to $0$. Every clause containing a black literal is satisfied, and all remaining clauses lie in $F_{\mathrm{gray}}$.

Thus $F$ is satisfiable if and only if $F_{\mathrm{gray}}$ is satisfiable.

This completes the proof. ∎

(b)

Let $B$ be the set of all black literals and $W$ the set of all white literals. The coloring condition ensures that no clause contains a white literal without also containing a black literal, so every clause that is affected by assigning $B$ is satisfied once a value is chosen for $B$.

The assignment that sets all literals in $B$ to $1$ and all literals in $W$ to $0$ satisfies every clause containing a black literal or a white literal. The remaining constraints are exactly the clauses disjoint from $B \cup W$, namely the all-gray clauses.

Hence $B$ functions as a partial assignment that satisfies every clause it touches, while leaving the residual formula on gray variables unchanged. This is precisely an autarky: a partial assignment that satisfies every clause containing any assigned literal, while reducing the instance to the subformula induced by unassigned variables.

Thus the black–white coloring describes an autarky decomposition of $F$ into a satisfied part and a residual gray SAT instance. ∎