Colouring early example of a computer-assisted proof

Colouring a Torus: The performance of graph colouring algorithmsIntroductionWhen conveying the development of map colouring it is difficult to remain distance from the history that bore it. Its importance once only resided in the minds of curious patrons who laid the foundations of this subject with much grander implications. It is through this great lineage of ideas graph colouring algorithms took form. This field holds countless applications: in scheduling algorithms used by aircraft and post offices, in the allocation/assignment algorithms of CPU registers and mobile radio frequencies, and to the less practical but no less noteworthy problem of solving a Sudoku puzzle.The earliest known reference to the mathematical concept of map colouring was that of Frances Guthrie’s who in 1852 took notice of the fact that only four colours were required to colour the counties of England: an observation of which would bring about the Four Colour Theorem.As this problem became better known, many so-called proofs arose. These proofs (although false) did succeed in conceptualizing abstract ideas which proved instrumental in solving the problem as well as holding larger implications to the field of graph theory itself. These include the introduction of Kempe Chains and Three Edge Colouring.1Further development occurred with a partial solution found by George Birkhoff who proved the theorem up to 25 faces, and Heinrich Heesch’s introduction of reducibility and discharging. The theorem was eventually solved by Kenneth Appel and Wolfgang Haken in 1976. They used a computer to exhaustively prove the theorem for a set of irreducible configurations: an early example of a computer-assisted proof that was controversial at the time.BackgroundMap colouring is the assignment of colours to regions of a map such that regions sharing a boundary are not coloured the same colour3.Graphs and Graph ColouringIt is possible in the subject of map colouring to transform the problem entirely into the graph colouring problem. This is performed by representing every colourable region on the map as the vertex and connecting these vertices with an edge if their corresponding regions share a border (fig 1.1). This of vertices connected by edges is what is known as a graph. More formally, a graph, G = (V, E), is the ordered pair of the vertex-set, V(G) and the edge-set, E(G)..Fig 1.1 Map of counties of Australia shown as a graph 2This corresponding graph has a few notable properties. It is an undirected graph because any for any region, A, that borders with B, B must also border with A.  And since the regions of the map cannot border themselves, the graph is also loopless.The graph colouring problem is defined as follows: For a graph G with vertex-set, V, edge-set, E and a set of colours (otherwise known as the vertex labelling), C = {1, 2, …, k}  find the function f : V ? {1, 2, . . . , q} such that for all vertex u,v ? V,  if uv ? E then f(u) ? f(v).The chromatic number, ?(G) is the minimum number of colours required to colour a graph i.e. the size of the colour set in the optimal colouring. The degree of a vertex is the number of edges incident with edges incident with it. For an individual vertex, v, this is denoted deg(v), but when describing an entire graph, the minimum degree of a vertex is given by ?(G) and the maximum, ?(G).For a  graph, G, a subgraph, Hs is a graph containing only vertices and edges of G where all vertices and edges are in G i.e.  E(Hs) ? E(G) and V(Hs) ? V(G).An induced subgraph, Hi is a subgraph in which the edges between remaining vertices are all preserved.And a minor is a graph, Hm, obtained by contracting the edges of G. Contraction of an edge is performed by removing the edge and merging the two vertices incident with it.A complete graph, Kn, is a graph of n vertices in which every vertex is connected to every other vertex by an edge. A complete bipartite graph, Km,n, is a graph which may be partitioned into two independent sets such that all vertices of the one set share an edge with every vertex of the other.A planar graph is a graph in which there exists some drawing with no intersecting edges called a plane drawing1.  If we observe the number of vertices, n, the number of edges, m, and the number of faces, f, of a graph the planarity of the graph can be determined with Euler’s Formula:? = n – m + fFor all planar graphs the Euler Characteristic,  ? = 2.The Four Colour Theorem states that for all planar graphs can be coloured with at most four colours 4. So, ? = 4. This can be generalized to graphs of ? ? 2 by the Heawood Conjecture:Wagner’s theorem states that a graph is planar if and only if it does not contain the complete graph, K5 or the complete bipartite graph. K3,3 as a minor. This is the equivalent result, of the better know Kuratowski’s Theorem. These graphs are referred to as Forbidden graphs and can be generalized to different families of graphs, especially totally disconnected, forests and outerplanar graphs5.Graph Colouring AlgorithmsTo doOther AlgorithmsThe flood fill algorithm which is used in paint programs: an algorithm that recursively calls a function to colour uncoloured adjacent pixels before colouring itself.RequirementsThe objective of this project is colour in a range of maps intended for representation on the surface of a sphere and torus with numerous graph colouring algorithms (and variations),  then gauge their performance in order to make a comparison of them. This information may then be used to design a well performing graph colouring algorithm well suited to the problem at hand. The program that is to be developed will need to take in some representation of the surface of sphere or torus and display a three-dimensional representation of the as well as some information indicative of the algorithms performance.Map RequirementsBefore any development can me made it is important to state my intended requirements of the maps that are to be processed. These requirements adhere to the mathematical form of the Four Colour Theorem problem and are principally does not intend application for cartographical purposes6.Requirement 1: Maps must be represented on a rectangular two-dimensional planeRequirement 2: Each region must be connected. Although cartographical maps may account for non-contiguous conditions this is inconsistent with the mathematical objectives. An example of an invalidation is a map of North America in which Alaska and Hawaii are separate from the contiguous United States (the 48 remaining states).Requirement 3: All boundaries must be connected. Any breakage in the boundary between two intended regions will combine them into one.Requirement 4: Two or more regions which meet at exactly one point i.e. a corner, must be regarded as non-adjacent and may be coloured the same. The mutual borders of any adjacent regions must therefore not be infinitesimal. Requirement 5: The map must  also satisfy the periodic boundary conditions of the surface in which it is to be embedded: the points at the opposite borders of the map must correspond with the same points.Fig 3.2 Example of diagram satisfying periodic boundary condition with y1 = y2 hence L1=L2 For example consider a line, L1 intersecting the left-most boundary of a map and a line, L2 that intersects the right-most boundary. If the y-coordinate of these intersections are y1,y2 respectively, then the lines L1 and L2 are the same boundary if and only if y1 = y2. In the case of a sphere, all points at the upper and lower boundaries correspond to the same point i.e. poles.   Graph representationThere must be some data representation of the graph of the map and some functionality converting the map into such a representation. This graph must be undirected, loopless and harmonious with the graph colouring algorithms of which it will be input. Graph colouring algorithmsThe project will require a variety of graph colouring algorithms that are representative of those mentioned in academic research. These will be capable of interpreting a graph and determining a valid colouration. These be either complete, finding the optimal colouring in all cases by exhaustively checking every configuration, or approximate, finding some valid colouration that is not optimal in all cases.Performance measureSince the object of this venture is to assess the performance of different algorithms it is clear that we require some metric for measure the time usage and operations of the aforementioned algorithms. Optimal?Visual DisplayAs mentioned before, we require a graphical representation to visualize the surface. This is not the subject of this report and will only briefly be mentioned in the remainder.SpecificationsThis project is written in Java.Map specificationFor any map provided the user will be expected to fulfill Map Requirements (1-5).In coherence with map requirement 1, the will be a 2-dimensional image that will me cylindrically mapped onto the surfaceFig 3.1. The projection of a 2-dimensional map to the surface of a sphereFig 3.2. The projection of a 2-dimensional map to the surface of a torus Pixels of a continuous line must must form a connected chain. If any whitespace is to divide this chains then requirement 3 is not satisfied. The pixels at opposites of an unbounded map must align to form a consistent chain of pixels as to satisfy the periodic boundary condition of requirement 4.   Apart from the previous requirements of an map, there are implementation-level specifications that arise when representing an image computationally. A valid image will conform to the restrictions of a bitmap and it will now be practical to think of maps in terms of pixels.The expected file format of the image will be PNG, and the ImageIO of the program will configured as such. JPEG,GIF, BMP and WBMP are also possible but not recommended. The map will be expected to be black and white. Colourable regions will be coloured white in the input images on all else will be viewed as a border. The thickness of the map must adhere do the maximum border width condition that will later be discussed.Region Reference BuilderThe region builder is responsible for building what shall be called a Region Reference Map. This is an array with a integers for each pixel. The integer, i , uniquely identifies for each pixel, the region in which it is contained (i ? 0) or otherwise identifies it as a border (i < 1).The manner in which the regions are detected is by the flood fill algorithm (bounded flood fill) and two variants: Spherical Flood Fill and Toradol Flood Fill. For bounded flood fill, adjacent pixels are only detected up to the boundaries of the map, however for the variants adjacent pixels are identified past the boundary of the map to the opposite side due to its periodicity. For spherical flood fill this only occurs for the vertical bounds (sides) but for toruses this happens for the the horizontal (top and bottom) bounds also.Graph modelThe graph model uses Google Guava's graph library: a Java library which provides graph-structured data 7. This library lacks the visualization of other libraries such as JGraph 8, but this is unimportant since this layer is hidden and only the map is visible.In identifying the regions we have gathered the vertices of the corresponding graph and now all that is necessary is to find the edges. This is done by way of border detection.Border detection consists of two very similar subprocedures: vertical and horizontal detection. Each procedure read values of the Region Reference Map in their corresponding direction and wherever a border is processed the identifier of the pre-region and post-region is compared. If their identifiers differ an edge should exist between them in the graph, so if no such edge pre-exists in the graph, an edge is added.Graph Colouring AlgorithmsThe graph colouring objects VisualizationThe 3d images produced of the sphere/torus are rendered using JMonkeyEngine. DesignReferences 1 Brun, Y., 2002. The four color theorem. MIT Undergraduate Journal of Mathematics, 21–28. 2 Ted Grajeda | Striped Candy LLC. (n.d.). Royalty Free Vector Maps. Retrieved December 6, 2017, from https://freevectormaps.com/3 Wilson, R. J. (2014). Four colors suffice: how the map problem was solved. Princeton, NJ: Princeton University Press 1-15.4 Robertson, N., Sanders, D., Seymour, P., & Thomas, R. (1997). The Four-Colour Theorem. Journal of Combinatorial Theory, Series B, 70(1), 2-44. doi:10.1006/jctb.1997.17505 Chartrand, G., Geller, D., & Hedetniemi, S. (1971). Graphs with forbidden subgraphs. Journal of Combinatorial Theory, Series B, 10(1), 12-41.6 Wilson, R. J. (2014). Four colors suffice: how the map problem was solved. Princeton, NJ: Princeton University Press 2-3.7 Decker, C. (n.d.). Google/guava. Retrieved December 11, 2017, from https://github.com/google/guava/wiki/GraphsExplained8 Alder, G. (n.d.). Retrieved December 11, 2017, from http://jgraph.sourceforge.net/doc/paper/index.html