2041-graph-coloring.md

So, essentially, for a NP-complete program, you want to iterate over the entire solution space. To do this, you want to define a bijection between a range of the natural numbers and the solution space. The most elegant way to do this is to define functions on the solutions that mirror the natural numbers (i.e., a homomorphism). The natural numbers can be defined as type nat = Z | S of nat, which gives you an initial (zero) element and a successor function. To define these for the solutions, I would have functions zero_soln and succ_soln which mirror Z and S:

Z : nat
S : nat -> nat
zero_soln : soln
succ_soln : soln -> soln

However, this definition describes an infinite set of solutions homomorphic to the infinite set of natural numbers. This is incorrect, since the solution space is finite in size.

Instead, we'd want to create a structure which has both initial and final elements. On the natural numbers, this could be represented by keeping the initial element, and adding a final element. OCaml's type system can't represent this in a strong way, but it can be implemented by changing the type of S to nat -> nat option, and stating that for any value equal to or above the maximum, S returns None.

By the homomorphism, the types of the functions on soln then are:

zero_soln : soln
succ_soln : soln -> soln option

The actual solutions are of type (int * string) list, while soln also needs to include the set of colors and vertices in order to define succ_soln, so I would define soln as:

type vertex = int;;
type color = string;;

type vertices = vertex list;;
type colors = color list;;

type color_mapping = (vertex * color) list;;

type soln = vertices * colors * graph * color_mapping;;

Since each color_mapping must contain every vertex, one can then treat color_mapping as an m-digit number in base n, where m is the number of vertices and n is the number of colors. The succ_soln function can then be treated as a simple successor. Iterating over the solution space as one iterates over the natural numbers (i.e. with relatively standard recursion or iteration) is then trivial.