Cube-Based Isomorph-Free Finite Model Finding

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00380256" target="_blank" >RIV/68407700:21730/24:00380256 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.3233/FAIA240980" target="_blank" >https://doi.org/10.3233/FAIA240980</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.3233/FAIA240980" target="_blank" >10.3233/FAIA240980</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Cube-Based Isomorph-Free Finite Model Finding

Popis výsledku v původním jazyce

Complete enumeration of finite models of first-order logic (FOL) formulas is pivotal to universal algebra, which studies and catalogs algebraic structures. Efficient finite model enumeration is highly challenging because the number of models grows rapidly with their size but at the same time, we are only interested in models modulo isomorphism. While isomorphism cuts down the number of models of interest, it is nontrivial to take that into account computa tionally. This paper develops a novel algorithm that achieves isomorphism free enumeration by employing isomorphic graph detection algo rithm nauty, cube-based search space splitting, and compact model representations. We name our algorithm cube-based isomorph-free finite model finding algorithm (CBIF). Our approach contrasts with the traditional two-step algorithms, which first enumerate (possibly isomorphic) models and then filter the isomorphic ones out in the sec ond stage. The experimental results show that CBIF is many orders of magnitude faster than the traditional two-step algorithms. CBIF enables us to calculate new results that are not found in the literature, including the extension of two existing OEIS sequences, thereby ad vancing the state of the art.

Název v anglickém jazyce

Cube-Based Isomorph-Free Finite Model Finding

Popis výsledku anglicky

Complete enumeration of finite models of first-order logic (FOL) formulas is pivotal to universal algebra, which studies and catalogs algebraic structures. Efficient finite model enumeration is highly challenging because the number of models grows rapidly with their size but at the same time, we are only interested in models modulo isomorphism. While isomorphism cuts down the number of models of interest, it is nontrivial to take that into account computa tionally. This paper develops a novel algorithm that achieves isomorphism free enumeration by employing isomorphic graph detection algo rithm nauty, cube-based search space splitting, and compact model representations. We name our algorithm cube-based isomorph-free finite model finding algorithm (CBIF). Our approach contrasts with the traditional two-step algorithms, which first enumerate (possibly isomorphic) models and then filter the isomorphic ones out in the sec ond stage. The experimental results show that CBIF is many orders of magnitude faster than the traditional two-step algorithms. CBIF enables us to calculate new results that are not found in the literature, including the extension of two existing OEIS sequences, thereby ad vancing the state of the art.

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

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2024

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

ECAI 2024 - 27th European Conference on Artificial Intelligence

ISBN

978-1-64368-548-9

ISSN

0922-6389

e-ISSN

1879-8314

Počet stran výsledku

8

Strana od-do

4100-4107

Název nakladatele

IOS Press

Místo vydání

Oxford

Místo konání akce

Santiago de Compostela

Datum konání akce

19. 10. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

—