Document Open Access Logo

The Complexity of Symmetry Breaking Beyond Lex-Leader

Authors Markus Anders, Sofia Brenner , Gaurav Rattan

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.3.pdf
  • Filesize: 0.87 MB
  • 24 pages

Document Identifiers

Author Details

Markus Anders
  • TU Darmstadt, Germany
Sofia Brenner
  • TU Darmstadt, Germany
Gaurav Rattan
  • University of Twente, Enschede, The Netherlands

Funding

The research leading to these results has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (EngageS: grant agreement No. 820148).
  • Brenner, Sofia: Received funding from the German Research Foundation DFG (SFB-TRR 195 "Symbolic Tools in Mathematics and their Application").

Cite AsGet BibTex

Markus Anders, Sofia Brenner, and Gaurav Rattan. The Complexity of Symmetry Breaking Beyond Lex-Leader. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.3

Abstract

Symmetry breaking is a widely popular approach to enhance solvers in constraint programming, such as those for SAT or MIP. Symmetry breaking predicates (SBPs) typically impose an order on variables and single out the lexicographic leader (lex-leader) in each orbit of assignments. Although it is NP-hard to find complete lex-leader SBPs, incomplete lex-leader SBPs are widely used in practice. In this paper, we investigate the complexity of computing complete SBPs, lex-leader or otherwise, for SAT. Our main result proves a natural barrier for efficiently computing SBPs: efficient certification of graph non-isomorphism. Our results explain the difficulty of obtaining short SBPs for important CP problems, such as matrix-models with row-column symmetries and graph generation problems. Our results hold even when SBPs are allowed to introduce additional variables. We show polynomial upper bounds for breaking certain symmetry groups, namely automorphism groups of trees and wreath products of groups with efficient SBPs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
Keywords
  • symmetry breaking
  • boolean satisfiability
  • matrix models
  • graph isomorphism

Metrics

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

