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

Solution

The clauses (17) encode a graph coloring instance as a conjunctive normal form formula in which each vertex is assigned one of a fixed set of colors, and adjacent vertices are forbidden from receiving the same color. A standard encoding introduces, for each vertex $v$ and each color $c$, a variable $v_c$ meaning that $v$ has color $c$. The clauses then enforce that each vertex receives at least one color and that no vertex receives two different colors, together with adjacency constraints preventing conflicts.

In this form, satisfiability corresponds exactly to the existence of a proper coloring of the graph, since a satisfying assignment selects for each vertex exactly one true color variable, and the adjacency clauses ensure that endpoints of every edge do not share a color.

The usefulness of clauses (17) for a SAT solver comes from their strong local propagation structure. Each vertex clause has the form of a short disjunction such as $(v_1 \vee v_2 \vee v_3)$ in the case of three colors. When all but one of these literals become false during the search, unit propagation forces the remaining literal to be true, thereby fixing the color of the vertex without further branching.

The edge clauses have the form $(\bar{u}_c \vee \bar{v}_c)$ for each edge $(u,v)$ and color $c$. When a vertex is assigned color $c$, these clauses immediately force the exclusion of color $c$ from all neighbors of that vertex. This produces a cascade of unit propagations that rapidly restricts the search space.

The combination of “at least one color per vertex” clauses and “no monochromatic edge” clauses creates frequent short implications and early contradictions. If a partial assignment attempts to assign incompatible colors to adjacent vertices, some edge clause becomes unsatisfied under a partial assignment and forces a conflict after few steps, allowing backtracking to occur early.

Thus the structure of clauses (17) translates global graph coloring constraints into many small, tightly coupled local constraints, which SAT solvers handle efficiently through unit propagation and conflict detection. This makes coloring instances particularly amenable to modern SAT-solving techniques. ∎