One possible algorithm would be the following:
- Take the map, and turn it into a graph.
- Delete all nodes with degree $<4$.
- 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.
- We run DPLL (or the simpler version, Davis-Putnam) on this clause set.
- 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$
- 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.