TAOCP 7.2.2.2 Exercise 161
Let $F$ be a set of clauses satisfying the condition that every clause containing a white literal also contains either a black literal or a blue literal.
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: yes
Solve time: 1m17s
Solution
Let $F$ be a set of clauses satisfying the condition that every clause containing a white literal also contains either a black literal or a blue literal. Let $A={a_1,\ldots,a_p}$ be the set of black literals and $B={l_1,\ldots,l_q}$ the set of blue literals. Let
$$ F' = F \cup {(l_1 \vee \cdots \vee l_q \vee a_j) : 1 \le j \le p}. $$
(a)
If $F'$ is satisfiable, then $F$ is satisfiable since $F \subseteq F'$.
Assume $F$ is satisfiable and let $\tau$ be a satisfying assignment for $F$. Construct an assignment $\tau'$ by modifying $\tau$ as follows. For every black literal $a$, assign its underlying variable so that $a$ is true under $\tau'$. For each variable, this fixes all literals in $A$ to true and all corresponding white literals to false by the defining correspondence between colors.
Consider any clause $C \in F$. If $C$ contains a white literal, then $C$ also contains either a black or a blue literal. Under $\tau'$, every black literal is true, so such a clause is satisfied regardless of the values of other literals. If $C$ contains no white literals, then it contains only black, blue, orange, and gray literals. The modification from $\tau$ to $\tau'$ affects only variables whose literals are black or white, so no blue, orange, or gray literal changes value. Since $C$ contains no white literals, no literal in $C$ changes from true to false when passing from $\tau$ to $\tau'$, hence $C$ remains satisfied.
Thus $\tau'$ satisfies $F$ and also satisfies every added clause $(l_1 \vee \cdots \vee l_q \vee a_j)$ because $a_j$ is true under $\tau'$. Therefore $F'$ is satisfiable.
This completes the equivalence $F$ satisfiable if and only if $F'$ satisfiable. ∎
(b)
Let $p=1$, so $A={a}$. Then
$$ F' = F \cup {(l_1 \vee \cdots \vee l_q \vee a)}. $$
The result states that $F$ is satisfiable if and only if adding a single clause requiring that either $a$ is true or at least one blue literal is true preserves satisfiability. In this case the construction shows that any satisfying assignment of $F$ can be modified to force $a$ true without destroying satisfiability of $F$, hence the added clause is always satisfiable.
(c)
Let $q=1$, so $B={l}$. Then
$$ F' = F \cup {(l \vee a_j) : 1 \le j \le p}. $$
The result becomes: $F$ is satisfiable if and only if one can add, for each black literal $a_j$, a binary clause requiring $l$ or $a_j$. Satisfiability is preserved because a satisfying assignment of $F$ can be adjusted so that all black literals are true, in which case every clause $(l \vee a_j)$ is satisfied regardless of the value of $l$.
(d)
Let $p=q=1$, so $A={a}$ and $B={l}$. Then
$$ F' = F \cup {(l \vee a)}. $$
In this case the statement reduces to: $F$ is satisfiable if and only if adjoining a single binary clause linking a black literal $a$ and a blue literal $l$ preserves satisfiability. The preceding construction ensures that any satisfying assignment of $F$ can be modified so that $a$ is true, which immediately satisfies $(l \vee a)$.
This completes the proof. ∎