Document Open Access Logo

Symmetries for Cube-And-Conquer in Finite Model Finding

Authors João Araújo , Choiwah Chow , Mikoláš Janota

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.8.pdf
  • Filesize: 0.76 MB
  • 19 pages

Document Identifiers

Author Details

João Araújo
  • Universidade Nova de Lisboa, Lisbon, Portugal
Choiwah Chow
  • Universidade Aberta, Lisbon, Portugal
Mikoláš Janota
  • Czech Technical University in Prague, Czech Republic

Funding

  • Araújo, João: Fundação para a Ciência e a Tecnologia, through the projects UIDB/00297{-}/2020 (CMA), PTDC/MAT-PUR/31174/2017, UIDB/04621/2020 and UIDP/04621/2020.
  • Janota, Mikoláš: The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902. This article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306.

Cite AsGet BibTex

João Araújo, Choiwah Chow, and Mikoláš Janota. Symmetries for Cube-And-Conquer in Finite Model Finding. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.8

Abstract

The cube-and-conquer paradigm enables massive parallelization of SAT solvers, which has proven to be crucial in solving highly combinatorial problems. In this paper, we apply the paradigm in the context of finite model finding, where we show that isomorphic cubes can be discarded since they lead to isomorphic models. However, we are faced with the complication that a well-known technique, the Least Number Heuristic (LNH), already exists in finite model finders to effectively prune (some) isomorphic models from the search. Therefore, it needs to be shown that isomorphic cubes still can be discarded when the LNH is used. The presented ideas are incorporated into the finite model finder Mace4, where we demonstrate significant improvements in model enumeration.

Subject Classification

ACM Subject Classification
  • Computing methodologies
  • Theory of computation → Constraint and logic programming
Keywords
  • finite model enumeration
  • cube-and-conquer
  • symmetry-breaking
  • parallel algorithm
  • least number heuristic

Metrics

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

Supplementary Materials

