Download all 15 colored fullerenes taken from here: https://networks.skewed.de/net/fullerene_structures
This is an example for the C2940 Fullerene.

Download all 15 colored fullerenes taken from here: https://networks.skewed.de/net/fullerene_structures
This is an example for the C2940 Fullerene.

On this great website https://networks.skewed.de/net/fullerene_structures, you can view and download fullerene structures in various formats.
Fullerenes are a perfect playground to test my four color algorithm.

I used the C6000 fullerene. 6000 atoms! A fullerene is an allotrope of carbon. Its molecules consist of carbon atoms connected by single and double bonds. A perfect 3-regular planar graphs ready to be tested.

And this is the four colored version you can play with, created using:
# python3 4ct.py -p planar_inputs/C6000.planar -c 2354 -o C6000

This zip file includes the C6000.dot + C6000.edgelist files.
See you around!
I converted the Sage implementation to a pure Python / Networkx solution … and improved the code, which will need extra improvement.
| Sage | Python3 + Networkx | |
| Random graph creation | 17 min 59 s * RandomTriangulation | 22 s * Custom |
| Planar embedding | 16 min 09 s * dual + set_embedding=True | 0 s * Not necessary |
| Elaboration | 2 min 12 s | 1 min 58 s |

Here is the file:
Other run:
| Sage | Python3 + Networkx | |
| Random graph creation | 3 min 19 s | 6 s |
| Planar embedding | 2 min 44 s | 0 s |
| Elaboration | 14 s | 23 s |
This is what I will be working for a while. Restart is difficult, but necessary.
Why use Reinforcement Learning for Graph coloring?
In my Python application, that works on 3-regular planar graph, deciding which is the order of the edges to remove can be non-trivial. A naive approach randomly picks edges from F2 faces, F3, F4 or F5. This is the approach I used :-(. It leads to impasses when rebuilding the map. See https://4coloring.wordpress.com/2014/08/27/four-color-theorem-experimenting-impasses-as-in-life/
But a reinforcement learning agent can learn to make better selections over time to reduce color conflicts, I hope :-), and shed light on some properties of the graph that can be used in the proof.
The code will be here: https://github.com/stefanutti/maps-coloring-python
Remove one edge at a time from F2, F3, F4, or F5 faces. These faces represent the basic unavoidable set. This process will reduce the map to three faces, including the ocean as the external area. Afterward, I will restore the edges in reverse order, consistently working with 3-regular planar graphs. I will consider Tait coloring of the edges and apply, when necessary, Kempe’s chain color switching to the edges.

For the Agent:

To color Voronoi graphs using the algorithm here https://github.com/stefanutti/maps-coloring-python, it is necessary to do some adjustments first:
It is known that we can also suppose that exactly three edges meet at each vertex since maps that have vertexes with more than three edges can be easily simplified without affecting the search of the coloring. In other words, if you can find a coloring for the map on the right, you can use the same coloring for the original map on the left.

Here is an example of these steps applied to the following Voronoi diagram. Three vertices have a degree greater than three.

If you can prove that it is possible to decompose a 3-regular graph into cycles, all with even length, you have also proved the four color theorem.
I think this fact is already known, but I never paid too much attention to it before.
Naturally, also the opposite is true: since the 4CT is true, it means that it is possible to color it, and also get the Tait coloring. And for any two colors you choose (for example Red and Green), the related Kempe cycles form a partition of the graph and each cycle has an even number of edges.
Once the decomposition is found, since the cycles have an even number of edges, it is possible to color the edges of a cycle with two alternate colors (for example Red and Green), forming this way Kempe cycles. When all cycles are colored (with R and G), it is possible to use a third color (for example Blue) to color the remaining edges.
The resulting graph will have a Tait coloring for all edges, which is equivalent to coloring all faces with four different colors.
But, how difficult is it to find all cycles?
This one has 6 Red-Green cycles (all of even length), that form a division on the 3-regular planar graph into cycles.

I realized that for some posts I may have used “Kempe loops” and “Kempe cycles” to describe closed “Kempe chains”, that in other words form closed paths (cycles). I think it would have been better always to use “Kempe cycles”.
https://en.wikipedia.org/wiki/Loop_(graph_theory)

https://en.wikipedia.org/wiki/Path_(graph_theory)

https://en.wikipedia.org/wiki/Hamiltonian_path

