Graph colouring

Graph colouring is the “hello world” of constraint solving, and it shows Savanty’s whole pipeline in a handful of lines. Colour every node with one of k colours so that no edge joins two nodes of the same colour.

The encoding, verbatim

node(n1). node(n2). node(n3).
1 { assign(N, c1); assign(N, c2); assign(N, c3) } 1 :- node(N).  % one colour per node
:- assign(n1, C), assign(n2, C).   % edge n1-n2: differ
:- assign(n2, C), assign(n3, C).   % edge n2-n3: differ
#show assign/2.

One choice rule for the palette; one integrity constraint per edge. That is the entire model, and it is exactly what Savanty’s generator emits from an English description like “colour these three regions with three colours so adjacent regions differ.”

Where the guarantee shows

Reduce the palette to two colours on a triangle and the problem becomes impossible. Clingo returns UNSAT, and Savanty’s minimal unsatisfiable core returns precisely the three adjacency constraints that clash — a definitive, localized explanation rather than a shrug.

Many practical problems reduce to colouring: register allocation, frequency assignment, and exam scheduling all become “assign one label per item so conflicting items differ.” Whenever your conflicts form a graph, this encoding applies — see the full pipeline.