Document Open Access Logo

Engineering a Preprocessor for Symmetry Detection

Authors Markus Anders, Pascal Schweitzer, Julian Stieß

PDF
Thumbnail PDF

File

LIPIcs.SEA.2023.1.pdf
  • Filesize: 1.94 MB
  • 21 pages

Document Identifiers

Author Details

Markus Anders
  • TU Darmstadt, Germany
Pascal Schweitzer
  • TU Darmstadt, Germany
Julian Stieß
  • University of Koblenz-Landau, Germany

Funding

Supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (EngageS: grant No. {820148}).

Acknowledgements

We thank Marc E. Pfetsch and Christopher Hojny for giving us further insights into the user-side of symmetry detection software, as well as providing us with the MIP2017 graphs.

Cite AsGet BibTex

Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a Preprocessor for Symmetry Detection. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SEA.2023.1

Abstract

State-of-the-art solvers for symmetry detection in combinatorial objects are becoming increasingly sophisticated software libraries. Most of the solvers were initially designed with inputs from combinatorics in mind (nauty, bliss, Traces, dejavu). They excel at dealing with a complicated core of the input. Others focus on practical instances that exhibit sparsity. They excel at dealing with comparatively easy but extremely large substructures of the input (saucy). In practice, these differences manifest in significantly diverging performances on different types of graph classes. We engineer a preprocessor for symmetry detection. The result is a tool designed to shrink sparse, large substructures of the input graph. On most of the practical instances, the preprocessor improves the overall running time significantly for many of the state-of-the-art solvers. At the same time, our benchmarks show that the additional overhead is negligible. Overall we obtain single algorithms with competitive performance across all benchmark graphs. As such, the preprocessor bridges the disparity between solvers that focus on combinatorial graphs and large practical graphs. In fact, on most of the practical instances the combined setup significantly outperforms previous state-of-the-art.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Graph algorithms
Keywords
  • graph isomorphism
  • automorphism groups
  • symmetry detection
  • preprocessors

Metrics

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

Supplementary Materials

References

  1. MIPLIB 2017 - The Mixed Integer Programming Library. URL: https://miplib.zib.de/.
  2. nauty and Traces. URL: http://pallini.di.uniroma1.it.
  3. sassy. URL: https://github.com/markusa4/sassy.
  4. SAT Competition 2021. URL: https://satcompetition.github.io/2021/.
  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 and Pascal Schweitzer. Engineering a fast probabilistic isomorphism test. In Martin Farach-Colton and Sabine Storandt, editors, Proceedings of the Symposium on Algorithm Engineering and Experiments, ALENEX 2021, Virtual Conference, January 10-11, 2021, pages 73-84. SIAM, 2021. URL: https://doi.org/10.1137/1.9781611976472.6.
  7. 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 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.
  8. Markus Anders, Pascal Schweitzer, and Florian Wetzels. Comparative design-choice analysis of color refinement algorithms beyond the worst case. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 15:1-15:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.15.
  9. Christoph Berkholz, Paul S. Bonsma, and Martin Grohe. Tight lower and upper bounds for the complexity of canonical colour refinement. Theory Comput. Syst., 60(4):581-614, 2017. URL: https://doi.org/10.1007/s00224-016-9686-0.
  10. Armin Biere, Florian Lonsing, and Martina Seidl. Blocked clause elimination for QBF. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 101-115. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_10.
  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. David Déharbe, Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo. Exploiting symmetry in SMT problems. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 222-236. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_18.
  13. 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.
  14. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 61-75. Springer, 2005. URL: https://doi.org/10.1007/11499107_5.
  15. 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.
  16. Mark K. Goldberg. A nonfactorial algorithm for testing isomorphism of two graphs. Discret. Appl. Math., 6(3):229-236, 1983. URL: https://doi.org/10.1016/0166-218X(83)90078-1.
  17. Christopher Hojny and Marc E. Pfetsch. Symmetry handling via symmetry breaking polytopes. In Ekrem Duman and Ali Fuat Alkaya, editors, 13th Cologne Twente Workshop on Graphs and Combinatorial Optimization, Istanbul, Turkey, May 26-28, 2015, pages 63-66, 2015. Google Scholar
  18. Derek F. Holt, Bettina Eick, and Eamonn A. O'Brien. Handbook of Computational Group Theory. Discrete Mathematics and Its Applications. Chapman and Hall/CRC, 2005. Google Scholar
  19. 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 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.
  20. Hadi Katebi, Karem A. Sakallah, and Igor L. Markov. Symmetry and satisfiability: An update. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 113-127. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_11.
  21. Manuel Kauers and Martina Seidl. Symmetries of quantified boolean formulas. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 199-216. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_13.
  22. 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.
  23. Sandra Kiefer, Pascal Schweitzer, and Erkal Selman. Graphs identified by logics with counting. ACM Trans. Comput. Log., 23(1):1:1-1:31, 2022. URL: https://doi.org/10.1145/3417515.
  24. Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo. Maxpre: An extended maxsat preprocessor. 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 449-456. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_28.
  25. François Margot. Symmetry in integer linear programming. In Michael Jünger, Thomas M. Liebling, Denis Naddef, George L. Nemhauser, William R. Pulleyblank, Gerhard Reinelt, Giovanni Rinaldi, and Laurence A. Wolsey, editors, 50 Years of Integer Programming 1958-2008 - From the Early Years to the State-of-the-Art, pages 647-686. Springer, 2010. URL: https://doi.org/10.1007/978-3-540-68279-0_17.
  26. 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.
  27. 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.
  28. Adolfo Piperno. Isomorphism test for digraphs with weighted edges. In Gianlorenzo D'Angelo, editor, 17th International Symposium on Experimental Algorithms, SEA 2018, June 27-29, 2018, L'Aquila, Italy, 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.
  29. Pascal Schweitzer and Daniel Wiebking. A unifying method for the design of algorithms canonizing combinatorial objects. In Moses Charikar and Edith Cohen, editors, Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 1247-1258. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316338.
  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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact