Cube-based Isomorph-free Finite Model Finding
Choiwah Chow, Mikoláš Janota, João Araújo
TL;DR
The paper tackles the challenge of enumerating finite models of first-order logic modulo isomorphism, which yields enormous search spaces. It introduces CBIF, a cube-based isomorph-free finite model finder that leverages nauty-based graph isomorphism, a compact graph-to-canonical-encoding pipeline, and a hash-based cube/model rejection scheme to avoid duplications. CBIF delivers orders-of-magnitude speedups over traditional two-step methods and enables new enumerations, including extensions of OEIS sequences, across complex algebras such as near-rings, C-loops, and IP loops. The approach reduces memory pressure by using compact representations and is compatible with existing symmetry-breaking and CP-based methods, broadening practical capabilities for computational algebra.
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.