Document Open Access Logo

SAT Preprocessors and Symmetry

Author Markus Anders

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.1.pdf
  • Filesize: 0.7 MB
  • 20 pages

Document Identifiers

Author Details

Markus Anders
  • TU Darmstadt, Germany

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}).

Acknowledgements

I want to thank Moritz Lichter, Pascal Schweitzer, Constantin Seebach and Damien Zufferey for the valuable discussions at different stages of the project. I also want to thank the anonymous reviewers at SAT 2022 for pointing out an error with the counter-examples used in an earlier version of the paper.

Cite As Get BibTex

Markus Anders. SAT Preprocessors and Symmetry. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SAT.2022.1

Abstract

Exploitation of symmetries is an indispensable approach to solve certain classes of difficult SAT instances. Numerous techniques for the use of symmetry in SAT have evolved over the past few decades. But no matter how symmetries are used precisely, they have to be detected first. We investigate how to detect more symmetry, faster. The initial idea is to reap the benefits of SAT preprocessing for symmetry detection. As it turns out, applying an off-the-shelf preprocessor before handling symmetry runs into problems: the preprocessor can haphazardly remove symmetry from formulas, severely impeding symmetry exploitation. 
Our main contribution is a theoretical framework that captures the relationship of SAT preprocessing techniques and symmetry. Based on this, we create a symmetry-aware preprocessor that can be applied safely before handling symmetry. We then demonstrate that applying the preprocessor does not only substantially decrease symmetry detection and breaking times, but also uncovers hidden symmetry not detectable in the original instances. Overall, we depart the conventional view of treating symmetry detection as a black-box, presenting a new application-specific approach to symmetry detection in SAT.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Graph algorithms analysis
  • Mathematics of computing → Graph algorithms
Keywords
  • boolean satisfiability
  • symmetry exploitation
  • graph isomorphism

Metrics

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

Related Versions

References

  1. EngageS. URL: https://www.mathematik.tu-darmstadt.de/EngageS.
  2. SAT Competition 2021. URL: https://satcompetition.github.io/2021/.
  3. 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.
  4. 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.
  5. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  6. James M. Crawford. A theoretical analysis of reasoning by symmetry in first-order logic (extended abstract). In AAAI Workshop on Tractable Reasoning, pages 17-22, 1992. Google Scholar
  7. 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.
  8. Paul T. Darga, Karem A. Sakallah, and Igor L. Markov. Faster symmetry discovery using sparsity of symmetries. In Limor Fix, editor, Proceedings of the 45th Design Automation Conference, DAC 2008, Anaheim, CA, USA, June 8-13, 2008, pages 149-154. ACM, 2008. URL: https://doi.org/10.1145/1391469.1391509.
  9. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  10. 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.
  11. 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.
  12. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause elimination for SAT and QSAT. J. Artif. Intell. Res., 53:127-168, 2015. URL: https://doi.org/10.1613/jair.4694.
  13. Matti Järvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  14. 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.
  15. Oliver Kullmann. On a generalization of extended resolution. Discret. Appl. Math., 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  16. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. Journal of Symbolic Computation, 60(0):94-112, 2014. URL: https://doi.org/10.1016/j.jsc.2013.09.003.
  17. Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. Cdclsym: Introducing effective symmetry breaking in SAT solving. In Dirk Beyer and Marieke Huisman, editors, 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.
  18. Muhammad Osama, Anton Wijs, and Armin Biere. SAT solving with GPU accelerated inprocessing. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 133-151. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_8.
  19. Adolfo Piperno. Search space contraction in canonical labeling of graphs (preliminary version). CoRR, abs/0804.4881, 2008. arXiv. URL: http://arxiv.org/abs/0804.4881.
  20. Karem A. Sakallah. Symmetry and satisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 289-338. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-289.
  21. 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.
  22. Rodrigue Konan Tchinda and Clémentin Tayou Djamégni. Enhancing static symmetry breaking with dynamic symmetry handling in CDCL SAT solvers. Int. J. Artif. Intell. Tools, 28(3):1950011:1-1950011:32, 2019. URL: https://doi.org/10.1142/S0218213019500118.
  23. Tevich Treethanyaphong and Athasit Surarerks. Dynamic symmetry breaking in SAT using augmented clauses with a polynomial-time lexicographic pruning. In 2nd European Conference on Electrical Engineering and Computer Science, EECS 2018, Bern, Switzerland, December 20-22, 2018, pages 242-247. IEEE, 2018. URL: https://doi.org/10.1109/EECS.2018.00053.
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 About DROPS Imprint Privacy Contact