Cube-Based Isomorph-Free Finite Model Finding

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Cube-Based Isomorph-Free Finite Model Finding

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2024

Confidentiality

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

Article name in the collection

ECAI 2024 - 27th European Conference on Artificial Intelligence

ISBN

978-1-64368-548-9

ISSN

0922-6389

e-ISSN

1879-8314

Number of pages

8

Pages from-to

4100-4107

Publisher name

IOS Press

Place of publication

Oxford

Event location

Santiago de Compostela

Event date

Oct 19, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—