Algorithms Transcending the SAT-Symmetry Interface

Authors Markus Anders, Pascal Schweitzer, Mate Soos



PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.1.pdf
  • Filesize: 0.81 MB
  • 21 pages

Document Identifiers

Author Details

Markus Anders
  • TU Darmstadt, Germany
Pascal Schweitzer
  • TU Darmstadt, Germany
Mate Soos
  • National University of Singapore, Singapore

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.1

Abstract

Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation. In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms. Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
Keywords
  • boolean satisfiability
  • symmetry exploitation
  • computational group theory

Metrics

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

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, pages 836-839. ACM, 2003. URL: https://doi.org/10.1145/775832.776042.
  2. Fadi A. Aloul, Arathi Ramani, Igor L. Markov, and Karem A. Sakallah. Solving difficult SAT instances in the presence of symmetry. In Proceedings of the 39th Design Automation Conference, DAC, pages 731-736. ACM, 2002. URL: https://doi.org/10.1145/513918.514102.
  3. Markus Anders and Pascal Schweitzer. Parallel computation of combinatorial symmetries. In Petra Mutzel, Rasmus Pagh, and Grzegorz Herman, editors, 29th Annual European Symposium on Algorithms, ESA, 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.
  4. Markus Anders and Pascal Schweitzer. Search problems in trees with symmetries: Near optimal traversal strategies for individualization-refinement algorithms. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP, 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.
  5. Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms transcending the sat-symmetry interface. CoRR, abs/2306.00613, 2023. URL: https://doi.org/10.48550/arXiv.2306.00613.
  6. Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a preprocessor for symmetry detection. CoRR, abs/2302.06351, 2023. URL: https://doi.org/10.48550/arXiv.2302.06351.
  7. Paul Beame, Richard M. Karp, Toniann Pitassi, and Michael E. Saks. The efficiency of resolution and davis-putnam procedures. SIAM J. Comput., 31(4):1048-1075, 2002. URL: https://doi.org/10.1137/S0097539700369156.
  8. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified symmetry and dominance breaking for combinatorial optimisation. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI, pages 3698-3707. AAAI Press, 2022. URL: https://ojs.aaai.org/index.php/AAAI/article/view/20283.
  9. 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.
  10. 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
  11. Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov. Exploiting structure in symmetry detection for CNF. In Sharad Malik, Limor Fix, and Andrew B. Kahng, editors, 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.
  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, volume 10491 of LNCS, pages 83-100. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_6.
  13. 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, volume 9710 of LNCS, pages 104-122. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_8.
  14. 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, volume 2470 of LNCS, pages 462-476. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_31.
  15. The GAP Group. GAP - Groups, Algorithms, and Programming, Version 4.12.2, 2022. URL: https://www.gap-system.org.
  16. Solomon W. Golomb and Peter Gaal. On the number of permutations on n objects with greatest cycle length k. Advances in Applied Mathematics, 20(1):98-107, 1998. URL: https://doi.org/10.1006/aama.1997.0567.
  17. Andrew Grayland, Christopher 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
  18. Tommi A. Junttila and Petteri Kaski. Conflict propagation and component recursion for canonical labeling. In Alberto Marchetti-Spaccamela and Michael Segal, editors, Theory and Practice of Algorithms in (Computer) Systems - First International ICST Conference, TAPAS, volume 6595 of LNCS, pages 151-162. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19754-3_16.
  19. Sandra Kiefer, Ilia Ponomarenko, and Pascal Schweitzer. The weisfeiler-leman dimension of planar graphs is at most 3. J. ACM, 66(6):44:1-44:31, 2019. URL: https://doi.org/10.1145/3333003.
  20. Sandra Kiefer, Pascal Schweitzer, and Erkal Selman. Graphs identified by logics with counting. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS, Part I, volume 9234 of LNCS, pages 319-330. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_25.
  21. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation. In Laurent D. Michel, editor, 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.
  22. Brendan D. McKay. Practical graph isomorphism. In 10th. Manitoba Conference on Numerical Mathematics and Computing (Winnipeg, 1980), pages 45-87, 1981. Google Scholar
  23. 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.
  24. M. Neunhöffer, Á. Seress, and M. Horn. recog, a package for constructive recognition of permutation and matrix groups, Version 1.4.2. https://gap-packages.github.io/recog, September 2022. GAP package.
  25. 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.
  26. Adolfo Piperno. Isomorphism test for digraphs with weighted edges. In Gianlorenzo D'Angelo, editor, 17th International Symposium on Experimental Algorithms, SEA, volume 103 of LIPIcs, pages 30:1-30:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.SEA.2018.30.
  27. Jean-Francois Puget. Symmetry breaking using stabilizers. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP, volume 2833 of LNCS, pages 585-599. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_40.
  28. 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.
  29. Karem A. Sakallah. Symmetry and satisfiability. In 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, pages 509-570. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200996.
  30. Ákos Seress. Permutation Group Algorithms. Cambridge Tracts in Mathematics. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511546549.
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