An Efficient SAT Encoding of Circuit Codes

AUTHOR(S)

Yury Chebiryak, and Daniel Kroening

PUBLISHER

IEEE International Symposium on Information Theory and its Applications, Auckland, New Zealand, 2008.

LINKS

preprint PDF download
DOI: 10.1109/ISITA.2008.4895595
- updated lower bounds on length of circuit codes.

Bibtex

@INPROCEEDINGS{ck-isita08,
AUTHOR = {Chebiryak, Y. and Kroening, D.},
TITLE = {An Efficient {SAT} Encoding of Circuit Codes},
BOOKTITLE = {IEEE International Symposium on Information Theory and its Applications},
DOI = {10.1109/ISITA.2008.4895595},
YEAR = {2008},
PAGES = {1-4},
}

ABSTRACT

In this paper, we consider the problem of classifying Hamiltonian cycles in a binary hypercube. Previous work proposed a classification of these cycles using the edge representation, and presented it for dimension 4. We classify cycles in further two dimensions using a reduction to propositional SAT. The proposed algorithm starts with an over-approximation of the set of equivalence classes, which is then refined by queries to a SAT-solver to remove spurious cycles. This method performs up to three orders of magnitude faster than an enumeration with symmetry breaking in the 5-cube.

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