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`:

```ocaml
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:

```ocaml
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:

```ocaml
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.