How can this planar map be coloured using $4$ colours?

Question

I'm working on an algorithm to colour a map drawn in an editor using 4 colours, as a visual demonstration of the four colour theorem. However, my (imperfect) algorithm was able to colour all maps except this one, which after giving it a go myself I struggled to do. I was also unable to collapse it into an 'untangled' graph, so it's possible there's some illegality about it I've not fully understood (or I'm just bad at graph theory). I'd appreciate any help with solving this, and if possible an explanation of/link to a good algorithm to go about solving problems of this style.

Here's the map:

Answer 1

One possible algorithm would be the following:

1. Take the map, and turn it into a graph.
2. Delete all nodes with degree $<4$.
3. Turn the graph into a clause set (a special form of a logical formula) by doing the following:
   a. For every edge $A\to B$ (where, $A,B$ are vertices of the graph), we add the formula $\lnot \left((A_0\Leftrightarrow B_0) \land(A_1\Leftrightarrow B_1) \right)$ as a clause into the clause set.
4. We run DPLL (or the simpler version, Davis-Putnam) on this clause set.
5. DPLL will give us a satisfying model. The color (whereas our colors are $0,1,2,3$) of a node $A$ is given by our model as $A= A_0 + 2\cdot A_1$
6. Determine for every deleted node a possible coloring using the model.

The underlying idea is the following:
Every border in the map says as much as "the bordering areas mustn't be equal" (in terms of color).

By letting our colors be $0,1,2,3$, we can represent each color in binary as $2^0\cdot z_0 + 2^1 \cdot z_1$.
As two numbers are equal iff all their bits are equal, we get for every border in the map between two areas $A,B$ the logic formula: $$\lnot \left((A_0\Leftrightarrow B_0) \land(A_1\Leftrightarrow B_1) \right)$$

Now a 4-coloring is a coloring where this formula holds for exactly every border.

Answer 2

This is a possible coloring. Done by hand, either really lucky or not that difficult. Perhaps it'll help with debug of the algorithm and shows that this map is definitely legal.

Answer 3

The map you have given can be simplified considerably by deleting some of the regions. If you have a region which is adjacent to $1, 2$ or $3$ other regions, you can simply delete it, or amalgamate it into some adjoining region, because when you colour the rest and put the region back, there will be a colour you can use.

The map you have looks complicated, but I can spot five regions you can simply delete in this example. And once you have deleted those you can possibly iterate the process.

That gives a rather simpler map to colour.