References

  1. João Araújo, João Pedro Araújo, Peter J. Cameron, Edmond W. H. Lee, and Jorge Raminhos. A survey on varieties generated by small semigroups and a companion website, 2019. URL: https://arxiv.org/abs/1911.05817.
  2. João Araújo, Choiwah Chow, and Mikoláš Janota. Boosting isomorphic model filtering with invariants. Constraints, 27(3):360-379, July 2022. URL: https://doi.org/10.1007/s10601-022-09336-x.
  3. João Araújo, David Matos, and João Ramires. MarcieDB: a model and theory database. https://marciedb.pythonanywhere.com, 2022.
  4. Gilles Audemard, Belaid Benhamou, and Laurent Henocque. Predicting and detecting symmetries in FOL finite model search. J. Autom. Reason., 36(3):177-212, 2006. URL: https://doi.org/10.1007/s10817-006-9040-3.
  5. Gilles Audemard and Laurent Henocque. The eXtended least number heuristic. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR, volume 2083 of Lecture Notes in Computer Science, pages 427-442, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-45744-5_35.
  6. Belaid Benhamou and Laurent Henocque. A hybrid method for finite model search in equational theories. Fundam. Informaticae, 39(1-2):21-38, 1999. URL: https://doi.org/10.3233/FI-1999-391202.
  7. R.D. Blumofe and C.E. Leiserson. Scheduling multithreaded computations by work stealing. In Proceedings 35th Annual Symposium on Foundations of Computer Science, pages 356-368, 1994. URL: https://doi.org/10.1109/SFCS.1994.365680.
  8. Thierry Boy de la Tour and Prakash Countcham. An isomorph-free SEM-like enumeration of models. Electronic Notes in Theoretical Computer Science, 125(2):91-113, 2005. Proceedings of the 5th International Workshop on Strategies in Automated Deduction (Strategies 2004). URL: https://doi.org/10.1016/j.entcs.2005.01.003.
  9. Stanley Burris and Hanamantagouda P. Sankappanavar. A course in universal algebra, volume 78 of Graduate texts in mathematics. Springer, New York, NY, 1981. Google Scholar
  10. Geoffrey Chu, Christian Schulte, and Peter J. Stuckey. Confidence-based work stealing in parallel constraint programming. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP, volume 5732, pages 226-241. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_20.
  11. Koen Claessen and Niklas Sörensson. New techniques that improve MACE-style finite model finding. In Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003. Google Scholar
  12. Michael Codish, Alice Miller, Patrick Prosser, and Peter James Stuckey. Breaking symmetries in graph representation. In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pages 510-516. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6480.
  13. 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), pages 148-159. Morgan Kaufmann, 1996. Google Scholar
  14. A. Distler and J. Mitchell. Smallsemi, a library of small semigroups in GAP, Version 0.6.12. https://gap-packages.github.io/smallsemi/, 2019. GAP package. Google Scholar
  15. Andreas Distler, Christopher Jefferson, Tom Kelsey, and Lars Kotthoff. The semigroups of order 10. In Michela Milano, editor, Principles and Practice of Constraint Programming - CP, volume 7514, pages 883-899. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_63.
  16. The GAP Group. GAP - Groups, Algorithms, and Programming, Version 4.11.1, 2021. URL: https://www.gap-system.org.
  17. Ian P. Gent, Christopher Jefferson, and Ian Miguel. Minion: A fast scalable constraint solver. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors, ECAI, 17th European Conference on Artificial Intelligence, Including Prestigious Applications of Intelligent Systems (PAIS), Proceedings, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 98-102, Amsterdam, Netherlands, 2006. IOS Press. URL: http://www.booksonline.iospress.nl/Content/View.aspx?piid=1654.
  18. Ian P. Gent, Ian Miguel, Peter Nightingale, Ciaran McCreesh, Patrick Prosser, Neil C. A. Moore, and Chris Unsworth. A review of literature on parallel constraint solving. Theory Pract. Log. Program., 18(5-6):725-758, 2018. URL: https://doi.org/10.1017/S1471068418000340.
  19. Pascal Van Hentenryck, Pierre Flener, Justin Pearson, and Magnus Ågren. Tractable symmetry breaking for CSPs with interchangeable values. In Georg Gottlob and Toby Walsh, editors, IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, pages 277-284. Morgan Kaufmann, 2003. URL: http://ijcai.org/Proceedings/03/Papers/041.pdf.
  20. Marijn Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, Hardware and Software: Verification and Testing - 7th International Haifa Verification Conference, HVC, Revised Selected Papers, volume 7261, pages 50-65. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-34188-5_8.
  21. Marijn J. H. Heule, Oliver Kullmann, and Armin Biere. Cube-and-conquer for satisfiability. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 31-59. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_2.
  22. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In Theory and Applications of Satisfiability Testing (SAT), 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  23. Antti E. J. Hyvärinen, Matteo Marescotti, and Natasha Sharygina. Lookahead in partitioning SMT. In Formal Methods in Computer Aided Design, FMCAD, pages 271-279. IEEE, 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_37.
  24. Xiangxue Jia and Jian Zhang. A powerful technique to eliminate isomorphism in finite model search. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, pages 318-331, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  25. Tommi Junttila, Matti Karppa, Petteri Kaski, and Jukka Kohonen. An adaptive prefix-assignment technique for symmetry reduction. Journal of Symbolic Computation, 99:21-49, 2020. URL: https://doi.org/10.1016/j.jsc.2019.03.002.
  26. Bernard Jurkowiak, Chu Min Li, and Gil Utard. A parallelization scheme based on work stealing for a class of SAT solvers. J. Autom. Reason., 34(1):73-101, 2005. URL: https://doi.org/10.1007/s10817-005-1970-7.
  27. Majid Ali Khan. Efficient enumeration of higher order algebraic structures. IEEE Access, 8:41309-41324, 2020. URL: https://doi.org/10.1109/ACCESS.2020.2976876.
  28. 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.
  29. Lars Kotthoff and Neil C. A. Moore. Distributed solving through model splitting. ArXiv, abs/1008.4328, 2010. Google Scholar
  30. Kenneth Kunen. The structure of conjugacy closed loops. Transactions of the American Mathematical Society, 352(6):2889-2911, 2000. Google Scholar
  31. Arnaud Malapert, Jean-Charles Régin, and Mohamed Rezgui. Embarrassingly parallel search in constraint programming. J. Artif. Intell. Res., 57:421-464, 2016. URL: https://doi.org/10.1613/jair.5247.
  32. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Improving search space splitting for parallel SAT solving. In 22nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/ICTAI.2010.56.
  33. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. An overview of parallel SAT solving. Constraints An Int. J., 17(3):304-347, 2012. URL: https://doi.org/10.1007/s10601-012-9121-3.
  34. W. McCune. Prover9 and mace4. ěrb|http://www.cs.unm.edu/ mccune/prover9/|, 2005-2010. Google Scholar
  35. William McCune. Mace4 reference manual and guide, August 2003. URL: https://www.cs.unm.edu/~mccune/prover9/mace4.pdf.
  36. Gábor Nagy and Petr Vojtěchovský. LOOPS, computing with quasigroups and loops in GAP, Version 3.4.1. https://gap-packages.github.io/loops/, November 2018. Refereed GAP package. Google Scholar
  37. Morten Nielsen. Parallel search in gecode. Technical Report, Gecode, 2006. Google Scholar
  38. Peter Nightingale, Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Patrick Spracklen. Automatically improving constraint models in savile row. Artificial Intelligence, 251:35-61, 2017. URL: https://doi.org/10.1016/j.artint.2017.07.001.
  39. Anthony Palmieri, Jean-Charles Régin, and Pierre Schaus. Parallel strategies selection. CoRR, abs/1604.06484, 2016. URL: https://arxiv.org/abs/1604.06484.
  40. Giles Reger, Martin Riener, and Martin Suda. Symmetry avoidance in MACE-style finite model finding. In Andreas Herzig and Andrei Popescu, editors, Frontiers of Combining Systems FroCoS, volume 11715, pages 3-21, Switzerland AG, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-29007-8_1.
  41. Jean-Charles Régin and Arnaud Malapert. Parallel constraint programming. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 337-379. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_9.
  42. Jean-Charles Régin, Mohamed Rezgui, and Arnaud Malapert. Embarrassingly parallel search. In Christian Schulte, editor, Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, volume 8124 of Lecture Notes in Computer Science, pages 596-610, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-40627-0_45.
  43. Francesca Rossi, Peter van Beek, and Toby Walsh, editors. Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence. Elsevier, 2006. URL: https://www.sciencedirect.com/science/bookseries/15746526/2.
  44. Neil J. A. Sloane and The OEIS Foundation Inc. The on-line encyclopedia of integer sequences, 2020. URL: http://oeis.org/?language=english.
  45. Jon Sneyers, Peter van Weert, Tom Schrijvers, and Leslie de Koninck. As time goes by: Constraint handling rules: A survey of chr research from 1998 to 2007. Theory and Practice of Logic Programming, 10(1):1-47, 2010. URL: https://doi.org/10.1017/S1471068409990123.
  46. Bernardo Subercaseaux and Marijn Heule. Toward optimal radio colorings of hypercubes via SAT-solving. In Ruzica Piskac and Andrei Voronkov, editors, Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 94 of EPiC Series in Computing, pages 386-404. EasyChair, 2023. URL: https://doi.org/10.29007/qrmp.
  47. Toby Walsh. Symmetry breaking constraints: Recent results. In Jörg Hoffmann and Bart Selman, editors, Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, July 22-26, 2012, Toronto, Ontario, Canada. AAAI Press, 2012. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI12/paper/view/4974.
  48. H. Zhang. Combinatorial designs by SAT solvers. Handbook of Satisfiability, pages 533-568, 2009. URL: https://cir.nii.ac.jp/crid/1571980076163512448.
  49. Hantao Zhang and Jian Zhang. MACE4 and SEM: A comparison of finite model generators. In Maria Paola Bonacina and Mark E. Stickel, editors, Automated Reasoning and Mathematics - Essays in Memory of William W. McCune, volume 7788 of Lecture Notes in Computer Science, pages 101-130. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36675-8_5.
  50. Jian Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17:1-22, August 1996. URL: https://doi.org/10.1007/BF00247667.
  51. Jian Zhang and Hantao Zhang. SEM: a system for enumerating models. In IJCAI, pages 298-303, 1995. URL: http://ijcai.org/Proceedings/95-1/Papers/039.pdf.
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