Updated 2012-05-24 23:35:27 by RLE

Arjen Markus (2 february 2004) The history of mathematics is filled with problems that seem easy but turn out to be devilishly complicated. One of these is the so-called four colours problem:

  • If you have a geographical map, how many colours do you need to colour each country in such a way that no two neighbouring countries have the same colour?

The answer is: 4.

But, if I remember correctly, it was the first theorem that was "proven" by the aid of a computer. Because the proof requires a lot of special cases. Lars H: That is indeed the case. See below for some more info about this.

Well, the theorem can be translated into a theorem about planar graphs - graphs that can be drawn without any edge crossing another one. And, it being game for mathematicians, it can be generalised to any kind of graph.

The script below takes a graph and determines whether it can be coloured with N colours in the above sense. The graph is given (that is a convenient format) as a list of pairs:

  • The name of the vertex
  • The names of the vertices that are connected to it

For instance the graph:
   A ----> B ----> C
   |       ^
   v       |
   D ------+

is represented by: {A {B D} B {C} D {B} C {}}

This graph can be coloured using three colours:
   A -> green
   B -> red
   C -> green
   D -> blue

   green ----> red ----> green
   |           ^
   v           |
   blue -------+

but not with two.
 # colour_graph.tcl --
 #    Determine whether a graph can be coloured with N colours
 #

 # DetermineColour --
 #    Determine the colour for the next node
 #
 # Arguments:
 #    coloured_nodes    The nodes that have sofar been coloured
 #    number            Number of available colours
 #    graph             Description of the graph
 #    rest_nodes        Nodes that still need to be coloured
 # Result:
 #    1 if we succeeded, 0 if not
 # Note:
 #    The procedure is recursive - the first node can always be
 #    coloured with colour 0.
 #
 proc DetermineColour { coloured_nodes number graph rest_nodes } {

    #
    # Do we have anything left?
    #
    if { [llength $rest_nodes] == 0 } {
       return 1
    }

    #
    # Take the next node and give it a colour
    #
    set next       [lindex $rest_nodes 0]
    set rest_nodes [lrange $rest_nodes 1 end]

    for { set i 0 } { $i < $number } { incr i } {
       set new_colours [concat $coloured_nodes $next $i]
       if { [ColourFits $new_colours $graph] } {
          if { [DetermineColour $new_colours $number $graph $rest_nodes] } {
             return 1
          }
       }
    }

    #
    # No success ...
    #
    return 0
 }

 # ColourFits --
 #    Check that the new colour fits (no two neighbours
 #    with the same colour)
 #
 # Arguments:
 #    colours           The nodes with their colours
 #    graph             Description of the graph
 # Result:
 #    1 if okay, 0 if not
 #
 proc ColourFits { colours graph } {

    #
    # We only need to look at the last colour!
    # All previous colours (if any have already been checked)
    #
    set new_node   [lindex $colours end-1]
    set new_colour [lindex $colours end]

    foreach { node connections } $graph {
       if { $node == $new_node } {
          foreach c $connections {
             set idx [lsearch $colours $c]
             if { $idx >= 0 } {
                set col [lindex $colours [incr idx]]
                if { $col == $new_colour } {
                   return 0 ;# The colour already exists
                }
             }
          }
       } else {
          if { [lsearch $connections $new_node] >= 0 } {
             set idx [lsearch $colours $node]
             if { $idx == -1 } {
                return 1 ;# No colour yet for the node
             } else {
                set col [lindex $colours [incr idx]]
                if { $col == $new_colour } {
                   return 0 ;# The colour already exists
                }
             }
          }
       }
    }

    #
    # We found a new acceptable colour
    #
    puts "Colours: $colours"
    return 1
 }

 # sufficientNumber --
 #    Determine if the number of colours is sufficient
 #
 # Arguments:
 #    number            Number of available colours
 #    graph             Description of the graph
 # Result:
 #    1 if we succeeded, 0 if not
 #
 proc sufficientNumber { number graph } {

    set rest_nodes     {}
    foreach {node connections} $graph {
       lappend rest_nodes $node
    }
    set coloured_nodes [concat [lindex $rest_nodes 0] "0"]
    set rest_nodes     [lrange $rest_nodes 1 end]

    puts "Rest: $rest_nodes"
    DetermineColour $coloured_nodes $number $graph $rest_nodes
 }

 # main --
 #    Main code (too lazy to write a general procedure)
 #
 # Note:
 #    The names of the nodes should not be numbers,
 #    otherwise the check must be made more complex.
 #
 set graph {A {B D} B {C} D {B} C {}}

 puts "Graph: $graph"
 puts "Number of colours = 1: [sufficientNumber 1 $graph]"
 puts "Number of colours = 2: [sufficientNumber 2 $graph]"
 puts "Number of colours = 3: [sufficientNumber 3 $graph]"
 puts "Number of colours = 4: [sufficientNumber 4 $graph]"

 set graph {A {B D C} B {C} D {B} C {}}

 puts "Graph: $graph"
 puts "Number of colours = 1: [sufficientNumber 1 $graph]"
 puts "Number of colours = 2: [sufficientNumber 2 $graph]"
 puts "Number of colours = 3: [sufficientNumber 3 $graph]"
 puts "Number of colours = 4: [sufficientNumber 4 $graph]"
 set graph {A {B D C} B {C} D {B} C {E F} E {A B} F {D}}

 puts "Graph: $graph"
 puts "Number of colours = 1: [sufficientNumber 1 $graph]"
 puts "Number of colours = 2: [sufficientNumber 2 $graph]"
 puts "Number of colours = 3: [sufficientNumber 3 $graph]"
 puts "Number of colours = 4: [sufficientNumber 4 $graph]"

