LIPIcs.CP.2021.4.pdf
- Filesize: 0.62 MB
- 9 pages
Document
Filtering Isomorphic Models by Invariants (Short Paper)
Authors
João Araújo 
,
Choiwah Chow ,
Mikoláš Janota
-
Part of:
Volume:
27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Principles and Practice of Constraint Programming (CP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-10-15
File
Document Identifiers
Author Details
Cite AsGet BibTex
João Araújo, Choiwah Chow, and Mikoláš Janota. Filtering Isomorphic Models by Invariants (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.4
https://doi.org/10.4230/LIPIcs.CP.2021.4
Abstract
The enumeration of finite models of first order logic formulas is an indispensable tool in computational algebra. The task is hindered by the existence of isomorphic models, which are of no use to mathematicians and therefore are typically filtered out a posteriori. This paper proposes a divide-and-conquer approach to speed up and parallelize this process. We design a series of invariant properties that enable us to partition existing models into mutually non-isomorphic blocks, which are then tackled separately. The presented approach is integrated into the popular tool Mace4, where it shows tremendous speed-ups for a variety of algebraic structures.
Subject Classification
ACM Subject Classification
- Computing methodologies
- Theory of computation → Constraint and logic programming
Keywords
- finite model enumeration
- isomorphism
- invariants
- Mace4
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- João Araújo, David Matos, and João Ramires. Axiomatic library finder. URL: https://axiomaticlibraryfinder.pythonanywhere.com/definitions [cited 15.05.2021].
-
Gilles Audemard and Laurent Henocque. The extended least number heuristic. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, pages 427-442, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg.
- 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.
-
Stanley Burris and Hanamantagouda P. Sankappanavar. A course in universal algebra, volume 78 of Graduate texts in mathematics. Springer, 1981.
-
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.
- A. Distler and J. Mitchell. Smallsemi, a library of small semigroups in GAP, Version 0.6.12, 2019. GAP package. URL: https://gap-packages.github.io/smallsemi/.
-
John D. Dixon and Brian Mortimer. Permutation Groups. Springer, 1996.
- The GAP Group. GAP - Groups, Algorithms, and Programming, Version 4.11.1, 2021. URL: https://www.gap-system.org.
- 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.
- Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the BooleanPythagorean 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.
-
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.
-
David Marker. Model Theory: An Introduction. Springer, 2002.
- William McCune. Mace4 reference manual and guide. Technical Report Technical Memorandum No. 264, Argonne National Laboratory, Argonne, IL, August 2003. URL: https://www.cs.unm.edu/~mccune/prover9/mace4.pdf.
- Brendan D McKay. Isomorph-free exhaustive generation. Journal of Algorithms, 26(2):306-324, 1998. URL: https://doi.org/10.1006/jagm.1997.0898.
- 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.
- Gábor Nagy and Petr Vojtěchovský. LOOPS, computing with quasigroups and loops in GAP, Version 3.4.1, November 2018. Refereed GAP package. URL: https://gap-packages.github.io/loops/.
- Neil J. A. Sloane and The OEIS Foundation Inc. The on-line encyclopedia of integer sequences, 2020. URL: http://oeis.org/?language=english.
- Jian Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17:1-22, August 1996. URL: https://doi.org/10.1007/BF00247667.
- 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.