Document Open Access Logo

Filtering Isomorphic Models by Invariants (Short Paper)

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

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.4.pdf
  • Filesize: 0.62 MB
  • 9 pages

Document Identifiers

Author Details

João Araújo
  • NOVA University 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 scientific 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 As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. João Araújo, David Matos, and João Ramires. Axiomatic library finder. URL: https://axiomaticlibraryfinder.pythonanywhere.com/definitions [cited 15.05.2021].
  2. 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. Google Scholar
  3. 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.
  4. Stanley Burris and Hanamantagouda P. Sankappanavar. A course in universal algebra, volume 78 of Graduate texts in mathematics. Springer, 1981. Google Scholar
  5. 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
  6. 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/.
  7. John D. Dixon and Brian Mortimer. Permutation Groups. Springer, 1996. Google Scholar
  8. The GAP Group. GAP - Groups, Algorithms, and Programming, Version 4.11.1, 2021. URL: https://www.gap-system.org.
  9. 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.
  10. 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.
  11. 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
  12. David Marker. Model Theory: An Introduction. Springer, 2002. Google Scholar
  13. 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.
  14. Brendan D McKay. Isomorph-free exhaustive generation. Journal of Algorithms, 26(2):306-324, 1998. URL: https://doi.org/10.1006/jagm.1997.0898.
  15. 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.
  16. 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/.
  17. Neil J. A. Sloane and The OEIS Foundation Inc. The on-line encyclopedia of integer sequences, 2020. URL: http://oeis.org/?language=english.
  18. Jian Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17:1-22, August 1996. URL: https://doi.org/10.1007/BF00247667.
  19. 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 About DROPS Imprint Privacy Contact