Lars H: The Four Colour Theorem (or 4CT as specialists like to call it) is indeed famous for (amongst many other things) that it was the first mathematical theorem whose proof extensively relied on computer calculations. There have been much arguing that the proof therefore cannot count as a real proof, but perhaps more from philosophers than from proper graph theorists. Quoting the original Mathematical Reviews review of the papers (Kenneth Appel and Wolfgang Haken: Every planar map is four colorable I&II, Illonois Journal of Mathematics 21 (1977), pp. 429-567 + supplements on microfisches):
In part I the authors describe a discharging procedure which was developed with the aid of a computer program. If correct, this procedure implies that every 5-connected planar triangulation must contain as a proper subgraph at least one member of a set U of over 1800 configurations. In part II, this unavoidable set is listed and the claim made that every configuration has been tested by a second computer program and found to be reducible. Thus, every 5-connected planar triangulation contains a reducible configuration and so cannot be minimally 5-chromatic, from which the title follows. // Reducibility of configurations can be determined by a well-defined process and many of their results have been confirmed by computer programs developed by other researchers. [...] In contrast, discharging is a less well-defined process. Their procedure is described by some 500 diagrams and is peculiar to their approach. The proof that it discharges every U-avoiding 5-connected planar triangulation involves several enumerations of subcases. The weakest part of the proof lies in these enumerations performed by the authors' first computer program. In the supplement of some 460 pages, they reconstruct this case analysis.

In other words, the proof was rather large. However, it wasn't as large a proof as the (roughly contemporary) classification of all simple groups, which no philosophers seem to have been concerned about, even though that proof had been far less scrutinized (being spread out over several dozen articles by over twenty different authors, and written in five different languages). But I suppose critisizing computers is more meriting.

As for what can be found on this page, I think this is the first time I have seen a formulation of graph colouring in terms of directed graphs. It makes no difference, though, because one still end up with the same condition that two adjacent vertices must have different colours.

The question answered by e.g.
 sufficientNumber 4 $graph

is normally stated as "Is $graph 4-colourable?". The minimal N such that a graph G is N-colourable is called the chromatic number of G, normally denoted "chi of G". There is a polynomial algorithm for deciding whether a graph is 2-colourable (bipartite), but already the problem of deciding whether a general graph is 3-colourable is NP-complete.

The algorithm used above is a branch-and-cut algorithm that makes a depth first search of the set of all possible ways of assigning to each vertex one colour from the given set, skipping branches of the search tree in which the same colour would be assigned to two neighbouring vertices. It probably won't be very efficient, because when testing k-colourablilty of an n vertex graph it may end up trying around (k-1)^n different colourings before deciding that none of them work. (Bad case: Testing k-colourability of a long path whose end is part of a complete graph with k+1 vertices. At least (k-1)^(n-k-1) ways of colouring the path will be tried.) An alternative approach (whose complexity is independent of the number of colours) would be to compute the chromatic polynomial of the graph.

AM I had no intention to do anything efficient :), just to work out a little idea. How would you go about computing the chromatic polynomial? (My knowledge of graph theory is pretty basic).

AM Okay, I looked it up at Mathworld [1] and it appears that computing the chromatic polynomial is at least an NP-complete problem. Hence the computation is exponential in the number of edges (well, the formulation is more complicated). So, in general, the above algorithm is not so bad :)