Boosting isomorphic model filtering with invariants. (English) Zbl 07594547
Summary: The enumeration of finite models is very important to the working discrete mathematician (algebra, graph theory, etc) and hence the search for effective methods to do this task is a critical goal in discrete computational mathematics. However, it is hindered by the possible existence of many isomorphic models, which usually only add noise. Typically, they are filtered out a posteriori, a step that might take a long time just to discard redundant models. This paper proposes a novel approach to split the generated models into mutually non-isomorphic blocks. To do that we use well-designed hand-crafted invariants as well as randomly generated invariants. The blocks are then tackled separately and possibly in parallel. This approach is integrated into Mace4 (the most popular tool among mathematicians) where it shows tremendous speed-ups for a large variety of algebraic structures.
Keywords:
computational algebra; finite model enumeration; isomorphism; invariant; random generation of invariants; Mace4; hashingReferences:
[1] | Aloise, D.; Deshpande, A.; Hansen, P.; Popat, P., Np-hardness of euclidean sum-of-squares clustering, Machine Learning, 75, 2, 245-248 (2009) · Zbl 1378.68047 · doi:10.1007/s10994-009-5103-0 |
[2] | Araújo, J., Chow, C., & Janota, M. (2021). Filtering isomorphic models by invariants. In L.D. Michel (Ed.) 27th International conference on principles and practice of constraint programming (CP 2021), Leibniz international proceedings in informatics (LIPIcs). doi:10.4230/LIPIcs.CP.2021.4, https://drops.dagstuhl.de/opus/volltexte/2021/15295, (Vol. 210 pp. 4:1-4:9). Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
[3] | Araújo, J., Matos, D., & Ramires, J. Axiomatic library finder (database). https://axiomaticlibraryfinder.pythonanywhere.com. |
[4] | Audemard, G.; Benhamou, B.; Henocque, L., Predicting and detecting symmetries in FOL finite model search, Journal of Automated Reasoning, 36, 3, 177-212 (2006) · Zbl 1107.68092 · doi:10.1007/s10817-006-9040-3 |
[5] | Audemard, G., & Henocque, L. (2001). The eXtended least number heuristic. In R. Goré, A. Leitsch, & T. Nipkow (Eds.) Automated reasoning, first international joint conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, proceedings, lecture notes in computer science. doi:10.1007/3-540-45744-5/_35, (Vol. 2083 pp. 427-442). Berlin: Springer. · Zbl 0988.68605 |
[6] | Baptista, L., & Silva, J.P.M. (2000). Using randomization and learning to solve hard real-world instances of satisfiability. In R. Dechter (Ed.) Principles and practice of constraint programming - CP 2000, 6th international conference, Singapore, September 18-21, 2000, proceedings, lecture notes in computer science. doi:10.1007/3-540-45349-0/_36, (Vol. 1894 pp. 489-494). Berlin: Springer. · Zbl 1044.68736 |
[7] | Benhamou, B.; Henocque, L., A hybrid method for finite model search in equational theories, Fundam Informaticae, 39, 1-2, 21-38 (1999) · Zbl 0951.68172 · doi:10.3233/FI-1999-391202 |
[8] | Boy de la Tour, T.; Countcham, P., An isomorph-free SEM-like enumeration of models, Electronic Notes in Theoretical Computer Science, 125, 2, 91-113 (2005) · Zbl 1272.68351 · doi:10.1016/j.entcs.2005.01.003 |
[9] | Burris, S.; Sankappanavar, HP, A course in universal algebra. Graduate texts in mathematics, Vol. 78 (1981), New York: Springer, New York · Zbl 0478.08001 |
[10] | Claessen, K., & Sörensson, N. (2003). New techniques that improve MACE-style finite model finding. In Proceedings of the CADE-19 workshop: model computation - principles, algorithms, applications. |
[11] | Crawford, J. M., Ginsberg, M. L., Luks, E. M., & Roy, A. (1996). Symmetry-breaking predicates for search problems. In L.C. Aiello, J. Doyle, & S.C. Shapiro (Eds.) Proceedings of the fifth international conference on principles of knowledge representation and reasoning (KR) (pp. 148-159). San Francisco: Morgan Kaufmann. |
[12] | Dixon, JD; Mortimer, B., Permutation groups (1996), New York: Springer, New York · Zbl 0951.20001 · doi:10.1007/978-1-4612-0731-3 |
[13] | Elhamdadi, M., Macquarrie, J., & Restrepo, R. (2012). Automorphism groups of quandles. J. Algebra Appl 11(1). doi:10.1142/S0219498812500089. · Zbl 1248.20070 |
[14] | The GAP Group: GAP - Groups, Algorithms, and Programming, Version 4.11.1 (2021). https://www.gap-system.org. |
[15] | Gent, I.P., Jefferson, C., & Miguel, I. (2006). Minion: a fast scalable constraint solver. In G. Brewka, S. Coradeschi, A. Perini, & P. Traverso (Eds.) ECAI 2006, 17th European conference on artificial intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, including prestigious applications of intelligent systems (PAIS 2006), proceedings, frontiers in artificial intelligence and applications. http://www.booksonline.iospress.nl/Content/View.aspx?piid=1654, (Vol. 141 pp. 98-102). Amsterdam: IOS Press. |
[16] | Gomes, C.P., Selman, B., & Kautz, H.A. (1998). Boosting combinatorial search through randomization. In J. Mostow C. Rich (Eds.) Proceedings of the fifteenth national conference on artificial intelligence and tenth innovative applications of artificial intelligence conference, AAAI 98, IAAI 98, July 26-30, 1998, Madison, Wisconsin, USA. http://www.aaai.org/Library/AAAI/1998/aaai98-061.php (pp. 431-437). Menlo Park: AAAI Press / The MIT Press. |
[17] | Janota, M., & Suda, M. (2018). Towards smarter MACE-style model finders. In G. Barthe, G. Sutcliffe, & M. Veanes (Eds.) LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, EPiC series in computing. doi:10.29007/w42s, (Vol. 57 pp. 454-470). Manchester: EasyChair. · Zbl 1415.68194 |
[18] | Jia, X., & Zhang, J. (2006). A powerful technique to eliminate isomorphism in finite model search. In U. Furbach N. Shankar (Eds.) Automated reasoning (pp. 318-331). Berlin: Springer. · Zbl 1222.68365 |
[19] | Lynce, I., Baptista, L., & Marques-Silva, J. (2002). Complete unrestricted backtracking algorithms for satisfiability. In Proceedings of the international symposium on theory and applications of satisfiability testing (pp. 214-221). |
[20] | Malandro, ME, Enumeration of finite inverse semigroups, Semigroup Forum, 99, 679-723 (2019) · Zbl 1467.20080 · doi:10.1007/s00233-019-10054-9 |
[21] | Marker, D., Model theory: an introduction (2002), New York: Springer, New York · Zbl 1003.03034 |
[22] | McCune, W. (2003). Mace4 reference manual and guide (Technical Memorandum No. 264), 20. https://www.cs.unm.edu/mccune/prover9/mace4.pdf. |
[23] | McKay, BD, Isomorph-free exhaustive generation, Journal of Algorithms, 26, 2, 306-324 (1998) · Zbl 0894.68107 · doi:10.1006/jagm.1997.0898 |
[24] | Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th design automation conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001. doi:10.1145/378239.379017 (pp. 530-535). New York: ACM. |
[25] | Nagy, G., & Vojtěchovský, P. (2018). LOOPS, computing with quasigroups and loops in GAP, Version 3.4.1. https://gap-packages.github.io/loops/. Refereed GAP package. · Zbl 1132.20044 |
[26] | Papadimitriou, CH; Steiglitz, K., Combinatorial optimization: algorithms and complexity (1982), Upper Saddle: Prentice-Hall, Upper Saddle · Zbl 0503.90060 |
[27] | Reger, G., Riener, M., & Suda, M. (2019). Symmetry avoidance in MACE-style finite model finding. In A. Herzig A. Popescu (Eds.) Frontiers of combining systems - 12th international symposium, FroCoS 2019, London, UK, September 4-6, 2019, proceedings, lecture notes in computer science. doi:10.1007/978-3-030-29007-8/_1, (Vol. 11715 pp. 3-21). Switzerland: Springer. · Zbl 1435.68305 |
[28] | Sloane, N.J.A., & Inc., T.O.F. (2020). The on-line encyclopedia of integer sequences. http://oeis.org/?language=english. |
[29] | Zhang, J., Constructing finite algebras with FALCON, Journal of Automated Reasoning, 17, 1-22 (1996) · Zbl 0877.68103 · doi:10.1007/BF00244457 |
[30] | Zhang, J., & Zhang, H. (1995). SEM: a system for enumerating models. In IJCAI. http://ijcai.org/Proceedings/95-1/Papers/039.pdf (pp. 298-303). |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.