Related Versions

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 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.
  3. Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms transcending the sat-symmetry interface. In 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 1:1-1:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.1.
  4. Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a preprocessor for symmetry detection. In 21st International Symposium on Experimental Algorithms, SEA 2023, July 24-26, 2023, Barcelona, Spain, volume 265 of LIPIcs, pages 1:1-1:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SEA.2023.1.
  5. László Babai. Graph isomorphism in quasipolynomial time [extended abstract]. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge, MA, USA, June 18-21, 2016, pages 684-697. ACM, 2016. URL: https://doi.org/10.1145/2897518.2897542.
  6. László Babai. Canonical form for graphs in quasipolynomial time: preliminary report. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 1237-1246. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316356.
  7. László Babai and Eugene M. Luks. Canonical labeling of graphs. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 25-27 April, 1983, Boston, Massachusetts, USA, pages 171-183. ACM, 1983. URL: https://doi.org/10.1145/800061.808746.
  8. László Babai and Eugene M. Luks. Canonical labeling of graphs. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, STOC '83, pages 171-183, New York, NY, USA, 1983. Association for Computing Machinery. Google Scholar
  9. László Babai, Eugene M. Luks, and Ákos Seress. Permutation groups in NC. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 409-420. ACM, 1987. URL: https://doi.org/10.1145/28395.28439.
  10. László Babai and Shlomo Moran. Arthur-merlin games: A randomized proof system, and a hierarchy of complexity classes. Journal of Computer and System Sciences, 36(2):254-276, 1988. URL: https://doi.org/10.1016/0022-0000(88)90028-1.
  11. 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.
  12. Bart Bogaerts, Jakob Nordström, Andy Oertel, and Çağrı Uluç Yıldırımoğlu. BreakID-kissat in SAT competition 2023 (system description). In Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions, Department of Computer Science Series of Publications B, Finland, 2023. Department of Computer Science, University of Helsinki. Google Scholar
  13. Mun See Chang and Christopher Jefferson. Disjoint direct product decompositions of permutation groups. J. Symb. Comput., 108:1-16, 2022. URL: https://doi.org/10.1016/j.jsc.2021.04.003.
  14. Michael Codish, Graeme Gange, Avraham Itzhakov, and Peter J. Stuckey. Breaking symmetries in graphs: The nauty way. In 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.
  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. Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov. Exploiting structure in symmetry detection for CNF. In Proceedings of the 41th Design Automation Conference, DAC 2004, San Diego, CA, USA, June 7-11, 2004, pages 530-534. ACM, 2004. URL: https://doi.org/10.1145/996566.996712.
  17. Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. Symmetric explanation learning: Effective dynamic symmetry handling for SAT. In 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 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, 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.
  20. John D. Dixon and Brian Mortimer. Permutation Groups. Graduate Texts in Mathematics. Springer New York, 1996. URL: https://books.google.de/books?id=4QDpFN6k61EC.
  21. 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.
  22. Pierre Flener, Alan M. Frisch, Brahim Hnich, Zeynep Kızıltan, Ian Miguel, and Toby Walsh. Matrix modelling. Technical Report APES-36-2001, APES group (2001), 2001. Google Scholar
  23. Pierre Flener, Justin Pearson, and Meinolf Sellmann. Static and dynamic structural symmetry breaking. Ann. Math. Artif. Intell., 57(1):37-57, 2009. URL: https://doi.org/10.1007/S10472-009-9172-3.
  24. Ian P. Gent, Karen E. Petrie, and Jean-François Puget. Symmetry in constraint programming. In 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.
  25. Andrew Grayland, Chris Jefferson, Ian Miguel, and Colva M. Roney-Dougal. Minimal ordering constraints for some families of variable symmetries. Annals of Mathematics and Artificial Intelligence, 57:75-102, 2009. Google Scholar
  26. Marijn J. H. Heule. Optimal symmetry breaking for graph problems. Math. Comput. Sci., 13(4):533-548, 2019. URL: https://doi.org/10.1007/S11786-019-00397-5.
  27. D.F. Holt, B. Eick, and E.A. O'Brien. Handbook of Computational Group Theory. Discrete Mathematics and Its Applications. CRC Press, 2005. URL: https://books.google.de/books?id=i2UjAASZ33YC.
  28. 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.
  29. Tommi A. Junttila and Petteri Kaski. Conflict propagation and component recursion for canonical labeling. In Theory and Practice of Algorithms in (Computer) Systems - First International ICST Conference, TAPAS 2011, Rome, Italy, April 18-20, 2011. Proceedings, volume 6595 of Lecture Notes in Computer Science, pages 151-162. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19754-3_16.
  30. George Katsirelos, Nina Narodytska, and Toby Walsh. On the complexity and completeness of static constraints for breaking row and column symmetry. In 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.
  31. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation. In 27th International Conference on Principles and Practice of Constraint Programming, CP, volume 210 of LIPIcs, pages 34:1-34:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.34.
  32. Johannes Köbler, Uwe Schöning, and Jacobo Torán. The Graph Isomorphism Problem: Its Structural Complexity. Progress in Theoretical Computer Science. Birkhäuser/Springer, 1993. URL: https://doi.org/10.1007/978-1-4612-0333-9.
  33. Eugene M. Luks. Isomorphism of graphs of bounded valence can be tested in polynomial time. Journal of Computer and System Sciences, 25(1):42-65, 1982. URL: https://doi.org/10.1016/0022-0000(82)90009-5.
  34. Eugene M. Luks. Hypergraph isomorphism and structural equivalence of boolean functions. In Jeffrey Scott Vitter, Lawrence L. Larmore, and Frank Thomson Leighton, editors, Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, May 1-4, 1999, Atlanta, Georgia, USA, pages 652-658. ACM, 1999. URL: https://doi.org/10.1145/301250.301427.
  35. Eugene M. Luks and Amitabha Roy. The complexity of symmetry-breaking formulas. Ann. Math. Artif. Intell., 41(1):19-45, 2004. URL: https://doi.org/10.1023/B:AMAI.0000018578.92398.10.
  36. François Margot. Pruning by isomorphism in branch-and-cut. Math. Program., 94(1):71-90, 2002. URL: https://doi.org/10.1007/S10107-002-0358-2.
  37. Brendan D. McKay. Isomorph-free exhaustive generation. J. Algorithms, 26(2):306-324, 1998. URL: https://doi.org/10.1006/JAGM.1997.0898.
  38. 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.
  39. Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. Cdclsym: Introducing effective symmetry breaking in SAT solving. In 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.
  40. James Ostrowski, Jeff T. Linderoth, Fabrizio Rossi, and Stefano Smriglio. Constraint orbital branching. In Integer Programming and Combinatorial Optimization, 13th International Conference, IPCO 2008, Bertinoro, Italy, May 26-28, 2008, Proceedings, volume 5035 of Lecture Notes in Computer Science, pages 225-239. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-68891-4_16.
  41. 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.
  42. G. Pólya. Kombinatorische Anzahlbestimmungen für Gruppen, Graphen und chemische Verbindungen. Acta Mathematica, 68(none):145 - 254, 1937. URL: https://doi.org/10.1007/BF02546665.
  43. Jean-Charles Régin. Generalized arc consistency for global cardinality constraint. In William J. Clancey and Daniel S. Weld, editors, Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, AAAI 96, IAAI 96, Portland, Oregon, USA, August 4-8, 1996, Volume 1, pages 209-215. AAAI Press / The MIT Press, 1996. URL: http://www.aaai.org/Library/AAAI/1996/aaai96-031.php.
  44. Ashish Sabharwal. Symchaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints An Int. J., 14(4):478-505, 2009. URL: https://doi.org/10.1007/S10601-008-9060-1.
  45. Karem A. Sakallah. Symmetry and satisfiability. In Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 509-570. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200996.
  46. Ákos Seress. Permutation Group Algorithms. Cambridge Tracts in Mathematics. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511546549.
  47. Toby Walsh. On the complexity of breaking symmetry. CoRR, abs/2005.08954, 2020. URL: https://arxiv.org/abs/2005.08954.
  48. Viktor N Zemlyachenko, Nickolay M Korneenko, and Regina I Tyshkevich. Graph isomorphism problem. Journal of Soviet Mathematics, 29:1426-1481, 1985. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact