Creative Commons Attribution 4.0 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: https://drops.dagstuhl.de/opus/volltexte/2021/15295/
Araújo, João ; Chow, Choiwah ; Janota, Mikoláš
Filtering Isomorphic Models by Invariants (Short Paper)
| pdf-format: |
|
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 | |
| Seminar: | 27th International Conference on Principles and Practice of Constraint Programming (CP 2021) | |
| Issue date: | 2021 | |
| Date of publication: | 15.10.2021 |
