The Four Colour Map Problem (4CMP) is one of the most well known problems of mathematics, and has posed
a challenge to mathematicians since the early 1850s. Kempe's 1879
proof, although flawed, remained
the foundation for the computer-assisted
proofs since the 1970s. But these
proofs have proven
difficult to verify due to the thousands of special cases considered, the hundreds of pages of manual proof,
the hundreds of
discharge rules, the uncovering of minor errors, and the use of custom assembly code.
The development of a simplified proof with a reduced number of cases, and the verification of a variant of
this using the general-purpose Coq proof assistant, leaves this problem in an unsatisfactory state for
mathematicians who expect a proof to provide insight into the problem, but provides an interesting challenge
problem for Constraint Logic Programming. This WIP talk discusses a CLP(FD) representation of 4CMP with
multiset visualization implemented in a common framework sitting on top of both SWI and SICStus Prolog.
It further discusses the tradeoffs between the two underlying solvers, compares timings for default labelings,
and explores and characterizes an optimized approach to labeling.