Document Open Access Logo

Simplify, Order, Break, Repeat

Authors Markus Anders , Cayden Codel , Marijn J. H. Heule

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.4.pdf
  • Filesize: 1.37 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Boolean satisfiability
  • symmetry handling
  • preprocessing
  • Schreier-Sims

Metrics

Abstract

Existing symmetry-breaking techniques for SAT constrain the search space without simplifying the formula. Lex-leader predicates, the most widely used approach, add global ordering constraints to remove symmetric solutions, but often at the cost of substantial formula blowup and large proofs. Moreover, they ignore structural properties of the formula, such as connectedness, that could enable stronger symmetry breaking. In this paper, we present a new algorithm that treats symmetry breaking not merely as a restriction mechanism, but as a simplification mechanism. Notably, it only adds unit and binary symmetry-breaking clauses, which enables strong formula simplifications. This can expose additional symmetries and in turn allows for multiple rounds of symmetry breaking. Crucially, we exploit connectivity in the formula’s graph representation, including the presence of cliques, to guide the order of symmetry breaking. We implemented our algorithm in the satsuma tool and evaluated it on a large set of benchmarks. As a preprocessing step for CaDiCaL, it improves PAR-2 scores by 22% on the SAT competition 2025 and by 12% on the SAT anniversary track. It also substantially outperforms lex-leader and orbitopal fixing while producing compact proofs.

Cite As Get BibTex

Markus Anders, Cayden Codel, and Marijn J. H. Heule. Simplify, Order, Break, Repeat. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.4

Author Details

Markus Anders
  • RPTU Kaiserslautern-Landau, Germany
Cayden Codel
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This work was supported by the National Science Foundation (NSF) under grant DMS-2434625 and by the AFRL and DARPA under Agreement FA8750-24-9-1000.

Acknowledgements

We thank Annika Jäger, Christopher Hojny, and Marc Pfetsch for their insights into related work in optimization. This work substantially benefited from https://www.dagstuhl.de/seminars/seminar-calendar/seminar-details/25231.

Supplementary Materials

