Computing binary combinatorial gray codes via exhaustive search with SAT solvers
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. Mehr anzeigen
Zeitschrift / SerieTechnical Report / ETH Zurich, Department of Computer Science
VerlagETH, Swiss Federal Institute of Technology Zurich, Computer Systems Institute
ThemaBinary sequences; Cyclic codes; Gray codes
Organisationseinheit02150 - Dep. Informatik / Dep. of Computer Science
AnmerkungenTechnical Reports D-Infk. See also http://e-citations.ethbib.ethz.ch/view/pub:22449.