Computing binary combinatorial gray codes via exhaustive search with SAT solvers

Abstract

The term binary combinatorial Gray code refers to a list of binary words such that the Hamming distance between two neighboring words is one and the list satisfies some additional properties that are of interest to a particular application, e.g., circuit testing, data compression, and computational biology. We apply a propositional encoding to the construction of several examples of combinatorial codes including coil-in-the-box codes, circuit codes, distance preserving codes, and necklaces. The codes are generated from satisfying assignments of the corresponding propositional formulae. The satisfying assignments are obtained using satisfiability (SAT) solvers, which are computational tools for the analysis of propositional formulae. New distance preserving and circuit codes are presented along with a complete list of equivalence classes of the coil-in-the-box codes for codeword length 6 with respect to symmetry transformations of hypercubes. A Gray ordered code composed of all necklaces of the length 9 is presented, improving the known result with length 7.