🧩 Constraint Solving POTD:Graph Coloring

[github-actions[bot]]

🎨 Problem of the Day: Graph Coloring

Category: Classic CSP · Date: 2026-05-14

---

Problem Statement

Given an undirected graph G = (V, E), assign a color to each vertex such that no two adjacent vertices share the same color, using the minimum number of colors possible (the chromatic number χ(G)).

Small Concrete Instance

Consider this 5-node graph (a cycle C5):

Vertices: {1, 2, 3, 4, 5}
Edges:    (1,2), (2,3), (3,4), (4,5), (5,1)

The chromatic number of an odd cycle is 3 — try it! Any 2-coloring forces a conflict.

Input: An adjacency list and a target number of colors k
Output (decision): A valid k-coloring, or UNSAT if none exists
Output (optimization): The minimum k and corresponding coloring

---

Why It Matters

• Register allocation in compilers: variables are nodes, conflicts are edges — coloring = assigning CPU registers with minimal spills.
• Frequency assignment in wireless networks: base stations are nodes, interference constraints are edges — colors are frequency bands.
• Examination timetabling: exams sharing students cannot overlap — finding the minimum number of time slots is exactly graph coloring.
• Printed circuit board testing and map coloring (the famous Four Color Theorem!) are classic applications.

---

Modeling Approaches

Approach 1 — Constraint Programming (CP)

Decision variables: color[v] ∈ {1..k} for each vertex v ∈ V

Constraints:

∀ (u,v) ∈ E: color[u] ≠ color[v]       -- no two adjacent vertices share a color

Symmetry breaking (critical for performance):

color[v0] = 1                            -- fix first vertex's color
∀ v in order: color[v] ≤ 1 + max{color[u] : u < v, u adjacent to v or color[u] used}

Trade-offs: CP propagation via arc consistency prunes the domain of color[v] whenever a neighbor is assigned. The alldifferent-like structure is exploited well by global clique constraints. Scales reasonably to hundreds of nodes with good search heuristics.

---

Approach 2 — SAT Encoding

Introduce Boolean variables x[v][c] = "vertex v gets color c".

At-least-one: ∀v: x[v][1] ∨ x[v][2] ∨ ... ∨ x[v][k]
At-most-one: ∀v, c≠c': ¬x[v][c] ∨ ¬x[v][c']
Conflict: ∀(u,v)∈E, ∀c: ¬x[u][c] ∨ ¬x[v][c]

This produces O(|V|·k) variables and O(|E|·k + |V|·k2) clauses. Modern CDCL SAT solvers (MiniSat, CaDiCaL) handle instances with thousands of nodes. The SAT encoding naturally supports incremental solving — increment k and re-solve.

Trade-offs: SAT loses the semantic structure CP exploits but benefits from decades of CDCL engineering. Works exceptionally well near phase transitions.

---

Approach 3 — MIP / ILP

min  k
s.t. Σ_c x[v][c] = 1           ∀v          (each vertex gets exactly one color)
     x[u][c] + x[v][c] ≤ 1     ∀(u,v)∈E,c  (no shared color on edges)
     x[v][c] ∈ {0,1}

LP relaxations are weak (fractional solutions abound), so MIP solvers lean heavily on branch-and-cut with clique inequalities. Better suited when combined with column generation (treating colors as patterns).

---

Example Model — MiniZinc (CP)

int: n = 5;            % number of vertices
int: k = 3;            % number of colors to try
int: m = 5;            % number of edges

array[1..m, 1..2] of int: edges =
  [| 1,2 | 2,3 | 3,4 | 4,5 | 5,1 |];

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: first vertex gets color 1
constraint color[1] = 1;

solve satisfy;

output [ "color = \(color)\n" ];

Run with k=2 → UNSAT; k=3 → solution found.

---

Key Techniques

1. Propagation — Forward Checking & Arc Consistency (AC-3)

When color[v] = c is assigned, AC-3 removes c from the domains of all neighbors. Bound consistency isn't meaningful here (discrete colors), but domain wipeout detection early in search is crucial. The DSATUR algorithm greedily assigns colors in order of saturation (number of distinct colors in the neighborhood) and is a remarkable constructive heuristic.

2. Symmetry Breaking

Graph coloring has massive color symmetry: any permutation of colors yields an equivalent solution. Without breaking this, a solver wastes exponential time on symmetric branches. The lex-leader constraint (color is lexicographically minimal among all equivalent colorings) is complete but expensive; practical variants fix the color of the first vertex and enforce that new colors are introduced in order.

3. Clique-Based Lower Bounds

The chromatic number χ(G) ≥ ω(G) where ω(G) is the clique number (size of the largest complete subgraph). Finding large cliques (itself NP-hard, but heuristically tractable) provides strong lower bounds that prune the search for the minimum k. Combined with fractional relaxations, this forms the backbone of branch-and-bound exact solvers like DSATUR + backtrack and Brelaz's algorithm.

---

Challenge Corner

💡 Think about this:

The graph coloring problem on perfect graphs (where χ(G) = ω(G) for every induced subgraph) is solvable in polynomial time. Interval graphs and chordal graphs are perfect.

Question: Can you exploit the chordal structure of a graph inside a CP model to make propagation complete — eliminating all backtracking? What global constraint would encode this?

As an extension: how would you model list coloring, where each vertex v has its own allowed set of colors L(v) ⊆ {1..k}? Does the SAT or CP model extend more naturally?

---

References

1. Rossi, van Beek & Walsh — Handbook of Constraint Programming (2006), Chapter 2: CSP fundamentals; Chapter 7: Graph problems.
2. Brélaz, D. — "New methods to color the vertices of a graph", CACM 1979. The classic DSATUR algorithm.
3. Gent, I. & Walsh, T. — "Phase transitions and annealing for graph colouring", ECAI 1996. Phase transition analysis in SAT/CSP.
4. OR-Tools CP-SAT documentation — [developers.google.com/optimization]((developers.google.com/redacted) — practical CP-SAT modeling with AddAllDifferent and AddForbiddenAssignments.

Generated by Constraint Solving — Problem of the Day · ● 2.4M · ◷

• expires on May 21, 2026, 12:07 PM UTC

[github-actions[bot]]

This discussion has been marked as outdated by Constraint Solving — Problem of the Day.

A newer discussion is available at Discussion #32350.