You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Graph coloring is one of the most celebrated problems in combinatorics and constraint solving β simple to state, surprisingly deep to solve, and everywhere in practice.
Problem Statement
Given an undirected graph G = (V, E) and a set of k colors, assign a color to each vertex such that no two adjacent vertices share the same color. The smallest k for which this is possible is the graph's chromatic numberΟ(G).
With k = 3? β β e.g., [1βR, 2βG, 3βR, 4βG, 5βB]
Input: graph G, integer k Output: a coloring assignment color[v] β {1..k} for all v β V, or UNSAT if none exists.
Why It Matters
Register allocation in compilers: variables competing for CPU registers are modeled as graph nodes; edges represent conflicts; colors represent registers.
Frequency assignment in wireless networks: channels must differ between nearby base stations to avoid interference.
Timetabling & exam scheduling: courses sharing students cannot be scheduled in the same slot β this is exactly graph coloring on a conflict graph.
Printed circuit board layer minimization: nets that cross need different layers.
Modeling Approaches
1. Constraint Programming (CP)
Decision variables: color[v] β {1..k} for each vertex v.
for each edge (u, v) β E:
color[u] β color[v]
Symmetry breaking (crucial!): since any permutation of color labels is equivalent, add:
color[v1] = 1 // fix first vertex
color[v2] β {1, 2} // second vertex uses β€ 2 colors
... // lex-leader or similar
Trade-offs: CP propagation via arc consistency (AC) is strong on sparse graphs. The alldifferent global constraint doesn't apply directly here, but specialized graph-coloring global constraints (e.g., gcc) can tighten bounds.
2. Mixed-Integer Programming (MIP)
Binary variables: x[v][c] = 1 if vertex v gets color c; y[c] = 1 if color c is used.
minimize Ξ£ y[c]
subject to:
Ξ£_c x[v][c] = 1 β v (each vertex gets exactly one color)
x[u][c] + x[v][c] β€ 1 β (u,v)βE, β c (adjacent vertices differ)
x[v][c] β€ y[c] β v, c (color used if assigned)
x[v][c], y[c] β {0, 1}
Trade-offs: MIP LP relaxations give strong lower bounds on Ο(G). However, the model has |V|Β·k + k binary variables and |E|Β·k constraints β it scales poorly for large dense graphs without column generation.
3. SAT Encoding
For each vertex v and color c, introduce Boolean p[v][c].
At-least-one per vertex: p[v][1] β¨ p[v][2] β¨ ... β¨ p[v][k] At-most-one per vertex: Β¬p[v][c] β¨ Β¬p[v][c'] for all c β c' Conflict clauses per edge: Β¬p[u][c] β¨ Β¬p[v][c] for all (u,v) β E, all c
Trade-offs: Modern CDCL SAT solvers handle millions of variables efficiently. Binary search on k finds Ο(G). The encoding is clean but produces O(|V|Β·k2) clauses for the AMO constraints β commander-variable or product encodings can reduce this.
For every edge (u, v), AC removes values from color[u]'s domain that have no support in color[v]'s domain (and vice versa). For graph coloring this is straightforward: value c is supported in color[u] iff color[v]'s domain contains some c' β c.
2. Variable Ordering β DSATUR Heuristic
The DSATUR algorithm greedily colors vertices in order of saturation (number of distinct colors already used by neighbors). It produces near-optimal colorings in practice and is the basis for many exact branch-and-bound solvers. In CP search, adopting a DSATUR-inspired dynamic variable ordering (dom/deg or dom/wdeg) dramatically reduces search effort.
3. Symmetry Breaking via Lex-Leader Constraints
Color labels are interchangeable: any bijection on {1..k} yields an equivalent solution. Without symmetry breaking, the solver explores k! symmetric copies of every solution. The lex-leader approach adds:
color[first_vertex_colored_c] < c for c = 2..k
This alone can reduce search space by orders of magnitude.
Challenge Corner
π Can you determine Ο(G) without enumerating all possible k values separately?
One approach: optimize directly β add a variable k_used and minimize it, with color[v] β€ k_used for all v. Does this formulation propagate well? What are the trade-offs versus binary search over k?
π Bonus: For planar graphs, the Four Color Theorem guarantees Ο(G) β€ 4. Can you encode planarity as a constraint and exploit this bound in a solver?
References
Rossi, van Beek & Walsh β Handbook of Constraint Programming (2006), Chapter 4: Graph Coloring as a CSP benchmark.
Brelaz, D. β "New methods to color the vertices of a graph," CACM 22(4), 1979. (Introduces DSATUR)
Trick, M. β [Constraint Programming tutorial on Graph Coloring]((mat.gsia.cmu.edu/redacted) β accessible overview with benchmark instances.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
Uh oh!
There was an error while loading. Please reload this page.
-
Graph coloring is one of the most celebrated problems in combinatorics and constraint solving β simple to state, surprisingly deep to solve, and everywhere in practice.
Problem Statement
Given an undirected graph
G = (V, E)and a set ofkcolors, assign a color to each vertex such that no two adjacent vertices share the same color. The smallestkfor which this is possible is the graph's chromatic numberΟ(G).Concrete instance β 5-node cycle graph (C5)
k = 2? β β odd cycle, impossible.k = 3? β β e.g.,[1βR, 2βG, 3βR, 4βG, 5βB]Input: graph
G, integerkOutput: a coloring assignment
color[v] β {1..k}for allv β V, or UNSAT if none exists.Why It Matters
Modeling Approaches
1. Constraint Programming (CP)
Decision variables:
color[v] β {1..k}for each vertexv.Symmetry breaking (crucial!): since any permutation of color labels is equivalent, add:
Trade-offs: CP propagation via arc consistency (AC) is strong on sparse graphs. The
alldifferentglobal constraint doesn't apply directly here, but specialized graph-coloring global constraints (e.g.,gcc) can tighten bounds.2. Mixed-Integer Programming (MIP)
Binary variables:
x[v][c] = 1if vertexvgets colorc;y[c] = 1if colorcis used.Trade-offs: MIP LP relaxations give strong lower bounds on
Ο(G). However, the model has|V|Β·k + kbinary variables and|E|Β·kconstraints β it scales poorly for large dense graphs without column generation.3. SAT Encoding
For each vertex
vand colorc, introduce Booleanp[v][c].At-least-one per vertex:
p[v][1] β¨ p[v][2] β¨ ... β¨ p[v][k]At-most-one per vertex:
Β¬p[v][c] β¨ Β¬p[v][c']for allc β c'Conflict clauses per edge:
Β¬p[u][c] β¨ Β¬p[v][c]for all(u,v) β E, allcTrade-offs: Modern CDCL SAT solvers handle millions of variables efficiently. Binary search on
kfindsΟ(G). The encoding is clean but producesO(|V|Β·k2)clauses for the AMO constraints β commander-variable or product encodings can reduce this.Example CP Model (MiniZinc)
Key Techniques
1. Propagation β Arc Consistency (AC-3/AC-4)
For every edge
(u, v), AC removes values fromcolor[u]'s domain that have no support incolor[v]'s domain (and vice versa). For graph coloring this is straightforward: valuecis supported incolor[u]iffcolor[v]'s domain contains somec' β c.2. Variable Ordering β DSATUR Heuristic
The DSATUR algorithm greedily colors vertices in order of saturation (number of distinct colors already used by neighbors). It produces near-optimal colorings in practice and is the basis for many exact branch-and-bound solvers. In CP search, adopting a DSATUR-inspired dynamic variable ordering (
dom/degordom/wdeg) dramatically reduces search effort.3. Symmetry Breaking via Lex-Leader Constraints
Color labels are interchangeable: any bijection on
{1..k}yields an equivalent solution. Without symmetry breaking, the solver exploresk!symmetric copies of every solution. The lex-leader approach adds:This alone can reduce search space by orders of magnitude.
Challenge Corner
References
Have a solution, a question, or a different modeling angle? Share it in the replies! π
Beta Was this translation helpful? Give feedback.
All reactions