🧩 Constraint Solving POTD:Graph Coloring #27186
Closed
Replies: 1 comment
-
|
This discussion has been marked as outdated by Constraint Solving — Problem of the Day. A newer discussion is available at Discussion #27344. |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
Graph Coloring is a cornerstone of constraint satisfaction, with elegant models in CP, SAT, and MIP — and direct industrial relevance in register allocation, frequency assignment, and timetabling.
Problem Statement
Graph Coloring asks: given a graph
G = (V, E)andkcolors, can you assign a color to each vertex so that no two adjacent vertices share the same color?Concrete instance (Petersen graph, k=3):
Vertices:
{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}Edges (outer pentagon + inner pentagram + spokes):
{(0,1),(1,2),(2,3),(3,4),(4,0), (5,7),(7,9),(9,6),(6,8),(8,5), (0,5),(1,6),(2,7),(3,8),(4,9)}Input: Graph
G, integerkOutput: Assignment
color: V → {1..k}such that∀(u,v) ∈ E: color(u) ≠ color(v), or UNSAT if impossible.The chromatic number
χ(G)is the minimumkfor which a valid coloring exists.Why It Matters
k = number of registersdetermines whether spilling is needed.Modeling Approaches
Approach 1: Constraint Programming (CP)
Decision variables:
color[v] ∈ {1..k}for each vertexv ∈ VConstraints:
Symmetry breaking (crucial for efficiency):
Trade-offs:
alldifferenton clique subsets strengthens propagation.≠constraints is cheap but propagates weakly on sparse graphs.Approach 2: SAT Encoding
Boolean variables:
x[v][c] = trueiff vertexvgets colorcAt-least-one per vertex:
At-most-one per vertex (pairwise or commander encoding):
Edge constraints:
Trade-offs:
O(|V|·k2 + |E|·k)— manageable for moderatek.Approach 3: MIP Formulation
Variables:
x[v][c] ∈ {0,1},w[c] ∈ {0,1}(is colorcused?)Objective:
minimize ∑_c w[c](find chromatic number)Constraints:
Trade-offs:
k); LP relaxation provides lower bounds.Example Model (MiniZinc)
Key Techniques
1. Clique-based propagation
Identify maximal cliques (e.g., via greedy or Bron-Kerbosch). An
alldifferentconstraint over a clique of sizeqimmediately establishes a lower boundχ(G) ≥ qand enforces stronger arc consistency than pairwise≠.2. DSATUR heuristic (variable ordering)
At each search node, branch on the vertex with the highest saturation degree — the number of distinct colors already used by its neighbors. DSATUR often finds optimal colorings quickly and makes an excellent value-ordering companion (smallest unused color first).
3. Symmetry breaking via canonical forms
Colors are inherently symmetric (swapping all 1s and 2s gives another valid coloring). Breaking this symmetry with lex-leader constraints or the first-fail color assignment rule (
color[v] ≤ 1 + max used color so far) can reduce search by a factor ofk!.Challenge Corner
References
Beta Was this translation helpful? Give feedback.
All reactions