Boosting Isomorphic Model Filtering with Invariants

TL;DR

This paper introduces a novel method for efficiently filtering isomorphic models in finite model enumeration by using invariants, significantly speeding up the process in algebraic structure analysis.

Contribution

It proposes a new approach that splits models into non-isomorphic blocks using invariants, enabling parallel processing and faster enumeration in Mace4.

Findings

Significant speed-ups in model enumeration with the new method.

Effective use of handcrafted and random invariants for filtering.

Applicable to a wide range of algebraic structures.

Abstract

The enumeration of finite models is very important to the working discrete mathematician (algebra, graph theory, etc) and hence the search for effective methods to do this task is a critical goal in discrete computational mathematics. However, it is hindered by the possible existence of many isomorphic models, which usually only add noise. Typically, they are filtered out {\em a posteriori}, a step that might take a long time just to discard redundant models. This paper proposes a novel approach to split the generated models into mutually non-isomorphic blocks. To do that we use well-designed hand-crafted invariants as well as randomly generated invariants. The blocks are then tackled separately and possibly in parallel. This approach is integrated into Mace4 (the most popular tool among mathematicians) where it shows tremendous speed-ups for a large variety of algebraic structures.