Document Open Access Logo

On Symmetries and Transformations

Authors Daimy Van Caudenberg , Markus Anders , Bart Bogaerts

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.54.pdf
  • Filesize: 1.01 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Permutations and combinations
Keywords
  • Symmetries
  • Theory
  • Modelling & Modelling Languages

Metrics

Abstract

When solving constraint problems, symmetry handling is a crucial optimization. However, it is well-known that several preprocessing methods and encodings change the syntactic symmetries of the problem, and hence make it more difficult to exploit the symmetries that were present in the original problem. As a consequence, when currently using such methods, one should either handle the symmetries on the original specification or live with the fact that efficiency is lost since this structure is no longer visible. In this paper, we take a different approach: we develop a framework in which symmetry information is explicitly part of the specification and can be passed along through different transformations. One subtle, but important point in this respect is that transformations can change the set of variables. We study theoretical properties of transformations that preserve symmetry information, and we analyze existing transformations from the literature in this framework. We experimentally evaluate our framework on translations of pseudo-Boolean constraints into CNF and show that in practice, simply passing on the symmetry information can lead to significant speed-ups in solving time.

Cite As Get BibTex

Daimy Van Caudenberg, Markus Anders, and Bart Bogaerts. On Symmetries and Transformations. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 54:1-54:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.54

Author Details

Daimy Van Caudenberg
  • KU Leuven, Dept. Computer Science, Leuven, Belgium
Markus Anders
  • RPTU Kaiserslautern-Landau, Kaiserslautern, Germany
Bart Bogaerts
  • KU Leuven, Dept. Computer Science, Leuven, Belgium
  • Vrije Universiteit Brussel, Brussels, Belgium

Funding

Funded by the European Union (ERC, CertiFOX, 101122653). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Supplementary Materials

