An Efficient SAT Encoding of Circuit Codes
IEEE International Symposium on Information Theory and its Applications, Auckland, New Zealand, 2008.
In this paper, we consider the problem of classifying Hamiltonian
cycles in a binary hypercube.
Previous work proposed a classification of these
cycles using the edge representation, and presented it for dimension 4.
We classify cycles in further two dimensions using a reduction to propositional SAT.
The proposed algorithm starts with an over-approximation of the set of
equivalence classes, which is then refined by queries to a SAT-solver to
remove spurious cycles.
This method performs up to three orders of magnitude faster than an enumeration with symmetry breaking in the 5-cube.