Considering the smallest known non-Hamiltonian 3-regular planar graphs, discovered by Barnette-Bosák-Lederberg, I computed the Tait coloring and then deformed it to put in evidence the R-G cycles that in this case are four.
Links to the historical importance of this graph:
https://mathworld.wolfram.com/Barnette-Bosak-LederbergGraph.html
https://en.wikipedia.org/wiki/Barnette–Bosák–Lederberg graph

And here is the Tait coloring of this graph:

Deformed here to better show the R-G cycles:

Some questions about the previous post:
Q1) Can cycles be concentric?
Yes, see this example.

Q2) Verify if at least one of the cycles (R-G, R-B, or G-B) form an Hamiltonian circuit
False.
From the Tait’s conjecture we now know (now = 1946 by William Thomas Tutte) that 3-regular graphs exist also without an Hamiltonian circuit. It means that, no matter what, it is not possible to find a cycle that touches all vertices, and therefore no single Kempe cycles of any two color selection, can exist.

From Wikipedia, the free encyclopedia
This article is about graph theory. For the conjectures in knot theory, see Tait conjectures.
In mathematics, Tait’s conjecture states that “Every 3-connected planar cubic graph has a Hamiltonian cycle (along the edges) through all its vertices“. It was proposed by P. G. Tait (1884) and disproved by W. T. Tutte (1946), who constructed a counterexample with 25 faces, 69 edges and 46 vertices. Several smaller counterexamples, with 21 faces, 57 edges and 38 vertices, were later proved minimal by Holton & McKay (1988). The condition that the graph be 3-regular is necessary due to polyhedra such as the rhombic dodecahedron, which forms a bipartite graph with six degree-four vertices on one side and eight degree-three vertices on the other side; because any Hamiltonian cycle would have to alternate between the two sides of the bipartition, but they have unequal numbers of vertices, the rhombic dodecahedron is not Hamiltonian. The conjecture was significant, because if true, it would have implied the four color theorem: as Tait described, the four-color problem is equivalent to the problem of finding 3-edge-colorings of bridgeless cubic planar graphs. In a Hamiltonian cubic planar graph, such an edge coloring is easy to find: use two colors alternately on the cycle, and a third color for all remaining edges. Alternatively, a 4-coloring of the faces of a Hamiltonian cubic planar graph may be constructed directly, using two colors for the faces inside the cycle and two more colors for the faces outside.
Smallest known non-Hamiltonian 3-regular planar graph: https://mathworld.wolfram.com/Barnette-Bosak-LederbergGraph.html.

Next post will be on the four coloring of the barnette-bosák-lederberg graph, which is the smallest known non-Hamiltonian graph, and the analysis of its Kempe cycles.
Q3) What about if I start with finding cycles, of even length (# of edges), that cross all vertices?
Some initial considerations: If cycles have to fit with Kempe cycles (closed paths of two alternating colors), they have to be of even length, and that would also mean that the total number of vertices crossed by all the cycles of the same two colors should be even too. Is it like this, or am I missing something? What about graphs with an odd number of vertices? Am I missing something?
Answer to the initial consideration: https://math.stackexchange.com/questions/181833/proving-that-the-number-of-vertices-of-odd-degree-in-any-graph-g-is-even + https://math.stackexchange.com/questions/181833/proving-that-the-number-of-vertices-of-odd-degree-in-any-graph-g-is-even
Finding cycles seems to be as difficult as finding a solution for of 4 coloring problem 😦
The other day, before going to sleep, I realized that I needed to revisit the problem, starting with a piece of evidence I had noticed long ago. When a map is colored, the corresponding Tait coloring of the borders creates color chains (R-G, R-B, or G-B) that always form loops. Moreover, there may be more than one loop for each pair of colors. For example, the map shown here has:
1 R-G loop
2 R-B loops
2 G-B loops

I wonder if analyzing how these loops form during the rebuilding phase of a map, after the reduction phase (see other posts), can lead me out of the mud.
Notes:
Deforming the original map, I managed to put in evidence the R-G loop, and then the other loops (R-B and G-B) respect to the first R-G deformation.



And here with the loops filled


Additional note:
This was the map when I discovered that infinite random switches throughout the entire graph do not solve the impasse. It was bad 😦 The graph here is identical to the one in the previous post.
https://four-color-theorem.org/2016/10/31/four-color-theorem-infinite-switches-are-not-enough/