Home Education Publications Hypercubes Miscellaneous	Finding Lean Induced Cycles in Binary Hypercubes AUTHOR(S) Yury Chebiryak, Thomas Wahl, Daniel Kroening and Leopold Haller PUBLISHER Procs. SAT Conference, Lecture Notes in Computer Science no. 5584, Springer, June 2009. LINKS PDF download DOI Bibtex @INPROCEEDINGS{cwk2009, AUTHOR = {Chebiryak, Y. and Wahl, T. and Kroening, D. and Haller, L.}, BOOKTITLE = {Theory and Applications of Satisfiability Testing -- SAT 2009}, TITLE = {Finding Lean Induced Cycles in Binary Hypercubes}, PAGES = {18--31}, VOLUME= {5584}, SERIES = {LNCS}, EDITOR = {O. Kullmann}, YEAR = {2009}, PUBLISHER = {Springer}, DOI = {10.1007/978-3-642-02777-2_4} } ABSTRACT Induced (chord-free) cycles in binary hypercubes have many applications in computer science. The state of the art for computing such cycles relies on genetic algorithms, which are, however, unable to perform a complete search. In this paper, we propose an approach to finding a special class of induced cycles we call lean, based on an efficient propositional SAT encoding. Lean induced cycles dominate a minimum number of hypercube nodes. Such cycles have been identified in Systems Biology as candidates for stable trajectories of gene regulatory networks. The encoding enabled us to compute lean induced cycles for hypercubes up to dimension 7. We also classify the induced cycles by the number of nodes they fail to dominate, using a custom-built All-SAT solver. We demonstrate how clause filtering can reduce the number of blocking clauses by two orders of magnitude. A part of this work was presented at the 7th Australia -- New Zealand Mathematics Convention, Christchurch, New Zealand, December 11, 2008. The work was supported by ETH Research Grant TH-19 06-3.

Home Education Publications Hypercubes Miscellaneous

Finding Lean Induced Cycles
in Binary Hypercubes

AUTHOR(S)

Yury Chebiryak, Thomas Wahl, Daniel Kroening and Leopold Haller

PUBLISHER

Procs. SAT Conference, Lecture Notes in Computer Science no. 5584, Springer, June 2009.

LINKS

Bibtex

@INPROCEEDINGS{cwk2009,
AUTHOR = {Chebiryak, Y. and Wahl, T. and Kroening, D. and Haller, L.},
BOOKTITLE = {Theory and Applications of Satisfiability Testing -- SAT 2009},
TITLE = {Finding Lean Induced Cycles in Binary Hypercubes},
PAGES = {18--31},
VOLUME= {5584},
SERIES = {LNCS},
EDITOR = {O. Kullmann},
YEAR = {2009},
PUBLISHER = {Springer},
DOI = {10.1007/978-3-642-02777-2_4}
}

ABSTRACT

Induced (chord-free) cycles in binary hypercubes have many applications in computer science. The state of the art for computing such cycles relies on genetic algorithms, which are, however, unable to perform a complete search. In this paper, we propose an approach to finding a special class of induced cycles we call lean, based on an efficient propositional SAT encoding. Lean induced cycles dominate a minimum number of hypercube nodes. Such cycles have been identified in Systems Biology as candidates for stable trajectories of gene regulatory networks. The encoding enabled us to compute lean induced cycles for hypercubes up to dimension 7. We also classify the induced cycles by the number of nodes they fail to dominate, using a custom-built All-SAT solver. We demonstrate how clause filtering can reduce the number of blocking clauses by two orders of magnitude.
A part of this work was presented at the 7th Australia -- New Zealand Mathematics Convention, Christchurch, New Zealand, December 11, 2008. The work was supported by ETH Research Grant TH-19 06-3.