The four colour theorem says every planar map can be coloured this way. This example does not prove the theorem; it finds one concrete colouring for the EU neighbour graph by finite search, and the proof shows every neighbour test that the answer depends on.
Run it in the playground · Source
Give each EU country one of four colours so that countries sharing a border never share a colour. Ireland, Cyprus, and Malta have no land neighbours in the graph, so any colour will do for them; Germany borders eight countries.
color(red).
color(green).
color(blue).
color(yellow).
neighbours(belgium, [france, netherlands, luxemburg, germany]).
neighbours(netherlands, [belgium, germany]).
neighbours(germany, [netherlands, belgium, luxemburg, denmark, france, austria, poland, czech_republic]).
neighbours(ireland, []).
Four colours, and one neighbours/2 fact per country (27 in all).
valid_color(Place, Color, Assigned) :-
neighbours(Place, Neighbors),
\+ (member([Neighbor, Color], Assigned), member(Neighbor, Neighbors)).
color_places([]).
color_places([[Place, Color]|Tail]) :-
color_places(Tail),
color(Color),
valid_color(Place, Color, Tail).
four_color_answer(european_union, Coloring) :-
place_order(Places),
place_pairs(Places, Coloring),
once(color_places(Coloring)).
The tail is coloured first, so each new choice is tested against countries
that already have a colour. A colour is valid when no neighbour already holds
it. once/1 asks for one colouring, not all of them.
eyeprolog examples/map-four-color-search.pl
four_color_answer(european_union, [[belgium, yellow], [netherlands, green], [luxemburg, green], [france, blue], [germany, red], [italy, red], [denmark, green], [ireland, red], [greece, red], [spain, green], [portugal, red], [austria, yellow], [sweden, green], [finland, red], [cyprus, red], [malta, red], [poland, blue], [hungary, blue], [czech_republic, green], [slovakia, red], [slovenia, green], [estonia, red], [latvia, green], [lithuania, red], [bulgaria, green], [romania, red], [croatia, red]]).
One colouring that uses all four colours. Belgium needs the fourth colour (yellow), because France, the Netherlands, and Germany around it already use blue, green, and red.
step(color_places([[croatia, red]]),
rule(37),
['Place' = croatia, 'Color' = red, 'Tail' = []],
[color_places([]), color(red), valid_color(croatia, red, [])]).
The proof builds the colouring from the end of the list: Croatia, coloured
first, gets red because nothing is coloured yet. Each later step adds one
country and one valid_color/3 test against the countries already coloured.
condition('C1', resolution, ok, 116).
condition('C5', re_decision, ok, 1).
condition('C6', boundary_consistency, ok, 0).
steps(144).
verified(116).
trusted(27).
verdict(checked_with_obligations).
All 116 rule and fact steps replay correctly. The 27 trusted steps are the
\+ neighbour tests, one per country: the checker cannot replay “no
neighbour has this colour” as a derivation, so it lists each as an
obligation(absent, …) that the answer rests on. Each is a finite membership
test you can confirm by reading the list it names.
yellow from the colours. Does a three-colouring of this graph
exist, and how long does the search take to decide?place_order/1 to start with Germany. Does the answer change?once/1 and count how many colourings the search can find for a small
part of the map, such as the Benelux countries.Learn more in The Art of EyeProlog, Chapter 10.