References

  1. Ignasi Abío and Peter J. Stuckey. Conflict directed lazy decomposition. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 70-85. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_8.
  2. Özgür Akgün, Mun See Chang, Ian P. Gent, and Christopher Jefferson. Breaking the symmetries of indistinguishable objects. In Guido Tack, editor, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 22nd International Conference, CPAIOR 2025, Melbourne, VIC, Australia, November 10-13, 2025, Proceedings, Part I, volume 15762 of Lecture Notes in Computer Science, pages 152-168. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-95973-8_10.
  3. Özgür Akgün, Alan M. Frisch, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Peter Nightingale. Conjure: Automatic generation of constraint models from problem specifications. Artif. Intell., 310:103751, 2022. URL: https://doi.org/10.1016/J.ARTINT.2022.103751.
  4. Fadi A. Aloul, Arathi Ramani, Igor L. Markov, and Karem A. Sakallah. ShatterPB: symmetry-breaking for pseudo-Boolean formulas. In Masaharu Imai, editor, Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, Yokohama, Japan, January 27-30, 2004, pages 883-886. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/ASPDAC.2004.179.
  5. Markus Anders. SAT preprocessors and symmetry. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 1:1-1:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.1.
  6. Markus Anders, Sofia Brenner, and Gaurav Rattan. The complexity of symmetry breaking beyond lex-leader. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, Girona, Spain, September 2-6, 2024, volume 307 of LIPIcs, pages 3:1-3:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CP.2024.3.
  7. Markus Anders, Sofia Brenner, and Gaurav Rattan. Satsuma: Structure-based symmetry breaking in SAT. J. Artif. Intell. Res., 85, 2026. URL: https://doi.org/10.1613/JAIR.1.18744.
  8. Markus Anders and Pascal Schweitzer. Parallel computation of combinatorial symmetries. In 29th Annual European Symposium on Algorithms, ESA 2021, September 6-8, 2021, Lisbon, Portugal (Virtual Conference), volume 204 of LIPIcs, pages 6:1-6:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ESA.2021.6.
  9. 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.
  10. Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New encodings of pseudo-Boolean constraints into CNF. 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 181-194. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_19.
  11. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In Marijn Heule, Ashlin Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2024 - Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 of Department of Computer Science Report Series B, pages 8-10. University of Helsinki, 2024. Google Scholar
  12. Hendrik Bierlee and Jip J. Dekker. Pindakaas. URL: https://doi.org/10.5281/zenodo.10851855.
  13. Ignace Bleukx, Hélène Verhaeghe, Bart Bogaerts, and Tias Guns. Exploiting symmetries in MUS computation. In Toby Walsh, Julie Shah, and Zico Kolter, editors, AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA, pages 11122-11130. AAAI Press, 2025. URL: https://doi.org/10.1609/AAAI.V39I11.33209.
  14. Geoffrey Chu and Peter J. Stuckey. Structure based extended resolution for constraint programming. CoRR, abs/1306.4418, 2013. URL: https://arxiv.org/abs/1306.4418.
  15. James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry-breaking predicates for search problems. In Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), Cambridge, Massachusetts, USA, November 5-8, 1996, pages 148-159. Morgan Kaufmann, 1996. Google Scholar
  16. 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), Cambridge, Massachusetts, USA, November 5-8, 1996, pages 148-159. Morgan Kaufmann, 1996. Google Scholar
  17. 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, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_6.
  18. Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker. Improved static symmetry breaking for SAT. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 104-122. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_8.
  19. Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker. On local domain symmetry for model expansion. Theory Pract. Log. Program., 16(5-6):636-652, 2016. URL: https://doi.org/10.1017/S1471068416000508.
  20. Pierre Flener, Alan M. Frisch, Brahim Hnich, Zeynep Kiziltan, Ian Miguel, Justin Pearson, and Toby Walsh. Breaking row and column symmetries in matrix models. In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, volume 2470 of Lecture Notes in Computer Science, pages 462-476. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_31.
  21. Alan M. Frisch, Warwick Harvey, Christopher Jefferson, Bernadette Martínez Hernández, and Ian Miguel. Essence : A constraint language for specifying combinatorial problems. Constraints An Int. J., 13(3):268-306, 2008. URL: https://doi.org/10.1007/s10601-008-9047-y.
  22. Ian P. Gent, Warwick Harvey, and Tom W. Kelsey. Groups and constraints: Symmetry breaking during search. In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, volume 2470 of Lecture Notes in Computer Science, pages 415-430. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_28.
  23. 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. URL: https://doi.org/10.1016/S1574-6526(06)80014-3.
  24. Andrew Grayland, Ian Miguel, and Colva M. Roney-Dougal. Snake lex: An alternative to double lex. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Lisbon, Portugal, September 20-24, 2009, Proceedings, volume 5732 of Lecture Notes in Computer Science, pages 391-399. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_32.
  25. Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective auxiliary variables via structured reencoding. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy, July 4-8, 2023, volume 271 of LIPIcs, pages 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.11.
  26. Christopher Hojny and Cédric Roy. A framework for handling and exploiting symmetry in benders' decomposition, 2025. URL: https://arxiv.org/abs/2511.22251.
  27. Tommi A. Junttila, Matti Karppa, Petteri Kaski, and Jukka Kohonen. An adaptive prefix-assignment technique for symmetry reduction. J. Symb. Comput., 99:21-49, 2020. URL: https://doi.org/10.1016/J.JSC.2019.03.002.
  28. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. J. Symb. Comput., 60:94-112, 2014. URL: https://doi.org/10.1016/J.JSC.2013.09.003.
  29. Christopher Mears, Maria Garcia de la Banda, Bart Demoen, and Mark Wallace. Lightweight dynamic symmetry breaking. Constraints An Int. J., 19(3):195-242, 2014. URL: https://doi.org/10.1007/S10601-013-9154-2.
  30. Marc E. Pfetsch and Thomas Rehn. A computational comparison of symmetry handling methods for mixed integer programs. Math. Program. Comput., 11(1):37-93, 2019. URL: https://doi.org/10.1007/S12532-018-0140-Y.
  31. Olivier Roussel, 2025. URL: https://www.cril.univ-artois.fr/PB25/.
  32. Daimy Van Caudenberg and Bart Bogaerts. Symmetry and dominance breaking for pseudo-Boolean optimization. In Toon Calders, Celine Vens, Jefrey Lijffijt, and Bart Goethals, editors, Artificial Intelligence and Machine Learning - 34th Joint Benelux Conference, BNAIC/Benelearn 2022, Mechelen, Belgium, November 7-9, 2022, Revised Selected Papers, volume 1805 of Communications in Computer and Information Science, pages 149-166. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-39144-6_10.
  33. Neng-Fa Zhou, Håkan Kjellerstrand, and Jonathan Fruhman. Constraint Solving and Planning with Picat. Springer Briefs in Intelligent Systems. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25883-6.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact