A Programming Approach to Planar Coloured Graphs

Abstract

The proof of the four colour theorem is a landmark of computational mathematics, and its machinery, degeneracy, Kempe chains, discharging, reducibility, and unavoidable sets, is a treasury of al- gorithmic ideas. This paper, the third in a series on learning and computing with planar graphs, takes a programming approach: it turns the proof strategies of the four colour theorem into concrete, imple- mentable procedures for colouring planar coloured graphs, and it supplies the proper colourings that the learning algorithms of the companion papers consume. We develop four programs with increasing ambi- tion. A degeneracy program colours any planar graph with at most six colours in linear time by peeling vertices of degree at most five. A Kempe chain program improves this to five colours in linear time by re- colouring along alternating two colour paths, using planarity to rule out the only obstruction. A discharging and reducibility program uses the charge that Euler’s formula distributes over a triangulation as a colour- ing priority and prunes small reducible configurations. A constraint search program performs saturation ordered backtracking with forward checking to reach the chromatic number when a minimum colouring is required, falling back on the always available four colouring guaranteed by the theorem. Each program is given with correctness and complexity, the intuition of every proof idea is made explicit, and the behaviour is illustrated on planar test graphs. The message is that the four colour theorem is not only a theorem to be admired but a design manual to be programmed