CODESAT

CODESAT ZIP

CODESAT is an extension of Minisat 2 SAT solver to find combinatorial Gray codes. The current implementation inludes the following kinds of codes in an n-cube:

  • Gray code
  • induced paths/cycles (aka snake-in-the-box and coil-in-the-box)
  • circuit codes (cyclic or not)
  • dominating paths/cycles/sets
  • set of nodes that are at least S bits apart (aka binary codes A(n,d))
It also allows to find any of these codes with a given weights distribution (see JSAT paper), or find all codes (i.e. perform a classification). The examples of usage are inluded into archive together with cygwin and linux executables. For any questions and suggestions (for example, adding an encoding of your favorite codes) please don't hesitate to contact me:

my email address

P.s. in order to solve a resulting propositional formula with a different SAT solver, replace "SOLVE" with "DUMP_CNF" in a .run script.

4-cube
The 4-cube
HC
A Hamiltonian cycle
coil
An induced cycle (coil)