General problem:

Find a circular path in the graph containing each node once and only once.

Genetic representation:

Turn it into a SAT problem by canonical transformation.