🧩 Constraint Solving POTD:Graph Coloring — Classic CSP with SAT, MIP, and CP Models

[github-actions[bot]]

Date: 2026-04-20 | Category: Classic CSP

---

Problem Statement

Graph Coloring asks: given a graph G = (V, E) and k colors, assign one color to each vertex so that no two adjacent vertices share the same color. The chromatic number χ(G) is the minimum k for which this is possible.

Concrete Instance — Petersen Graph (10 vertices, 15 edges)

Vertices: {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
Edges (outer pentagon + inner pentagram + spokes):
  Outer: 0-1, 1-2, 2-3, 3-4, 4-0
  Inner: 5-7, 7-9, 9-6, 6-8, 8-5
  Spokes: 0-5, 1-6, 2-7, 3-8, 4-9

Question: Can we color this graph with 3 colors?
Answer: Yes — χ(Petersen) = 3. A valid coloring: {0→R, 1→G, 2→B, 3→G, 4→B, 5→G, 6→R, 7→R, 8→B, 9→B} (verify: every edge has distinct endpoints).

Input: Graph G, integer k
Output: A mapping color: V → {1..k} satisfying all edge constraints, or UNSAT

---

Why It Matters

• Register Allocation: Compilers model variables as graph vertices and register conflicts as edges; coloring directly yields a register assignment. A spill occurs when χ > #registers``.
• Timetabling & Scheduling: Exams sharing students are adjacent; colors are time-slots. Frequency assignment in wireless networks works identically.
• VLSI Design: Layers in circuit routing and via minimization reduce to graph coloring variants.

---

Modeling Approaches

Approach 1 — Constraint Programming (CP)

Decision variables: color_v ∈ {1..k} for each v ∈ V

Constraints:

∀ (u,v) ∈ E :  color_u ≠ color_v

Global constraint: allDifferent can be applied to cliques in the graph for stronger propagation.

Symmetry breaking: Fix color_{v_0} = 1, and for each new vertex v_i (in BFS order) require color_{v_i} ≤ 1 + max(color_{v_j} : j < i). This eliminates permutations of the color palette.

Trade-offs: CP propagation via arc consistency (AC-3 / AC-4) prunes domains aggressively. The notEqual constraint is lightweight, but clique-based allDifferent provides stronger bounds on k.

---

Approach 2 — SAT Encoding

Variables: Boolean x_{v,c} = "vertex v gets color c"

At-least-one per vertex:

∀ v :  x_{v,1} ∨ x_{v,2} ∨ ... ∨ x_{v,k}

At-most-one per vertex (pairwise):

∀ v, c1 < c2 :  ¬x_{v,c1} ∨ ¬x_{v,c2}

Edge constraints:

∀ (u,v) ∈ E, ∀ c :  ¬x_{u,c} ∨ ¬x_{v,c}

Total clauses: |V| (ALO) + |V|·k(k-1)/2 (AMO) + |E|·k (edges)

Trade-offs: Modern CDCL solvers (MiniSat, CaDiCaL) handle this well for moderate k. The AMO encoding blows up for large k; commander-variable or product encodings can compress it. SAT is ideal when you need a yes/no answer quickly.

---

Approach 3 — Mixed-Integer Programming (MIP)

Variables: x_{v,c} ∈ {0,1}, w_c ∈ {0,1} (is color c used?)

Minimize: ∑_c w_c (minimize number of colors used)

Constraints:

∑_c x_{v,c} = 1          ∀ v        (exactly one color)
x_{u,c} + x_{v,c} ≤ w_c  ∀ (u,v)∈E, ∀ c
x_{v,c} ≤ w_c             ∀ v, c

Trade-offs: MIP naturally optimizes χ(G) rather than just deciding feasibility. LP relaxation provides lower bounds; clique inequalities tighten the LP gap substantially.

---

Example Model — MiniZinc (CP)

int: n;          % number of vertices
int: k;          % number of colors
int: m;          % number of edges
array[1..m, 1..2] of int: edges;

array[1..n] of var 1..k: color;

% No two adjacent vertices share a color
constraint forall(e in 1..m)(
  color[edges[e,1]] != color[edges[e,2]]
);

% Symmetry breaking: colors used in non-decreasing order
constraint color[1] = 1;
constraint forall(v in 2..n)(
  color[v] <= 1 + max(color[u] | u in 1..v-1)
);

solve satisfy;

For the Petersen graph: set n=10, k=3, m=15 and provide the edge list. The solver returns a valid 3-coloring in milliseconds.

---

Key Techniques

1. Propagation — Bounds on Cliques

The clique lower bound states χ(G) ≥ ω(G) (clique number). Finding a large clique (even a maximal one via greedy) tightens the domain of k before search begins. In CP, posting allDifferent over a clique prunes all k < |clique|.

2. DSATUR Heuristic

DSATUR (Brélaz 1979) is a powerful variable-ordering heuristic:

• At each step, color the uncolored vertex with the highest saturation (most distinct colors in its neighborhood).
• Tie-break on degree.
• Often finds optimal or near-optimal colorings without backtracking.
• Used both standalone and as a branching strategy inside CP/SAT solvers.

3. Symmetry Breaking via Value Ordering

Permuting the color labels gives k! equivalent solutions. The lex-leader constraint eliminates these: ensure the color assignment is lexicographically minimal among all equivalent solutions. In practice, the incremental symmetry-breaking above (color v_i ≤ 1 + max previous colors) achieves this efficiently.

---

Challenge Corner

🧩 Think about this:

The fractional chromatic number χ_f(G) is defined via a linear programming relaxation and always satisfies χ_f(G) ≤ χ(G).

1. Can you write the LP relaxation for the SAT-based coloring formulation and identify what χ_f represents geometrically?
2. For the Petersen graph, χ_f = 5/2. How large is the integrality gap relative to χ = 3?
3. Can you encode a list coloring variant — where each vertex v has its own allowed color set L(v) ⊆ {1..k} — as a minor modification of the CP model above?

---

References

1. Brélaz, D. (1979). "New Methods to Color the Vertices of a Graph." Communications of the ACM, 22(4):251–256. — The classic DSATUR paper.
2. Rossi, F., van Beek, P., Walsh, T. (eds.) (2006). Handbook of Constraint Programming, Elsevier. — Chapter 2 covers CSP foundations; Chapter 7 covers graph problems.
3. Mehrotra, A. & Trick, M. A. (1996). "A Column Generation Approach for Graph Coloring." INFORMS Journal on Computing, 8(4):344–354. — Branch-and-price approach achieving state-of-the-art MIP results.
4. Sinz, C. (2005). "Towards an Optimal CNF Encoding of Boolean Cardinality Constraints." CP 2005, LNCS 3709. — The AMO encoding options referenced in the SAT model.

Generated by Constraint Solving — Problem of the Day · ● 114.4K · ◷

• expires on Apr 27, 2026, 12:58 PM UTC