License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2021.4
URN: urn:nbn:de:0030-drops-152956
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15295/
Go to the corresponding LIPIcs Volume Portal

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

Filtering Isomorphic Models by Invariants (Short Paper)

pdf-format:
LIPIcs-CP-2021-4.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{araujo_et_al:LIPIcs.CP.2021.4,
  author =	{Ara\'{u}jo, Jo\~{a}o and Chow, Choiwah and Janota, Mikol\'{a}\v{s}},
  title =	{{Filtering Isomorphic Models by Invariants}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{4:1--4:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15295},
  URN =		{urn:nbn:de:0030-drops-152956},
  doi =		{10.4230/LIPIcs.CP.2021.4},
  annote =	{Keywords: finite model enumeration, isomorphism, invariants, Mace4}
}

Keywords: finite model enumeration, isomorphism, invariants, Mace4
Collection: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Issue Date: 2021
Date of publication: 15.10.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI