Solve a four colour diagram problem using an SMT (Integer) solver

This article is a development and simpler version of Colour a diagram with 4 collars using a Python sat solver  In the previous version binary logic was used to solve the problem ie. Is region 1 red ( yes or no ), Is region 1 Blue ( yes or no) etc. In this version of the problem integers are used to represent the colour for each region. 1=Red, 2=Blue, 3=Green, 4=Yellow.

Take this simple diagram with regions marked 1 to 9. Given the constraint that areas with shared sides cannot have the same colour (touching corners is ok), how can this diagram be coloured with just 4 colours ? This type of problem was originally called called Guthrie's problem after F. Guthrie, who first conjectured in 1852 that "Only 4 colours are needed for any flat diagram."  Reference : Four Colour Theorem

Original Diagram

The first leap we take is to simplify the problem by translating spaces into dots and boundaries into lines.  This example diagram shows how any space can be represented by a dot and the boundaries between regions as a line. When each connected dot (which represents a region) has a different colour, we have our answer. Using points and lines, to represent areas and boundaries simplifies the problem without changing the constraints of the problem.

(Diagram from wikipedia)

From the starting diagram give each region dot a number then join those dots where regions share a boundary. Each of these lines should only cross one region boundary between two neighbouring areas. This completes the translation from map to (non-directional) network graph. Every boundary between two areas is crossed by a single line that joins the numbered points.

Netlist 1

We can list the boundary edges (yellow lines that join up dots) by using the start and finish region numbers.  For example region 1 has a boundary with region 2. This would be listed as ‘12’  and/or identically as  ‘21’ depending which end was used as the starting point. 

Each point generates one joining line for each neighbour. The number of lines that comes from any point must equal the number of boundaries with neighbour regions.

These lines are listed here as two digits being the boundaries between each region, each row showing the lines from each point :

Point	In contact with	Number of Vertex
1	2,3,5,9	4
2	1,4,8,9	4
3	1,4,5,6	4
4	2,3,7,8	4
5	1,3,6,8,9	5
6	3,5,7	3
7	4,6,8	3
8	2,4,5,7,9	5
9	1,2,5,8	4
TOTAL		36 << Must be an even number as each line has two ends. The Number of Vertex must equal the number of 0s in the matching row and column in the check matrix below.

This gives us the input data for the problem

1 2,1 3,1 5,1 9,
2 1,2 4,2 8,2 9,
3 1,3 4,3 6,3 5,
4 2,4 3,4 7,4 8
5 1,5 3,5 6,5 8,5 9,
6 7,6 3,6 5,
7 6,7 8,7 4,
8 2,8 4,8 5,8 7,8 9
9 1,9 2,9 5,9 8

This list could be easily simplified to remove duplicates ( 12 is effectively the same path as 21) by removing each entry where the second digit is smaller than the first.

This is where we have to take the next small jump and rephrase the connections into logical statements that describe the current graph situation in a way suitable for automatic solving. The structured language is SMTLIB version 2 than can be used as input to many different solvers such as Z3 and Math5. First we say each region must have one (but any) colour and then each region pairs that touch must have different colours.

The rules are generated as :

1. Every region can have any colour value from the list of 1,2,3,4
2. Regions that touch and share a border must have distinct, unequal colour values.

The following lines are generated which set up the solver to use Integer logic and warn that we will need the actual values as answers. The for each region R1 to R9 an Integer value is declared and it's range is set to greater than 0 and less then 5 Ie: 1 .. 4

(set-logic LIA)

(set-option :produce-models true)

(set-option :produce-assignments true)

(declare-const R1 Int)

(assert (and (> R1 0) (< R1 5)))

(declare-const R2 Int)

(assert (and (> R2 0) (< R2 5)))

.....

.... R3 to R9 are also declared and set using similar lines. Next we set the constrains between the regions in the form that R1 and R2 must have distinct values. Finally the instruction file is completed with a request to check for an answer then finally show the answer value for each region.

(assert (distinct R1 R2))

(assert (distinct R1 R3))

(assert (distinct R1 R5))

(assert (distinct R1 R9))

(assert (distinct R2 R1))

(assert (distinct R2 R4))

.....

(check-sat)
(get-value (R1 R2 R3 R4 R5 R6 R7 R8 R9 ))
(exit)

The full file is then passed to the solver that will generate a line of "sat" or "unsat" depending on if the problem can be solved along with the colour assignments for each region.

$ ./makeSMT.pl | ../solver_m5 

sat

( (R1 4)

  (R2 3)

  (R3 1)

  (R4 4)

  (R5 3)

  (R6 4)

  (R7 3)

  (R8 2)

  (R9 1) )

Here is the list of colours to be applied to the regions for the solution. 

1=Red R3, R9

2=Blue R8 

3=Green R2, R5, R7

4=Yellow R1, R4, R6

A correct 4 colour solution.

Just a little harder

If we take the above problem and adjust the regions 3 and 6 we see the problem evolve. However adjusting the netlist to add the touching regions 3 & 2 and 6 & 8 the problem is solved using the same method.

Adjusted version of the problem above giving netlist 2

Solved !

A harder problem from Martin Gardner

This 110 region diagram was original proposed as requiring 5 colours as an April Fools joke. Lets see if we can generate a four colour solution. Starting with the diagram each region is numbered.

McGregor Map from 1975

Make a list of each region and just the *higher* numbered regions that they touch.

Extract the numbers and make some perl lines such as 

%regions_4 = ( #McGregorLines.txt

"R1", "R2,R3,R4,R5,R6,R7,R8,R9,R10,R11,R20,R100,R109,R110",

"R2", "R3,R12,R101,R102,R103,R104,R105,R106,R110",

"R3", "R4,R13,R12",

"R4", "R5,R14,R13",

"R5", "R6,R15,R14",

.......

From this data structure build the lines needed for an SMTLIB solver in the same way as for the smaller puzzle above but we have 110 regions which generates about 550 lines.

(set-logic LIA)

(set-option :produce-models true)

(set-option :produce-assignments true)

(declare-const R1 Int)

(assert (and (> R1 0) (< R1 5)))

(declare-const R10 Int)

(assert (and (> R10 0) (< R10 5)))

.....snip

(declare-const R98 Int)

(assert (and (> R98 0) (< R98 5)))

(declare-const R99 Int)

(assert (and (> R99 0) (< R99 5)))

(assert (distinct R1 R2))

(assert (distinct R1 R3))

(assert (distinct R1 R4))

(assert (distinct R1 R5))

.......snip

(assert (distinct R1 R109))

(assert (distinct R1 R110))

(assert (distinct R10 R11))

......snip

(assert (distinct R102 R103))

(assert (distinct R103 R104))

......snip

(assert (distinct R99 R109))
(check-sat)

(get-value (R1 R10 R100 R101 R102 R103 R104 R105 R106 R107 R108 R109 R11 R110 R12 R13 R14 R15 R16 R17 R18 R19 R2 R20 R21 R22 R23 R24 R25 R26 R27 R28 R29 R3 R30 R31 R32 R33 R34 R35 R36 R37 R38 R39 R4 R40 R41 R42 R43 R44 R45 R46 R47 R48 R49 R5 R50 R51 R52 R53 R54 R55 R56 R57 R58 R59 R6 R60 R61 R62 R63 R64 R65 R66 R67 R68 R69 R7 R70 R71 R72 R73 R74 R75 R76 R77 R78 R79 R8 R80 R81 R82 R83 R84 R85 R86 R87 R88 R89 R9 R90 R91 R92 R93 R94 R95 R96 R97 R98 R99 ))

(exit)

Present the SMTLIB file to the solver and gather the output. Both the Math5 solver and the Z3 solver were used to check the answers. Both the solvers take about 0.5s on a MacBookPro 2011 with a 2.2Ghz Core i7

sat

( (R1 4)

  (R10 1)

  (R100 2)

  (R101 1)

  (R102 3)

  (R103 1)

  (R104 4)

  (R105 3)

  (R106 1)

.....snip

Apply the colours to the original regions on the diagram ... both solvers appear to have created valid but different answers.

1=Red, 2=Blue, 3=Green, 4=Yellow.

M5 Solver

Z3 Solver

and Finally .....

Our favourite question came up on the game show The Chase last week.

Contestant said 6 but we know the answer is 4.