TAOCP 7.2.2.2 Exercise 161

Section 7.2.2.2: Satisfiability

Exercise 161. ▶ [21] [21] (Black and blue principle.) Now consider coloring literals either white, black, orange, blue, or gray, in such a way that $l$ is white if and only if $\bar{l}$ is black, and $l$ is orange if and only if $\bar{l}$ is blue. (Hence $l$ is gray if and only if $\bar{l}$ is gray.) Suppose further that $F$ is a set of clauses in which every clause containing a white literal also contains either a black literal or a blue literal (or both). Let $A = {a_1, \ldots, a_p}$ be the black literals and $B = {l_1, \ldots, l_q}$ be the blue literals. Also let $F'$ be the set of clauses obtained by adding $p$ additional clauses $(l_1 \vee \cdots \vee l_q \vee a_j)$ to $F$, for $1 \le j \le p$.

a) Prove that $F$ is satisfiable if and only if $F'$ is satisfiable.

b) Restate and simplify that result in the case that $p = 1$.

c) Restate and simplify that result in the case that $q = 1$.

d) Restate and simplify that result in the case that $p = q = 1$. (In this special case, $(l \vee a)$ is called a binary clause.)

Verified: no
Solve time: 2m48s

---

Corrected solution:

Edit

Solution

Let (F') be obtained from (F) by adjoining the clauses

[ (l_1\vee\cdots\vee l_q\vee a_j),\qquad 1\le j\le p . ]

The reverse implication is immediate because every clause of (F) is also a clause of (F'). Thus, if (F') is satisfiable, then (F) is satisfiable.

It remains to prove that if (F) is satisfiable, then (F') is satisfiable.

Assume that (F) has a satisfying assignment. Modify this assignment by making every black literal and every blue literal true. This is consistent because a literal and its complement cannot both be black or both be blue: if a literal is black, its complement is white, and if a literal is blue, its complement is orange.

We show that the modified assignment still satisfies every clause of (F). Consider a clause (C) of (F).

If (C) contains a black or blue literal, then (C) is satisfied by the modified assignment, because all such literals have been made true.

Now suppose that (C) contains neither a black nor a blue literal. Any literal whose value changed from true to false during the modification must have been the complement of either a black literal or a blue literal. Such a literal is respectively white or orange. Since (C) contains no black or blue literals, no literal in (C) could have changed from true to false. Therefore every literal that was true in the original satisfying assignment remains true, and (C) is still satisfied.

Equivalently, one may focus on the only possible danger: a clause losing all of its originally true literals. Such a loss can occur only if the clause contains a white or orange literal that was changed to false. If the changed literal is white, the hypothesis on (F) guarantees that the clause also contains a black or blue literal, which is now true. If the changed literal is orange, its complement is blue, so the orange literal itself cannot have been changed by making blue literals true. Hence no clause becomes false.

Thus the modified assignment satisfies (F) and has every black and every blue literal true. In particular, every added clause

[ (l_1\vee\cdots\vee l_q\vee a_j) ]

is satisfied, because it contains the true literals (l_1,\ldots,l_q) and (a_j). Therefore the modified assignment satisfies (F'), proving that (F') is satisfiable.

Hence,

[ F\text{ is satisfiable}\iff F'\text{ is satisfiable}. ]

This proves part (a).

For part (b), suppose that (p=1), so the set of black literals is (A={a}). Only one additional clause is added:

[ (l_1\vee\cdots\vee l_q\vee a). ]

Therefore the black and blue principle says that, under the stated coloring condition, adding the single clause

[ a\vee l_1\vee\cdots\vee l_q ]

does not change whether the formula is satisfiable. Equivalently, every satisfying instance of (F) has a satisfying assignment in which this additional condition holds.

For part (c), suppose that (q=1), so the set of blue literals is (B={l}). The added clauses are

[ (l\vee a_j),\qquad 1\le j\le p . ]

Their conjunction can be simplified by distributivity:

[ (l\vee a_1)\wedge\cdots\wedge(l\vee a_p) \equiv l\vee(a_1\wedge\cdots\wedge a_p). ]

Thus the result states that, under the coloring condition, adjoining the requirement

[ l\vee(a_1\wedge\cdots\wedge a_p) ]

preserves satisfiability.

For part (d), suppose that (p=q=1). Then there is one black literal (a) and one blue literal (l), and the only added clause is

[ (l\vee a). ]

The principle becomes the following special case: if every clause containing the white literal (\bar a) also contains either (a) or (l), then adding the binary clause

[ (l\vee a) ]

does not change the satisfiability of the formula.

This is the binary-clause form of the black and blue principle.