Filtering Isomorphic Models by Invariants

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00353759" target="_blank" >RIV/68407700:21730/21:00353759 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.4230/LIPIcs.CP.2021.4" target="_blank" >https://doi.org/10.4230/LIPIcs.CP.2021.4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.CP.2021.4" target="_blank" >10.4230/LIPIcs.CP.2021.4</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Filtering Isomorphic Models by Invariants

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Filtering Isomorphic Models by Invariants

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

ISBN

978-3-95977-211-2

ISSN

—

e-ISSN

1868-8969

Počet stran výsledku

9

Strana od-do

1-9

Název nakladatele

Dagstuhl Publishing,

Místo vydání

Saarbrücken

Místo konání akce

Montpellier

Datum konání akce

25. 10. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—