Document Open Access Logo

SAT Modulo Symmetries for Graph Generation

Authors Markus Kirchweger, Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.34.pdf
  • Filesize: 0.72 MB
  • 16 pages

Document Identifiers

Author Details

Markus Kirchweger
  • Algorithms and Complexity Group, TU Wien, Austria
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

The authors acknowledge the support from the Austrian Science Fund (FWF), project P32441, and from the Vienna Science and Technology Fund (WWTF), project ICT19-065.

Cite AsGet BibTex

Markus Kirchweger and Stefan Szeider. SAT Modulo Symmetries for Graph Generation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 34:1-34:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.34

Abstract

We propose a novel constraint-based approach to graph generation. Our approach utilizes the interaction between a CDCL SAT solver and a special symmetry propagator where the SAT solver runs on an encoding of the desired graph property. The symmetry propagator checks partially generated graphs for minimality w.r.t. a lexicographic ordering during the solving process. This approach has several advantages over a static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator can perform a complete symmetry breaking without causing a prohibitively large initial encoding. We instantiate our approach by generating extremal graphs with certain restrictions in terms of girth and diameter. With our approach, we could confirm the Simon-Murty Conjecture (1979) on diameter-2-critical graphs for graphs up to 18 vertices.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Extremal graph theory
Keywords
  • symmetry breaking
  • SAT encodings
  • graph generation
  • combinatorial search
  • extremal graphs
  • CDCL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. E. Abajo and A. Diánez. Exact value of ex(n;C₃,…,C_s) for n ≤ ⌊25(s-1)/8⌋. Discrete Math., 185:1-7, 2015. URL: https://doi.org/10.1016/j.dam.2014.11.021.
  2. Vikraman Arvind, Bireswar Das, and Johannes Köbler. A logspace algorithm for partial 2-tree canonization. In Edward A. Hirsch, Alexander A. Razborov, Alexei L. Semenov, and Anatol Slissenko, editors, Computer Science - Theory and Applications, Third International Computer Science Symposium in Russia, CSR 2008, Moscow, Russia, June 7-12, 2008, Proceedings, volume 5010 of Lecture Notes in Computer Science, pages 40-51. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79709-8_8.
  3. Rolf Backofen and Sebastian Will. Excluding symmetries in constraint-based search. Constraints, 7(3-4):333-349, 2002. URL: https://doi.org/10.1023/A:1020533821509.
  4. Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of boolean cardinality constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer Science, pages 108-122. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_8.
  5. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1267-1330. IOS Press, second edition, 2021. Google Scholar
  6. Béla Bollobás. Extremal graph theory. Academic Press, 1978. Google Scholar
  7. Louis Caccetta and Roland Häggkvist. On diameter critical graphs. Discrete Math., 28(3):223-229, 1979. URL: https://doi.org/10.1016/0012-365X(79)90129-8.
  8. Ya-Chen Chen and Zoltán Füredi. Minimum vertex-diameter-2-critical graphs. J. Graph Theory, 50(4):293-315, 2005. URL: https://doi.org/10.1002/jgt.20111.
  9. Geoffrey Chu, Maria Garcia de la Banda, Christopher Mears, and Peter J. Stuckey. Symmetries, almost symmetries, and lazy clause generation. Constraints, 19(4):434-462, 2014. URL: https://doi.org/10.1007/s10601-014-9163-9.
  10. Michael Codish, Alice Miller, Patrick Prosser, and Peter J. Stuckey. Constraints for symmetry breaking in graph representation. Constraints, 24(1):1-24, 2019. URL: https://doi.org/10.1007/s10601-018-9294-5.
  11. Antoine Dailly, Florent Foucaud, and Adriana Hansberg. Strengthening the Murty-Simon conjecture on diameter 2 critical graphs. Discrete Math., 342(11):3142-3159, 2019. URL: https://doi.org/10.1016/j.disc.2019.06.023.
  12. Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. Symmetric explanation learning: Effective dynamic symmetry handling for SAT. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 83-100. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_6.
  13. Jo Devriendt, Bart Bogaerts, Broes De Cat, Marc Denecker, and Christopher Mears. Symmetry propagation: Improved dynamic symmetry breaking in SAT. In IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9, 2012, pages 49-56. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/ICTAI.2012.16.
  14. P. Erdős and A. Rényi. On a problem in the theory of graphs. Magyar Tud. Akad. Mat. Kutató Int. Közl., 7:623-641 (1963), 1962. Google Scholar
  15. Torsten Fahle, Stefan Schamberger, and Meinolf Sellmann. Symmetry breaking. In Toby Walsh, editor, Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, volume 2239 of Lecture Notes in Computer Science, pages 93-107. Springer Verlag, 2001. URL: https://doi.org/10.1007/3-540-45578-7_7.
  16. Genghua Fan. On diameter 2-critical graphs. Discret. Math., 67(3):235-240, 1987. URL: https://doi.org/10.1016/0012-365X(87)90174-9.
  17. David K. Garnick, Y. H. Harris Kwong, and Felix Lazebnik. Extremal graphs without three-cycles or four-cycles. J. Graph Theory, 17(5):633-645, 1993. URL: https://doi.org/10.1002/jgt.3190170511.
  18. Martin Gebser, Tomi Janhunen, and Jussi Rintanen. SAT modulo graphs: Acyclicity. In Eduardo Fermé and João Leite, editors, Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, volume 8761 of Lecture Notes in Computer Science, pages 137-151. Springer Verlag, 2014. URL: https://doi.org/10.1007/978-3-319-11558-0_10.
  19. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, and Philipp Wanko. Theory solving made easy with Clingo 5. In Manuel Carro, Andy King, Neda Saeedloei, and Marina De Vos, editors, Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016 TCs, October 16-21, 2016, New York City, USA, volume 52 of OASICS, pages 2:1-2:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/OASIcs.ICLP.2016.2.
  20. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Clingo = ASP + control: Preliminary report. CoRR, abs/1405.3694, 2014. URL: http://arxiv.org/abs/1405.3694.
  21. Ian P. Gent, Karen E. Petrie, and Jean-François Puget. Symmetry in constraint programming. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence, pages 329-376. Elsevier, 2006. Google Scholar
  22. Teresa Haynes, Michael Henning, Lucas Merwe, and Anders Yeo. A maximum degree theorem for diameter-2-critical graphs. Open Mathematics, 12(12):1882-1889, 2014. URL: https://doi.org/10.2478/s11533-014-0449-3.
  23. Teresa W. Haynes, Michael A. Henning, Lucas C. van der Merwe, and Anders Yeo. Progress on the Murty-Simon Conjecture on diameter-2 critical graphs: a survey. J. Comb. Optim., 30(3):579-595, 2015. URL: https://doi.org/10.1007/s10878-013-9651-7.
  24. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation, 2021. URL: https://doi.org/10.5281/zenodo.5170575.
  25. Mark H. Liffiton and Jordyn C. Maglalang. A cardinality solver: More expressive constraints for free - (poster presentation). In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science, pages 485-486. Springer Verlag, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_47.
  26. Po-Shen Loh and Jie Ma. Diameter critical graphs. J. Combin. Theory Ser. B, 117:34-58, 2016. URL: https://doi.org/10.1016/j.jctb.2015.11.004.
  27. W. Mantel. Problem 28. Wiskundige Opgaven, 10:60-61, 1907. Google Scholar
  28. João Marques-Silva and Sharad Malik. Propositional SAT solving. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 247-275. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_9.
  29. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. J. Symbolic Comput., 60:94-112, 2014. URL: https://doi.org/10.1016/j.jsc.2013.09.003.
  30. Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. CDCLSym: introducing effective symmetry breaking in SAT solving. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, volume 10805 of Lecture Notes in Computer Science, pages 99-114. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_6.
  31. Amit Metodi and Michael Codish. Compiling finite domain constraints to SAT with BEE. Theory Pract. Log. Program., 12(4-5):465-483, 2012. URL: https://doi.org/10.1017/S1471068412000130.
  32. Jean-Francois Puget. Symmetry breaking using stabilizers. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer Science, pages 585-599. Springer Verlag, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_40.
  33. Jovan Radosavljević and Miodrag Živković. The list of diameter-2-critical graphs with at most 10 nodes. IPSI Trans. Adv. Res., 16(1):1-5, 2020. URL: http://ipsitransactions.org/journals/papers/tar/2020jan/p9.pdf.
  34. Bas Schaafsma, Marijn Heule, and Hans van Maaren. Dynamic symmetry breaking by simulating Zykov contraction. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 223-236. Springer Verlag, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_22.
  35. Jianmin Tang, Yuqing Lin, Camino Balbuena, and Mirka Miller. Calculating the extremal number ex(v;C₃,C₄,… ,C_n). Discr. Appl. Math., 157(9):2198-2206, 2009. URL: https://doi.org/10.1016/j.dam.2007.10.029.
  36. P. Wang, G. W. Dueck, and S. MacMillan. Using simulated annealing to construct extremal graphs. Discrete Math., 235(1-3):125-135, 2001. Combinatorics (Prague, 1998). URL: https://doi.org/10.1016/S0012-365X(00)00265-X.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact