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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Iyer, S.P., Nylén, A.: SAT-solving the coverability problem for Petri nets. Formal Methods in System Design 24(1), 25–43 (2004)
Chebiryak, Y., Kroening, D.: An efficient SAT encoding of circuit codes. In: Procs. IEEE International Symposium on Information Theory and its Applications, Auckland, New Zealand, December 2008, pp. 1235–1238 (2008)
Chebiryak, Y., Kroening, D.: Towards a classification of Hamiltonian cycles in the 6-cube. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4, 57–74 (2008)
de Jong, H., Page, M.: Search for steady states of piecewise-linear differential equation models of genetic regulatory networks. IEEE/ACM Trans. Comput. Biology Bioinform. 5(2), 208–222 (2008)
Diaz-Gomez, P.A., Hougen, D.F.: Genetic algorithms for hunting snakes in hypercubes: Fitness function analysis and open questions. In: SNPD-SAWN 2006: Proceedings of the Seventh ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, Washington, DC, USA, pp. 389–394. IEEE Computer Society, Los Alamitos (2006)
Dransfield, M.R., Marek, V.W., Truszczynski, M.: Satisfiability and computing van der Waerden numbers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 1–13. Springer, Heidelberg (2004)
Edwards, R.: Symbolic dynamics and computation in model gene networks. Chaos 11(1), 160–169 (2001)
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Glass, L.: Combinatorial aspects of dynamics in biological systems. In: Landman, U. (ed.) Statistical mechanics and statistical methods in theory and applications, pp. 585–611. Plenum Press (1977)
Knuth, D.E.: The Art of Computer Programming. fascicle 2: Generating All Tuples and Permutations, vol. 4. Addison-Wesley Professional, Reading (2005)
Kouril, M., Franco, J.V.: Resolution tunnels for improved SAT solver performance. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 143–157. Springer, Heidelberg (2005)
Liu, X., Schrack, G.F.: A heuristic approach for constructing symmetric Gray codes. Appl. Math. Comput. 155(1), 55–63 (2004)
Livingston, M., Stout, Q.: Perfect dominating sets. Congressus Numerantium 79, 187–203 (1990)
Na’aman Kam, D., Kugler, H., Rami Marelly, A., Hubbard, J., Stern, M.: Formal modelling of C. elegans development. A scenario-based approach. Modelling in Molecular Biology, 151–174 (2004)
Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)
Savage, C.: A survey of combinatorial Gray codes. SIAM Review 39(4), 605–629 (1997)
Schewe, L.: Generation of oriented matroids using satisfiability solvers. In: Iglesias, A., Takayama, N. (eds.) ICMS 2006. LNCS, vol. 4151, pp. 216–218. Springer, Heidelberg (2006)
Singleton, R.C.: Generalized snake-in-the-box codes. IEEE Transactions on Electronic Computers EC-15(4), 596–602 (1966)
Zinovik, I., Chebiryak, Y., Kroening, D.: Cyclic attractors in Glass models for gene regulatory networks. IEEE Trans. Inf. Theory: Special Issue on Molecular Biology and Neuroscience (December 2009) (accepted)
Zinovik, I., Kroening, D., Chebiryak, Y.: An algebraic algorithm for the identification of Glass networks with periodic orbits along cyclic attractors. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) Ab 2007. LNCS, vol. 4545, pp. 140–154. Springer, Heidelberg (2007)
Zinovik, I., Kroening, D., Chebiryak, Y.: Computing binary combinatorial Gray codes via exhaustive search with SAT-solvers. IEEE Transactions on Information Theory 54(4), 1819–1823 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chebiryak, Y., Wahl, T., Kroening, D., Haller, L. (2009). Finding Lean Induced Cycles in Binary Hypercubes. In: Kullmann, O. (eds) Theory and Applications of Satisfiability Testing - SAT 2009. SAT 2009. Lecture Notes in Computer Science, vol 5584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02777-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-02777-2_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02776-5
Online ISBN: 978-3-642-02777-2
eBook Packages: Computer ScienceComputer Science (R0)