Computing Binary Combinatorial Gray Codes
via Exhaustive Search with SAT-solvers


Igor Zinovik, Daniel Kroening, and Yury Chebiryak


IEEE Transactions on Information Theory, vol. 54, pp. 1819-1823, April 2008.


PDF download
Digital Object Identifier (DOI): 10.1109/TIT.2008.917695
Some codes reported in this paper are available here.
- an extended version of this paper is available as technical report 580, ETH Zurich
- a table with current bounds of circuit codes is here.


AUTHOR = { Zinovik, Igor
and Kroening, Daniel
and Chebiryak, Yury },
TITLE = { Computing Binary Combinatorial {Gray} Codes via Exhaustive Search with {SAT}-solvers},
JOURNAL = { IEEE Transactions on Information Theory},
VOLUME = {54},
NUMBER = {4},
PAGES = {1819-1823},
ISSN = {0018-9448},
YEAR = {April 2008 },
DOI = {10.1109/TIT.2008.917695},


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. 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.

This work was supported in part by an award from IBM Research and by an ETH Research Grant TH-19 06-3.