🧩 Constraint Solving POTD:Problem of the Day: Graph Coloring

[github-actions[bot]]

Problem Statement

Assign a color to each vertex of a graph such that no two adjacent vertices share the same color, using the minimum number of colors possible (the graph's chromatic number).

Concrete Instance:
Consider a map with 5 regions arranged like this:

    A --- B
    |\ /|
    | X |
    |/ \|
    D --- C

• Vertices: {A, B, C, D, E} (where E is in the center, connecting A-B-C-D in a cycle)
• Edges: A-B, B-C, C-D, D-A, A-E, B-E, C-E, D-E
• Question: What is the minimum number of colors needed?

Input: Graph G = (V, E) where V is a set of vertices and E is a set of edges.
Output: A function color: V → {1, 2, ..., k} such that for all edges (u, v) ∈ E, color(u) ≠ color(v), and k is minimized.

Why It Matters

Map Coloring & Geographic Planning: Cartographers and urban planners use graph coloring to ensure adjacent regions have distinct visual colors for clarity. The famous Four Color Theorem guarantees planar maps need at most 4 colors.

Register Allocation: Compiler optimizers solve graph coloring to assign processor registers to program variables, minimizing memory spills and improving code performance.

Frequency Assignment: Telecommunications engineers color a graph of towers to assign radio frequencies such that interfering towers (adjacent nodes) don't use overlapping bands.

Timetabling: Universities color a graph of exam courses, where edges connect courses sharing students. Adjacent courses (conflicting students) must have different exam time slots.

Modeling Approaches

Approach 1: Constraint Programming (Domain-based)

Decision Variables: color[v] ∈ {1, 2, ..., k} for each vertex v ∈ V, where k is an upper bound (e.g., |V| or a known upper bound like Δ+1, where Δ is max degree).

Constraints:

• color[u] ≠ color[v] for all (u, v) ∈ E (stated as a disequality constraint)
• Optional: Lexicographic ordering on color assignments to break symmetries: color[v1] ≤ color[v2] if v1 < v2 (in some ordering)

Strengths: Declarative, exploits domain consistency and specialized global constraints like all_different. Efficient propagation can prune the search space dramatically.

Weaknesses: Simple formulation can be symmetric (many equivalent colorings swap color labels), requiring symmetry-breaking constraints. Naive all_different propagation alone may not be tight enough for dense graphs.

---

Approach 2: Integer Linear Programming (ILP)

Decision Variables:

• Binary variables x[v, c] ∈ {0, 1}: true if vertex v is assigned color c
• Continuous variable k ≥ 0: the number of colors used (to minimize)

Constraints:

• Exactly one color per vertex: Σ_c x[v, c] = 1 for all v ∈ V
• Edge constraint: x[u, c] + x[v, c] ≤ 1 for all (u, v) ∈ E and all c (adjacent vertices cannot share a color)
• Color usage tracking: k ≥ c · (1/|V|) · Σ_v x[v, c] or use a big-M formulation to count active colors

Objective: Minimize k

Strengths: Leverages mature LP/MIP solvers (CPLEX, Gurobi). Can incorporate side constraints easily (e.g., costs per color, preferred colors for certain vertices).

Weaknesses: Linear relaxation is loose for chromatic number. Requires a large number of binary variables (O(|V| · k)), making it expensive for large graphs. Less natural representation than CP.

---

Approach 3: SAT-based Encoding

Propositional Variables: x[v, c] ∈ {true, false}: vertex v has color c

Clauses (in CNF):

• Exactly-one clause: (x[v, 1] ∨ x[v, 2] ∨ ... ∨ x[v, k]) ∧ Π_{c1 < c2} (¬x[v, c1] ∨ ¬x[v, c2])
• Edge constraints: (¬x[u, c] ∨ ¬x[v, c]) for all (u, v) ∈ E and all c (a clause saying "not both u and v are color c")

Search: Run a SAT solver (MiniSat, Glucose, CaDiCaL). Iteratively increase k from a lower bound until SAT returns satisfiable.

Strengths: Automatic conflict analysis and clause learning lead to powerful pruning. Modern SAT solvers are highly optimized.

Weaknesses: Encoding overhead; requires iterating on k. Less intuitive than CP for those new to SAT.

Example: CP Model (Pseudo-code)

# Pseudo-code in MiniZinc-like syntax
int: n = 5;  % number of vertices
int: max_k = n;  % upper bound on colors
set of int: Vertices = 1..n;
set of int: Colors = 1..max_k;

% Edge list: {(1,2), (2,3), (3,4), (4,1), (1,5), (2,5), (3,5), (4,5)}
set of int: Edges = {(1,2), (2,3), (3,4), (4,1), (1,5), (2,5), (3,5), (4,5)};

% Decision variable: color assignment
array[Vertices] of var Colors: color;

% Objective: minimize colors used
var int: k = max(color);

% Constraints: no two adjacent vertices have the same color
constraint forall((u, v) in Edges)(color[u] != color[v]);

% Symmetry-breaking: vertices colored in non-decreasing order
constraint forall(i in Vertices diff {max(Vertices)})(
  color[i] <= color[i+1] + 1
);

solve minimize k;

This model is compact and directly expresses the problem. The solver uses arc-consistency and specialized global constraint propagators to prune infeasible branches.

Key Techniques

1. Arc Consistency (AC-3 Algorithm)

Arc consistency iteratively removes values from variable domains that have no supporting assignment in a neighboring variable. For graph coloring, this means: if a vertex v is assigned color c, all neighbors' domains shrink to exclude c. Specialized propagators like all_different achieve stronger consistency (domain consistency or bound consistency) efficiently.

2. Greedy Heuristics & Ordering

A simple greedy coloring (e.g., "color vertices in order of descending degree") often gives a good upper bound quickly. In branch-and-bound, this upper bound prunes many branches early. More sophisticated heuristics like the Largest Degree First (LDF) or Saturation Degree ordering (color the vertex whose neighbors use the most colors) guide search toward tight lower bounds.

3. Symmetry-Breaking & Normalization

Graph coloring is highly symmetric: swapping color labels 1 and 2 yields an equivalent solution. CP solvers mitigate this by imposing ordering constraints (e.g., vertex 1 always gets color 1) or channeling variables to a canonical form. SAT solvers use clause learning and restart strategies to recover from thrashing on symmetric branches.

4. Lower Bounds via Cliques & Fractional Chromatic Number

A clique (complete subgraph) of size ω requires at least ω colors. Computing a maximum clique provides a lower bound. The fractional chromatic number (via LP relaxation) provides a tighter bound but is expensive to compute. These bounds drive branch-and-bound or integer programming algorithms.

Challenge Corner

Open Questions for You:

1. Symmetry Reduction: The concretely encoded CP model above uses color[i] <= color[i+1] + 1 to break color-label symmetry. Can you generalize this to a more efficient formulation that doesn't enforce a total order on vertices but still eliminates most symmetric solutions?

2. Hybrid Reasoning: What if you first compute a lower bound using a maximum clique algorithm, then feed that into a SAT solver as a clause? How would such a hybrid strategy compare to pure SAT or pure CP?

3. Parameterized Complexity: Graph coloring is NP-hard in general. However, if the graph's treewidth is bounded (a structural parameter), the problem becomes tractable. How would you exploit treewidth decomposition to solve coloring more efficiently?

4. Real-World Twist: In the register allocation application, each vertex (variable) has a lifetime interval during which it must reside in a register. Vertices with non-overlapping lifetimes don't conflict. How would you model this constraint efficiently? Does it change the complexity?

References

1. Rossi, F., van Beek, P., & Walsh, T. (Eds.). Handbook of Constraint Programming (Chapter 2–3 on Constraint Propagation and CSP Techniques). Elsevier, 2006.
   → Essential reference for CP fundamentals and global constraints.

2. Jensen, T. R., & Toft, B. Graph Coloring Problems. Wiley, 1995.
   → Comprehensive monograph on algorithmic and theoretical aspects of chromatic numbers.

3. Geoff Knottenbelt (École Polytechnique). Satisfiability and SAT Solvers (Course Notes & Survey).
   → Accessible introduction to SAT-based encodings of CSP problems.

4. Wikipedia: Graph Coloring & Four Color Theorem (accessible starting point)
   → Good visual examples and references to planarity, applications, and historical context.

---

What coloring techniques do you find most effective? Share your solver implementations, benchmarks, or real-world applications in the discussion below!

Generated by 🧩 Constraint Solving — Problem of the Day · haiku45 · 8.54 AIC · ⌖ 4.42 AIC · ⊞ 5.8K · ◷

• expires on Aug 11, 2026, 4:10 AM UTC-08:00

[github-actions[bot]]

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

A newer discussion is available at Discussion #50541.