Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Finding Lean Induced Cycles in Binary Hypercubes

  • Conference paper

Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 5584))

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 calllean, 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 howclause 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Article MATH  Google Scholar 

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

    Google Scholar 

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

    MathSciNet MATH  Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

  7. Edwards, R.: Symbolic dynamics and computation in model gene networks. Chaos 11(1), 160–169 (2001)

    Article  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

  11. Knuth, D.E.: The Art of Computer Programming. fascicle 2: Generating All Tuples and Permutations, vol. 4. Addison-Wesley Professional, Reading (2005)

    MATH  Google Scholar 

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

    Chapter  Google Scholar 

  13. Liu, X., Schrack, G.F.: A heuristic approach for constructing symmetric Gray codes. Appl. Math. Comput. 155(1), 55–63 (2004)

    MathSciNet MATH  Google Scholar 

  14. Livingston, M., Stout, Q.: Perfect dominating sets. Congressus Numerantium 79, 187–203 (1990)

    MathSciNet MATH  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

  17. Savage, C.: A survey of combinatorial Gray codes. SIAM Review 39(4), 605–629 (1997)

    Article MathSciNet MATH  Google Scholar 

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

    Chapter  Google Scholar 

  19. Singleton, R.C.: Generalized snake-in-the-box codes. IEEE Transactions on Electronic Computers EC-15(4), 596–602 (1966)

    Article  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Article MathSciNet MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Systems Institute, ETH Zurich, Switzerland

    Yury Chebiryak, Thomas Wahl & Daniel Kroening

  2. Computing Laboratory, Oxford University, United Kingdom

    Thomas Wahl, Daniel Kroening & Leopold Haller

Authors
  1. Yury Chebiryak

    You can also search for this author inPubMed Google Scholar

  2. Thomas Wahl

    You can also search for this author inPubMed Google Scholar

  3. Daniel Kroening

    You can also search for this author inPubMed Google Scholar

  4. Leopold Haller

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, Swansea University, Faraday Building, Singleton Park, SA2 8PP, Swansea, UK

    Oliver Kullmann

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

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp