It's possible to color all countries on political map using only 4 colors. This is example from Wolfram Mathematica's website (using FindInstance):

Any map or vertices on planar graph can be colored using at most 4 colors. This is quite interesting story behind this. This is a first serious proof finished using automated theorem prover (Coq): https://en.wikipedia.org/wiki/Four_color_theorem.

Another example where I use graph coloring: https://yurichev.com/blog/tiling_Z3/.

Now what about something practical? Four-colored maps are not used in cartography, however, graph coloring is used in scheduling.

I've found this problem in the "Discrete Structures, Logic and Computability" book by James L. Hein:

Suppose some people form committees to do various tasks. The problem is to schedule the committee meetings in as few time slots as possible. To simplify the discussion, we’ll represent each person with a number. For example, let S = {1, 2, 3, 4, 5, 6, 7} represent a set of seven people, and suppose they have formed six three-person committees as follows: S1 = {1, 2, 3}, S2 = {2, 3, 4}, S3 = {3, 4, 5}, S4 = {4, 5, 6}, S5 = {5, 6, 7}, S6 = {1, 6, 7}. We can model the problem with the graph pictured in Figure 1.4.4, where the committee names are the vertices and an edge connects two vertices if a person belongs to both committees represented by the vertices. If each committee meets for one hour, what is the smallest number of hours needed for the committees to do their work? From the graph, it follows that an edge between two committees means that they have at least one member in common. Thus, they cannot meet at the same time. No edge between committees means that they can meet at the same time. For example, committees S1 and S4 can meet the first hour. Then committees S2 and S5 can meet the second hour. Finally, committees S3 and S6 can meet the third hour. Can you see why three hours is the smallest number of hours that the six committees can meet?

And this is solution:

#!/usr/bin/env python import itertools from z3 import * # 7 peoples, 6 committees S={} S[1]=set([1, 2, 3]) S[2]=set([2, 3, 4]) S[3]=set([3, 4, 5]) S[4]=set([4, 5, 6]) S[5]=set([5, 6, 7]) S[6]=set([1, 6, 7]) committees=len(S) s=Solver() Color_or_Hour=[Int('Color_or_hour_%d' % i) for i in range(committees)] # enumerate all possible pairs of committees: for pair in itertools.combinations(S, r=2): # if intersection of two sets has *something* (i.e., if two committees has at least one person in common): if len(S[pair[0]] & S[pair[1]])>0: # ... add an edge between vertices (or persons) -- these colors (or hours) must differ: s.add(Color_or_Hour[pair[0]-1] != Color_or_Hour[pair[1]-1]) # limit all colors (or hours) in 0..2 range (3 colors/hours): for i in range(committees): s.add(And(Color_or_Hour[i]>=0, Color_or_Hour[i]<=2)) assert s.check()==sat m=s.model() #print m schedule={} for i in range(committees): hour=m[Color_or_Hour[i]].as_long() if hour not in schedule: schedule[hour]=[] schedule[hour].append(i+1) for t in schedule: print "hour:", t, "committees:", schedule[t]

Result:

hour: 0 committees: [1, 4] hour: 1 committees: [2, 5] hour: 2 committees: [3, 6]

If you increase total number of hours to 4, the result is somewhat sparser:

hour: 0 committees: [3] hour: 1 committees: [1, 4] hour: 2 committees: [2, 5] hour: 3 committees: [6]

Please drop me email about any bug(s) and suggestion(s):