Skip to main content
SpringerLink
Log in

Computing Maximum Unavoidable Subgraphs Using SAT Solvers

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2016 (SAT 2016)

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

  • 1934 Accesses

Abstract

Unavoidable subgraphs have been widely studied in the context of Ramsey Theory. The research in this area focuses on highly structured graphs such as cliques, cycles, paths, stars, trees, and wheels. We propose to study maximum unavoidable subgraphs measuring the size in the number of edges. We computed maximum unavoidable subgraphs for graphs up to order nine via SAT solving and observed that these subgraphs are less structured, although all are bipartite. Additionally, we found large unavoidable bipartite subgraphs up to order twelve. We also present the concept of multi-component unavoidable subgraphs and show that large multi-component subgraphs are unavoidable in small graphs. We envision that maximum unavoidable subgraphs can be exploited using an alternative approach to breaking graph symmetries.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Currently, our system is not able to prove this property for \(n > 18\) due to out of computational resources.

  2. 2.

    We found multiple maximum unavoidable subgraphs for \(K_9\). Figure 3 (a) shows one of them.

References

  1. Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI 2003, Acapulco, Mexico, 9–15 August 2003, pp. 271–276. Morgan Kaufmann (2003)

    Google Scholar 

  2. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, pp. 399–404, 11–17 July 2009

    Google Scholar 

  3. Bondy, J.A., Erdős, P.: Ramsey numbers for cycles in graphs. J. Combin. Theory Ser. B 14(1), 46–54 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  4. Burr, S.A., Erdős, P.: Extremal Ramsey theory for graphs. Utilitas Math. 9, 247–258 (1976)

    MathSciNet  MATH  Google Scholar 

  5. Codish, M., Miller, A., Prosser, P., Stuckey, P.J.: Breaking symmetries in graph representation. In: Proceedings of IJCAI 2013, pp. 510–516. IJCAI/AAAI (2013)

    Google Scholar 

  6. Gerencsér, L., Gyárfás, A.: On Ramsey-type problems. Annales Universitatis Scientiarum Budapestinensis 10, 167–170 (1967)

    MathSciNet  MATH  Google Scholar 

  7. Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory. A Wiley-Interscience Publication. Wiley, New York (1990)

    Google Scholar 

  8. Harary, F.: Recent results on generalized ramsey theory for graphs. In: Alavi, Y., Lick, D.R., White, A.T. (eds.) Graph Theory and Applications. Lecture Notes in Mathematics, vol. 303, pp. 125–138. Springer, Heidelberg (1972)

    Chapter  Google Scholar 

  9. Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228–245. Springer, Switzerland (2016)

    Google Scholar 

  10. Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219–226. Springer, Heidelberg (2014)

    Google Scholar 

  11. McKay, B.D., Piperno, A.: Practical graph isomorphism, II. J. Symbol. Comput. 60, 94–112 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  12. McKay, B.D., Radziszowski, S.P.: R(4, 5) = 25. J. Graph Theory 19(3), 309–322 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  13. Radziszowski, S.P.: Small Ramsey numbers. Electron. J. Combin., #DS1 (2014)

    Google Scholar 

  14. Radziszowski, S.P., Jin, X.: Paths, cycles and wheels in graphs without antitriangle. Australas. J. Combin. 9, 221–232 (1994)

    MathSciNet  MATH  Google Scholar 

  15. Thurley, M.: sharpSAT – counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424–429. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Acknowledgements

The authors are supported by the National Science Foundation under grant number CCF-1526760 and acknowledge the Texas Advanced Computing Center (TACC) at The University of Texas at Austin for providing grid resources that have contributed to the research results reported within this paper.

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Texas at Austin, Austin, TX, USA

    C. K. Cuong & M. J. H. Heule

Authors
  1. C. K. Cuong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. J. H. Heule
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to C. K. Cuong .

Editor information

Editors and Affiliations

  1. Aix-Marseille Université, Marseille, France

    Nadia Creignou

  2. Université d'Artois, Lens, France

    Daniel Le Berre

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Cuong, C.K., Heule, M.J.H. (2016). Computing Maximum Unavoidable Subgraphs Using SAT Solvers. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40970-2_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40969-6

  • Online ISBN: 978-3-319-40970-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation