Document Open Access Logo

Breaking Symmetries with Involutions

Authors Michael Codish , Mikoláš Janota

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.8.pdf
  • Filesize: 0.93 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.8.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies
  • Theory of computation → Constraint and logic programming
Keywords
  • graph symmetry
  • patterns
  • permutation
  • Ramsey graphs
  • greedy
  • CEGAR

Metrics

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

Abstract

Symmetry breaking for graphs and other combinatorial objects is notoriously hard. On the one hand, complete symmetry breaks are exponential in size. On the other hand, current, state-of-the-art, partial symmetry breaks are often considered too weak to be of practical use. Recently, the concept of graph patterns has been introduced and provides a concise representation for (large) sets of non-canonical graphs, i.e. graphs that are not lex-leaders and can be excluded from search. In particular, four (specific) graph patterns apply to identify about 3/4 of the set of all non-canonical graphs. Taking this approach further, we discover that graph patterns that derive from permutations that are involutions play an important role in the construction of symmetry breaks for graphs. We take advantage of this to guide the construction of partial and complete symmetry-breaking constraints based on graph patterns. The resulting constraints are small in size and strong in the number of symmetries they break.

Cite As Get BibTex

Michael Codish and Mikoláš Janota. Breaking Symmetries with Involutions. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.8

Author Details

Michael Codish
  • Department of Computer Science, Ben-Gurion University of the Negev, Beer-Sheva, Israel
Mikoláš Janota
  • CIIRC, Czech Technical University in Prague, Czech Republic

Funding

The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902 and co-funded by the European Union under the project ROBOPROX (reg. no. CZ.02.01.01/00/22_008/0004590).

Acknowledgements

The authors would like to thank the anonymous reviewers for their valuable comments and constructive feedback, which helped improve the quality and clarity of this paper. This work began at the Dagstuhl-Seminar 23261 SAT Encodings and Beyond.

References

  1. László Babai and Eugene M. Luks. Canonical labeling of graphs. In Proceedings of the fifteenth annual ACM symposium on Theory of computing, pages 171-183. ACM, 1983. URL: https://doi.org/10.1145/800061.808746.
  2. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  3. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and Aravinda Prasad Sistla, editors, Computer Aided Verification, pages 154-169, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/10722167_15.
  4. Michael Codish, Thorsten Ehlers, Graeme Gange, Avraham Itzhakov, and Peter J. Stuckey. Breaking symmetries with lex implications. In John P. Gallagher and Martin Sulzmann, editors, Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings, volume 10818 of Lecture Notes in Computer Science, pages 182-197. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-90686-7_12.
  5. Michael Codish, Graeme Gange, Avraham Itzhakov, and Peter J. Stuckey. Breaking symmetries in graphs: The nauty way. In Michel Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, volume 9892 of Lecture Notes in Computer Science, pages 157-172. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-44953-1_11.
  6. Michael Codish and Mikoláš Janota. Breaking symmetries from a set-covering perspective. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 22nd International Conference, CPAIOR, Melbourne, Australia November 10-13, 2025 Proceedings, Lecture Notes in Computer Science. Springer, 2025. Google Scholar
  7. 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.
  8. Michael Codish, Alice Miller, Patrick Prosser, and Peter James Stuckey. Breaking symmetries in graph representation. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 510-516, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6480.
  9. James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry-breaking predicates for search problems. In Luigia Carlucci Aiello, Jon Doyle, and Stuart C. Shapiro, editors, Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), pages 148-159. Morgan Kaufmann, 1996. Google Scholar
  10. Marek Dančo, Mikoláš Janota, Michael Codish, and João Jorge Araújo. Complete symmetry breaking for finite models. In AAAI 2025, 2025. URL: https://doi.org/10.48550/arXiv.2502.10155.
  11. Alan M. Frisch and Warwick Harvey. Constraints for breaking all row and column symmetries in a three-by-two matrix. In Proceedings of SymCon'03, 2003. Google Scholar
  12. Thibault Gauthier and Chad E. Brown. A formal proof of R(4, 5)=25. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 16:1-16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ITP.2024.16.
  13. Marijn J. H. Heule. Optimal symmetry breaking for graph problems. Mathematics in Computer Science, 2019. Google Scholar
  14. Avraham Itzhakov and Michael Codish. Breaking symmetries in graph search with canonizing sets. Constraints, pages 1-18, 2016. Google Scholar
  15. Avraham Itzhakov and Michael Codish. Breaking symmetries with high dimensional graph invariants and their combination. In André A. Ciré, editor, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 20th International Conference, CPAIOR 2023, Nice, France, May 29 - June 1, 2023, Proceedings, volume 13884 of Lecture Notes in Computer Science, pages 133-149. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-33271-5_10.
  16. George Katsirelos, Nina Narodytska, and Toby Walsh. On the complexity and completeness of static constraints for breaking row and column symmetry. In David Cohen, editor, Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, volume 6308 of Lecture Notes in Computer Science, pages 305-320. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15396-9_26.
  17. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation and enumeration. ACM Trans. Comput. Log., 25(3):1-30, 2024. URL: https://doi.org/10.1145/3670405.
  18. Vladmír Kvasnička and Jiří Pospíchal. Canonical indexing and constructive enumeration of molecular graphs. J. Chem. Inf. Comput. Sci., 30(2):99-105, April 1990. URL: https://doi.org/10.1021/CI00066A001.
  19. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pages 667-673, 2017. URL: https://doi.org/10.24963/ijcai.2017/93.
  20. João Marques-Silva, Mikoláš Janota, and Anton Belov. Minimal sets over monotone predicates in boolean formulae. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV, volume 8044 of Lecture Notes in Computer Science, pages 592-607. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_39.
  21. Alexander Nöhrer, Armin Biere, and Alexander Egyed. Managing SAT inconsistencies with HUMUS. In Ulrich W. Eisenecker, Sven Apel, and Stefania Gnesi, editors, Sixth International Workshop on Variability Modelling of Software-Intensive Systems, Leipzig, Germany, January 25-27, 2012. Proceedings, pages 83-91. ACM, 2012. URL: https://doi.org/10.1145/2110147.2110157.
  22. Stanislaw P. Radziszowski. Small Ramsey numbers. Electronic Journal of Combinatorics, 1994. Revision #14: January, 2014. URL: http://www.combinatorics.org/.
  23. Jussi Rintanen and Masood Feyzbakhsh Rankooh. Symmetry-breaking constraints for directed graphs. In Ulle Endriss, Francisco S. Melo, Kerstin Bach, Alberto José Bugarín Diz, Jose Maria Alonso-Moral, Senén Barro, and Fredrik Heintz, editors, ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain - Including 13th Conference on Prestigious Applications of Intelligent Systems (PAIS 2024), volume 392 of Frontiers in Artificial Intelligence and Applications, pages 4248-4253. IOS Press, 2024. URL: https://doi.org/10.3233/FAIA240998.
  24. Ilya Shlyakhter. Generating effective symmetry-breaking predicates for search problems. Discrete Applied Mathematics, 155(12):1539-1548, 2007. URL: https://doi.org/10.1016/J.DAM.2005.10.018.
  25. Mate Soos and Kuldeep S. Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, pages 1592-1599. AAAI Press, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011592.
  26. Toby Walsh. General symmetry breaking constraints. In Principles and Practice of Constraint Programming - CP 2006, 12th International Conference, CP 2006, Nantes, France, September 25-29, 2006, Proceedings, pages 650-664, 2006. URL: https://doi.org/10.1007/11889205_46.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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