# Four-colouring the McGregor map
A good approach to this sort of problem is to represent the map as a graph. Regions of the map are represented as vertices, and borders between regions as edges between the corresponding nodes.
Due to the complexity of the McGregor map, this problem is really two-fold - before we can begin to work with the final graph, we must first obtain it, i.e. identify all of the different map regions and borders between them. Doing this by hand is a laborious and error-prone process, so this certainly calls for automation.
## Finding map regions and generating a graph
I chose to use a vector graphics (SVG) version of the map for this, because this allows working with each region of the map as a distinct unit in code. JavaScript makes this fairly nice and easy -- hence also why this submission is an HTML file.
Conveniently, there is an SVG file of the McGregor map available online ([source](https://www.cs.cmu.edu/~bryant/boolean/macgregor.html)), which I have embedded in this document.
**The basic technique boils down to this:**
1. Assign an identifier to each region (vertex):
\[ V := \left\{ v \:|\: 1 \leq v \leq 110 \right\} \]
2. Identify every region's possible neighbours (rectangular bounding box is adjacent or intersects)
3. Find the corners of every region's outline
4. Find the actual neighbours for each region by checking, for each of its possible neighbours, whether its corners intersect with the neighbour's outline (or vice-versa).
5. For each region \( v \) and each of its neighbours \( w \), add an edge \( \left( v, w \right) \) between itself and each of its actual neighbours to an initially empty set \( E \) -- but only if neither \( \left( v, w \right) \) nor \( \left( v, w \right) \) are in the set yet.
## Obtaining a SAT-solvable CNF
This part is quite straightforward; there are two important constraints:
1. No two adjacent regions (vertices that share an edge) may have the same colour
2. Every region (vertex) must be assigned at least one colour
_**Note:** A region may have more than one colour assigned. Encoding the constraint _"Every region must be assigned at most one colour"_ would complicate the CNF substantially, and is not actually necessary to solve the task -- that being simply to prove that there exists at least one 4-colouring of the map, not a unique one. Additionally, extraneous colours can easily be removed from a found colouring, if necessary._
First, we define the atoms -- there are 110 regions as defined above, and 4 colours identified by \( C := \left\{ 1, 2, 3, 4 \right\} \). Thus, there are 440 atoms:
\[ \{ a_i \:|\: 1 \leq i \leq 440 \} \text{: Region } r = \left\lfloor \frac{a}{4} \right\rfloor \text{ has colour } c = \left\lfloor \frac{a}{4} \right\rfloor \]
Then, we can encode the constraints:
**Constraint 1** is encoded using the edges identified in step 1; for each edge we add one DNF clause per colour, encoding that at least one of the regions is NOT assigned that colour.
\[ \bigwedge \left\{ \bigwedge \left\{ \left( \neg a_{(110c)+v_i} \vee \neg a_{(110c)+v_j} \right) \:|\: c \in C \right\} \:|\: (v_i, v_j) \in E \right\} \]
**Constraint 2** is encoded using the atoms defined above; for each region \( v \), we add a DNF clause encoding that at least one of the corresponding atoms is true:
\[ \bigwedge \left\{ \bigvee \left\{ \left( a_{(110c) + v} \right) \:|\: c \in C \right\} \:|\: v \in V \right\} \]
Finally, this CNF can be encoded in DIMACS format (you may press one of the two buttons on the top right to do this) and processed by a SAT solver. The result, as expected, is that there does exist a 4-colouring of the McGregor map.
The file `output.txt` generated by `minisat mcgregor_dimacs.txt output.txt` may be imported on this page using the file selector, in order to visualize the found colouring.