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. Show more
Journal / seriesTechnical Report / ETH Zurich, Department of Computer Science
PublisherETH, Swiss Federal Institute of Technology Zurich, Computer Systems Institute
SubjectBinary sequences; Cyclic codes; Gray codes
Organisational unit02150 - Dep. Informatik / Dep. of Computer Science
NotesTechnical Reports D-Infk. See also http://e-citations.ethbib.ethz.ch/view/pub:22449.
MoreShow all metadata