2026-07-24T11:55:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15295 2024-03-12T12:00:16Z ddc:004 open_access

Filtering Isomorphic Models by Invariants (Short Paper) Araújo, João Chow, Choiwah Janota, Mikoláš finite model enumeration isomorphism invariants Mace4 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik João Araújo and Choiwah Chow and Mikoláš Janota 2021 Is Part Of LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2021.4 urn:nbn:de:0030-drops-152956 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.4 eng https://creativecommons.org/licenses/by/4.0/legalcode