TAOCP 7.2.2.2 Exercise 14

Exercise 14. [22] [22] Explain why the clauses (17) might help a SAT solver to color a graph.

Verified: yes
Solve time: 56s

Solution

The clauses (17) are useful because they encode the constraints of a graph-coloring problem in a form that allows a SAT solver to detect forced choices early.

Suppose the graph has vertices $v_1,\ldots,v_n$ and colors $1,\ldots,k$. The usual SAT formulation introduces a Boolean variable for each possible assignment of a color to a vertex. The variable $x_{i,j}$ represents the assertion that vertex $v_i$ has color $j$. The clauses in (17) express two kinds of requirements.

First, every vertex must receive at least one color. This is represented by a clause of the form

$$ x_{i,1}\vee x_{i,2}\vee\cdots\vee x_{i,k}. $$

A satisfying assignment must make at least one literal in this clause true, so every vertex is assigned some color.

Second, incompatible color assignments must be forbidden. If two adjacent vertices $v_i$ and $v_j$ cannot both have color $c$, the corresponding clause is

$$ \bar{x}{i,c}\vee \bar{x}{j,c}. $$

This binary clause states that at least one of the two vertices does not receive color $c$. Binary clauses are especially valuable to SAT solvers because they create implication relations. If a solver temporarily assigns $x_{i,c}=1$, the clause above forces $\bar{x}_{j,c}=1$, eliminating that color from the neighboring vertex immediately.

Thus the coloring constraints generate many short clauses, especially binary clauses, that propagate information through the implication structures used by SAT algorithms. A partial coloring that cannot be extended to a complete coloring produces a contradiction quickly, because a chain of forced assignments eventually violates one of the clauses. Without these clauses, a solver would have to explore many assignments that already violate simple adjacency restrictions.

The clauses (17) therefore help a SAT solver by converting graph-theoretic restrictions into logical consequences that can be discovered by unit propagation and related inference procedures. A graph-coloring instance that appears to require a large search can become much smaller after these forced consequences are repeatedly applied.