Cube-based Isomorph-free Finite Model Finding

TL;DR

This paper introduces CBIF, a novel algorithm for efficiently enumerating finite models of first-order logic formulas without duplicates due to isomorphism, significantly improving speed over traditional methods.

Contribution

The paper presents a new cube-based isomorph-free enumeration algorithm that integrates graph isomorphism detection and compact model representations, outperforming existing approaches.

Findings

CBIF is many orders of magnitude faster than traditional algorithms.

Enabled calculation of new finite model enumeration results.

Extended two OEIS sequences with new data.

Abstract

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 computationally. This paper develops a novel algorithm that achieves isomorphism-free enumeration by employing isomorphic graph detection algorithm 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 second 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 advancing the state of the art.