References

  1. Fadi A. Aloul, Igor L. Markov, and Karem A. Sakallah. Shatter: efficient symmetry-breaking for boolean satisfiability. In Proceedings of the 40th Design Automation Conference, DAC 2003, Anaheim, CA, USA, June 2-6, 2003, pages 836-839. ACM, 2003. URL: https://doi.org/10.1145/775832.776042.
  2. Markus Anders. SAT preprocessors and symmetry. In 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.
  3. Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, and Yong Kiam Tan. Faster certified symmetry breaking using orders with auxiliary variables, 2025. URL: https://doi.org/10.48550/arXiv.2511.16637.
  4. 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.
  5. Markus Anders, Cayden R. Codel, and Marijn J. H. Heule. Orbitopal fixing in SAT. In Sebastian Junges and Guy Katz, editors, Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I, Lecture Notes in Computer Science, pages 89-109. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22752-2_5.
  6. 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.
  7. Markus Anders and Pascal Schweitzer. Search problems in trees with symmetries: Near optimal traversal strategies for individualization-refinement algorithms. In 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 16:1-16:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.16.
  8. Tomas Balyo, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B. Helsinki Institute for Information Technology, 2022. Google Scholar
  9. Timo Berthold and Marc E Pfetsch. Detecting orbitopal symmetries. In Operations Research Proceedings 2008: Selected Papers of the Annual International Conference of the German Operations Research Society (GOR) University of Augsburg, September 3-5, 2008, pages 433-438. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00142-0_70.
  10. Armin Biere. Two pigeons per hole problem. In Adrian Balint, Anton Belov, Marijn J.H. Heule, and Matti Järvisalo, editors, Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, volume B, page 103, 2013. Google Scholar
  11. 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.
  12. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  13. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res., 77:1539-1589, 2023. URL: https://doi.org/10.1613/JAIR.1.14296.
  14. Shawn T. Brown, Paola Buitrago, Edward Hanna, Sergiu Sanielevici, Robin Scibek, and Nicholas A. Nystrom. Bridges-2: A platform for rapidly-evolving and data intensive research. In Practice and Experience in Advanced Research Computing 2021: Evolution Across All Dimensions, PEARC '21, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437359.3465593.
  15. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, Volume 17, Issue 2, April 2021. URL: https://doi.org/10.23638/LMCS-17(2:12)2021.
  16. Cayden R. Codel, Jeremy Avigad, and Marijn J. H. Heule. Verified substitution redundancy checking. In Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, pages 186-196. IEEE, 2024. URL: https://doi.org/10.34727/2024/ISBN.978-3-85448-065-5_24.
  17. 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
  18. Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker. Improved static symmetry breaking for SAT. In 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. 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 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.
  20. Ian P. Gent, Tom W. Kelsey, Steve Linton, Iain McDonald, Ian Miguel, and Barbara M. Smith. Conditional symmetry breaking. In Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, Lecture Notes in Computer Science, pages 256-270. Springer, 2005. URL: https://doi.org/10.1007/11564751_21.
  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. URL: https://doi.org/10.1016/S1574-6526(06)80014-3.
  22. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-boolean proofs. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3768-3777. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16494.
  23. Marijn J. H. Heule, Anthony Karahalios, and Willem-Jan van Hoeve. From Cliques to Colorings and Back Again. In Christine Solnon, editor, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022), volume 235 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:10, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2022.26.
  24. Annika Jäger and Marc E. Pfetsch. Structure-preserving symmetry presolving for mixed-binary linear problems. In Integer Programming and Combinatorial Optimization, 2026. To appear. Google Scholar
  25. Tim Januschowski and Marc E Pfetsch. Branch-cut-and-propagate for the maximum k-colorable subgraph problem with symmetry. In International Conference on AI and OR Techniques in Constriant Programming for Combinatorial Optimization Problems, pages 99-116. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21311-3_11.
  26. Matti Järvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. In Automated Reasoning, pages 355-370, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  27. Volker Kaibel, Matthias Peinhardt, and Marc E. Pfetsch. Orbitopal fixing. Discrete Optimization, 8(4):595-610, 2011. URL: https://doi.org/10.1016/j.disopt.2011.07.001.
  28. Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. CNFgen: A generator of crafted benchmarks. 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 464-473. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_30.
  29. François Margot. Pruning by isomorphism in branch-and-cut. Mathematical Programming, 94(1):71-90, 2002. URL: https://doi.org/10.1007/S10107-002-0358-2.
  30. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Comput. Sci. Rev., 5(2):119-161, 2011. URL: https://doi.org/10.1016/J.COSREV.2010.09.009.
  31. Adrián Rebola-Pardo. Even shorter proofs without new variables. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.22.
  32. Ákos Seress. Permutation Group Algorithms. Cambridge Tracts in Mathematics. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511546549.
  33. Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule. Reencoding unique literal clauses. In 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, August 12-15, 2025, Glasgow, Scotland, volume 341 of LIPIcs, pages 29:1-29:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.29.
  34. Charles C. Sims. Computational methods in the study of permutation groups. In Computational Problems in Abstract Algebra, pages 169-183. Pergamon, 1970. URL: https://doi.org/10.1016/B978-0-08-012975-4.50020-5.
  35. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. 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 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  36. Jasper van Doornmalen and Christopher Hojny. A unified framework for symmetry handling. Mathematical Programming, Series A, 212:217-271, 2025. URL: https://doi.org/10.1007/s10107-024-02102-2.
  37. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014, volume 8561, pages 422-429. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  38. Patric R.J. Östergård. A fast algorithm for the maximum clique problem. Discrete Applied Mathematics, 120(1):197-207, 2002. Special Issue devoted to the 6th Twente Workshop on Graphs and Combinatorial Optimization. URL: https://doi.org/10.1016/S0166-218X(01)00290-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