# Boosting Isomorphic Model Filtering with Invariants

João Araújo
Universidade Nova de Lisboa, Lisbon, Portugal
<EMAIL_ADDRESS>& Choiwah Chow
Universidade Aberta, Lisbon, Portugal
<EMAIL_ADDRESS>& Mikoláš Janota
Czech Technical University in Prague, Czechia
<EMAIL_ADDRESS>Corresponding author

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

_Keywords_ Computational algebra $\cdot$ Finite model enumeration $\cdot$
Isomorphism $\cdot$ Invariant $\cdot$ Random generation of invariants $\cdot$
Mace4 $\cdot$ Hashing

##  1 Introduction

To study and get intuition on different types of relational algebras (groups,
semigroups, and their ordered versions, quasigroups, fields, rings, MV-
algebras, lattices, etc.), mathematicians resort to libraries of all order $n$
models (for small values of $n$) of the algebra they are interested in. These
libraries allow experimentation such as forming and/or testing conjectures
etc., to gain insights into the algebras in question. Indeed, GAP [14], the
most popular computational algebra system, has many libraries of different
algebras (semigroups, quasigroups, etc.), and more are needed. These libraries
are so important that the search for them has a long history in mathematics
predating for many years the use of computers. (See Appendix B of [12]; and
for more recent results please see OEIS [28], where many of the sequences are
the number of order $n$ non-isomorphic models of a given class of algebras.)

Many of these algebras can be defined in first-order logic (FOL) and there are
tools to allow mathematicians to encode their algebras and produce a
meaningful library. The problem is that usually the tools, such as Mace4 [22],
which can be easily learned and used by mathematicians and hence is very
popular among them, generate too many isomorphic models (see Section 2 for the
definition of isomorphism) that need to be eliminated [4]. For example, out of
the 230,984 models for the implication algebras (see definition in [3]) of
order 10 generated by Mace4, only 18 ($\approx 0.0078\%$) of them are pairwise
non-isomorphic.

Redundant models may either be eliminated during the search phase or filtered
out afterwards. Guaranteeing that search never produces isomorphic models is a
hard problem and is rarely seen in modern solvers. This paper, therefore,
tackles the second problem, i.e., the removal of redundant models from an
already enumerated set.

In the context of finite model enumeration, the complexity of checking whether
two models are isomorphic is only part of the problem. Another source of
complexity is the large number of models that need to be checked. If every
model is checked against all others, then the performance degrades rapidly as
the total number of models increases.

If we assign to each generated model a vector that is invariant under
isomorphism and put all models having the same invariant vectors into separate
blocks, then models across the blocks will not be isomorphic. This splits the
problem into substantially smaller sub-problems. Moreover, processing of the
blocks can easily be done in parallel as models across blocks cannot be
isomorphic. Parallel processing is an important facet of our approach since
modern-day computers are more often than not equipped with multiple cores.

Our contributions to the area of isomorphic model elimination are111Some
preliminary ideas and results have been presented in [2]. This paper adds more
invariants including randomly generated invariants and proves their validity.
It also reports substantially more experimental results and drills deeper into
related work.:

  1. 1.

Devise an invariant-based parallel algorithm that can be applied to algebras
defined by first-order logic formulas and containing at least one binary
operation or relation (see Section 5).

  2. 2.

Design a small basic set of invariants that have high discriminating power,
and yet are inexpensive to compute (see Section 3).

  3. 3.

Add randomly generated invariants to the invariant-based algorithm to help
discover invariants of high discriminating power (see Section 4).

  4. 4.

Use a hash-map to store models partitioned by the invariant-based algorithm to
allow fast storage and retrieval of models in the same block (see Section 5).

Our goal is to help mathematicians on two levels: first, provide them with a
tool on their desktop that quickly produces a library for the algebra they are
working on; second, run the tool on a cluster of computers to precompute
libraries for the most famous classes of algebras, and add them to GAP [14] or
a similar system.

##  2 Definitions and Preliminaries

We give a brief overview of the mathematics used in the subsequent sections;
we draw mainly from Chapter 2 of [9].

A relational algebra is a triple $(D,\Sigma_{F},\Sigma_{R})$, where $D$ is a
set and $\Sigma_{F}$ is a set of operations, that is, functions
$f:\,D^{n}\rightarrow D$ and $\Sigma_{R}$ is a set of relations, i.e.,
$R\in\Sigma_{R}$ is a subset of $D^{n}$. The order of a relational algebra is
the size of its domain $D$. (Recall that examples of relational algebras are
all imaginable algebras, (di)graphs, etc.; in the following, by algebra we
mean relational algebra.)

While the concept of isomorphism is ubiquitous to scientific literature, its
definition appears under slight variations. Throughout this paper, we rely on
the following definition. Let $A$ and $B$ be structures defined on the same
signature $\Sigma_{F},\Sigma_{R}$. A function $f$ from $A$ to $B$ is said to
be an _isomorphism_ if it is a bijection and preserves all operations and
relations. This means that if $g\in\Sigma_{F}$, with the respective
interpretations $g^{A}$ and $g^{B}$ in $A$ and $B$, then
$f(g^{A}(a_{1},\dots,a_{n}))=g^{B}(f(a_{1}),\dots,f(a_{n}))$, for all
$a_{1},\dots,a_{n}\in A$. Analogously, $f$ preserves $R\in\Sigma_{R}$ of arity
$n$, with the respective interpretations $R^{A}$ and $R^{B}$ in $A$ and $B$,
if $(a_{1},\ldots,a_{n})\in R^{A}$ implies $(f(a_{1}),\dots,f(a_{n}))\in
R^{B}$, for all $a_{1},\ldots,a_{n}\in A$.

An important property of isomorphisms is that they preserve sets defined by
some fixed formula. More precisely, suppose we have two finite relational
algebras $A$ and $B$, on a signature $\Sigma$, isomorphic under $f:A\to B$. In
addition, suppose we have a set $S$ contained in $A^{k}$ and definable by a
FOL formula $\Phi$ in the language of $\Sigma$. Then $f(S)$ is precisely the
subset of $B^{k}$ that satisfies $\Phi$ (cf. Theorem 1.1.10 in [21]).

For example, suppose we have two isomorphic finite algebras: $(A,*)$ and
$(B,*)$, with $f:A\to B$ an isomorphism. Suppose also that $S$ is the set
$\\{(x,y)\in A\mid(\exists z\in A)\ (x*^{A}z)*^{A}y=x*^{A}(z*^{A}y)\\}$. As
$S$ is the set of all elements in $A^{2}$ that satisfy a FOL in a language
with the function symbol $*$, then $f(S):=\\{(f(x),f(y))\mid(x,y)\in S\\}$ is
precisely the set of all pairs $(x,y)\in B^{2}$ such that $(\exists z\in B)\
(x*^{B}z)*^{B}y=x*^{B}(z*^{B}y)$.

This idea is usually expressed by saying that sets definable by FOL formulas
are invariant (or preserved) under isomorphism. This guarantees that when we
split the list of algebras using invariants based on defining formulas,
algebras in different blocks are non-isomorphic; algebras inside the same
block might be isomorphic or non-isomorphic. Therefore, to discard the
redundant algebras we only have to check within each block. This is the ground
for our invariants-based algorithm. For future reference, we state these
considerations as a proposition.

######  Proposition 1.

Let $A$ and $B$ be algebras of a signature $\Sigma$ and $f:A\to B$ be their
isomorphism. Then any vector $(a_{1},a_{2},\dots,a_{m})\in{A^{m}}$ satisfies a
first-order formula in the common language $\Sigma$ if and only if the vector
$(f(a_{1}),f(a_{2}),\dots,f(a_{m}))\in{B^{m}}$ satisfies the same first-order
formula in $B$.

##  3 Basic Invariants

The goal of this section is to introduce our list of basic invariants.

We start by observing that the axioms satisfied by an algebra might render
some invariants useless. For example, if the algebra is a group, then the
invariant that counts the number of idempotents would be useless (there is
exactly one idempotent in each group). Thus, we need multiple invariants with
inner algebraic meaning and large discriminating power in order to target as
many different algebraic properties/classes as possible. On the other hand, we
should choose properties that are inexpensive to compute and not very many as
that could slow down the computation.

Our choices of invariants are based on concepts ubiquitous in various kinds of
algebras. For example, one of our invariants (B5) is based on the fact that
idempotents appear in many algebras; in particular, it is well-known that
every finite semigroup has at least one idempotent and hence this invariant is
useful for a wide range of algebras, especially those that have a semigroup
reduct.

As observed above, the overwhelming majority of the most popular algebras are
defined using operations of arity at most 2 (see page 26 of [9]), so we design
most of our invariants around binary operations. We have 10 invariants from
binary operations, 4 from binary relations, 4 from unary operations, and 1
from ternary operations to target different common algebraic structures.
Together they have high discriminating powers, and yet are easy and
inexpensive to compute.

In the following discussions on invariants, the domain of the algebra is
denoted by $D=\\{1,2,\cdots,n\\}$.

###  3.1 Invariants from Unary Operations

For each unary operation $g$ in the algebra, we compute the invariants for
each element $x\in{D}$:

  1. U1

1 if $g(x)=x$, 0 otherwise (fixed point);

  2. U2

1 if $g(x)\neq{x}$ and $g(g(x))=x$, 0 otherwise (transposition);

  3. U3

The number of $y\in{D}$ such that $g(y)=x$ (size of the inverse image);

  4. U4

The number of $y\in{D}$ such that $g(g(y))=x$ (size of the inverse image under
$g^{2}$).

The correctness of these invariants follows readily from Proposition 1. Of
course, the correctness of these invariants can also be proved directly
(without using Proposition 1); as a sample illustration, we provide the
details for invariant U3 in the next result.

######  Proposition 2.

Let $f$ be an isomorphism of algebras $A$ and $B$ and $v_{A},v_{B}$ be
invariant vectors calculated according to U3 for $A$ and $B$, respectively.
Then $v_{A}=v_{B}$.

###### Proof.

For $C\in\\{A,B\\}$, $x\in C$, and $g^{C}$ an interpretation of $g$ in $C$,
define $K^{C}_{x}:=\\{y\in C\mid g^{C}(y)=x\\}$. We claim that
$K^{B}_{f(x)}=f(K^{A}_{x})$, i.e. $x$ and $f(x)$ will be represented by the
same number $\lvert{K}^{B}_{f(x)}\rvert=\lvert{f}(K^{A}_{x})\rvert$, in the
(sorted) vectors $v_{A}$ and $v_{B}$, respectively.

If $y\in K^{A}_{x}$, then $g^{A}(y)=x$ so that $f(g^{A}(y))=f(x)$ and hence
$g^{B}(f(y))=f(x)$, that is, $f(K^{A}_{x})\subseteq K^{B}_{f(x)}$. It follows
that

$\lvert{K}^{A}_{x}\rvert=\lvert{f}(K^{A}_{x})\rvert\leq\lvert{K}^{B}_{f(x)}\rvert.$

As $f^{-1}:B\to A$ is an isomorphism too, the foregoing argument shows that

$\lvert{K}^{B}_{u}\rvert=\lvert{f}^{-1}(K^{B}_{u})\rvert\leq\lvert{K}^{A}_{f^{-1}(u)}\rvert.$

Taking in the previous formula $u=f(x)$ we get

$\lvert{K}^{B}_{f(x)}\rvert=\lvert{f}^{-1}(K^{B}_{f(x)})\rvert\leq\lvert{K}^{A}_{f^{-1}(f(x))}\rvert=\lvert{K}^{A}_{x}\rvert.$

Now
$\lvert{K}^{A}_{x}\rvert=\lvert{f}(K^{A}_{x})\rvert\leq\lvert{K}^{B}_{f(x)}\rvert\leq\lvert{K}^{A}_{x}\rvert$
implies
$\lvert{K}^{A}_{x}\rvert=\lvert{f}(K^{A}_{x})\rvert=\lvert{K}^{B}_{f(x)}\rvert$.
As $f(K^{A}_{x})\subseteq K^{B}_{f(x)}$ it follows that
$f(K^{A}_{x})=K^{B}_{f(x)}$ (as we are dealing with finite structures).

∎

Similar arguments can easily be used to directly prove the correctness of the
other invariants.

###  3.2 Invariants from Binary Operations

For each domain element $x\in{D}$, we compute the following invariants for
each binary operation in the algebra:

  1. B1

The smallest integer $n$ such that $x^{n}=x^{k},n>k>=1$ where we define
$x^{n}$ to be $(\ldots(x*x)*x)*x)\ldots$ for $n$ $x$’s (_periodicity_).

  2. B2

The number of $y\in D$ such that $x=(xy)x$ (_number of inverses_).

  3. B3

The number of distinct $xy$ for all $y\in{D}$ (_size of right ideal_).

  4. B4

The number of distinct $yx$ for all $y\in{D}$ (_size of left ideal_).

  5. B5

1 if $xx=x$, 0 otherwise (_idempotency_).

  6. B6

The number of $y\in D$ such that $x(yy)=(yy)x$ (_number of commuting
squares_).

  7. B7

The number of $y\in D$ such that $x=yy$ (_number of square roots_).

  8. B8

The number of $y\in D$ such that $x(xy)=(xx)y$ (_number of square
associatizers_).

  9. B9

The number of pairs of $y,z\in{D}$ such that $zy=yz=x$ (_number of commuting
pairs_).

  10. B10

The number of $y\in{D}$ such that there exist pairs of $s,t\in{D}$ where
$x=st$ and $y=ts$ (_number of conjugates_).

###  3.3 Invariants from Binary Relations

For each domain element $x\in{D}$, the following invariants are calculated for
each binary relation $R$:

  1. R1

The number of distinct $y$ such that $R(x,y)$.

  2. R2

The number of distinct $y$ such that $R(y,x)$.

  3. R3

1 if $R(x,x)$, 0 otherwise. (reflexivity)

  4. R4

The number of $y$ such that $R(x,y)\ \&\ R(y,x)$.

###  3.4 Invariants from Ternary Operations

Ternary operations are very rare. Indeed, no ternary operation exists in the
definition in any of the 158 algebras listed in the ALF database [3], although
a few of them come from the Skolemization of binary operations. Moreover,
calculations involving ternary operations are often very expensive as deeply
nested loops are involved. Thus, only one simple invariant would be included
in the algorithm. For each domain element $x\in{D}$, we compute one invariant
for each ternary operation:

  1. T1

The number of times $x$ appears in the ternary operation table. (frequency)

We call the hand-crafted invariants listed above the _basic invariants_ to
differentiate them from the randomly generated invariants which will be
discussed in Section 4. It should be simple to see that the validity of these
basic invariants follows from Proposition 3.

##  4 Random Invariants

As discussed in Section 3, we need different invariants to target different
algebraic structures. The basic invariants are inspired by our knowledge of
the most popular algebras, however, there are many other (less common)
algebraic structures and new ones are permanently appearing.

Therefore, we need a general way (adaptable to each class of algebras) of
generating invariants with good discriminating power. A practical solution to
this problem is to generate a large set of invariants with a random number of
operations and a random number of variables, and then automatically discover
the best subset to use.

###  4.1 Generation of Random Invariants

A first-order formula can be represented by an expression tree with operations
in the internal nodes and variables in the leaves. For example, Fig. 1 shows
the tree representation of the first-order formula

$x=(x*y)+x^{\prime}$ (1)

It is simple to randomly generate such an expression tree, as shown in
Algorithm 1. For simplicity, the root is set to be an operation that evaluates
to true or false, and it always has two children. It is the only node that can
be assigned the equality relation. It may also be a binary relation if there
is one in the algebra.

$=$$x$$+$$*$$x$$y$′$x$ Figure 1: Expression tree for $x=(x*y)+x^{\prime}$.

input : A list of binary/unary operations/relations, max depth of tree, list
of variables

output : An expression tree representing a first-order formula

1

2

3Function BuildNode (level) begin

/*recursively build a node */

/*maxLevel is maximum depth of tree allowed */

4 if  _level = maxLevel_ then

5 nodeType $\leftarrow$ leaf

6 else

7 nodeType $\leftarrow$ random pick a leaf, unary, or binary operation

8 create newNode

9 if  _nodeType = leaf_ then

10 newNode.value $\leftarrow$ randomly pick a variable

11 return newNode

12 newNode.op $\leftarrow$ randomly pick a unary or binary operation

13 newNode.left $\leftarrow$ buildNode (level +1)

14 if  _newNode.op is a binary operation_ then

15 newNode.right $\leftarrow$ buildNode (level +1)

16

17 return newNode

18

19begin

20 create root node $R$

21 $R.\textnormal{{op}}$ $\leftarrow$ randomly pick the equality operation, or
one of the binary relations (if exists)

22 $R$.left $\leftarrow$ BuildNode (1)

23 $R$.right $\leftarrow$ BuildNode (1)

24 return $R$

25

26

Algorithm 1 Generation of Random First-order Formula

######  Proposition 3.

If we fix a variable in the first-order formula generated by Algorithm 1 as
the base variable, then the number of solutions will be an invariant.

###### Proof.

Correctness is shown as in Proposition 2.∎∎

We may choose any of the variables in the randomly generated first-order
formula as the base variable for the invariant. For example, if we choose $x$
as the base variable for the first-order formula (1), then the invariant would
read: The number of $y\in{D}$ such that $x=(x*y)+x^{\prime}$, which is a valid
invariant by the foregoing argument.

###  4.2 Quality Measure of Random Invariants

After a large set of invariants is generated, a small subset will be selected
based on its ability to reduce the work of the next step in filtering out
isomorphic models. For a block with $m$ models, the worst-case scenario
requires comparing every pair of models for isomorphism. There would be
$m(m-1)/2$ comparisons in total. Based on this observation, we measure the
quality of invariants by a score as follows: For a collection of invariants
that induces a set of blocks of models {$S_{i}\mid 1\leq{i}\leq{n}$}, its
score is computed as

$\sum_{i\in\\{1..n\\}}|S_{j}|(|S_{j}|-1)$ (2)

The goal is to find the set of invariants having the minimum score over all
possible combinations of randomly generated invariants in conjunction with the
basic invariants.

###  4.3 Selecting Random Invariants

We are not aware of any tractable algorithm for finding the optimal subset
from a large set of random invariants according to the quality measure stated
above.111We conjecture that the problem is NP-hard; it resembles K-means
clustering, which is NP-hard [1]. A feasible solution is to apply a greedy
algorithm (see page 282 of [26] for the general discussions) to a small sample
of the models to find an approximate optimal subset. In practice, it is
sufficient to use a sample size of 0.1–0.2%, or a thousand, whichever is
larger, of the original set of models (see Section 6 for discussions). The
algorithm is detailed in Algorithm 2. The idea of the algorithm is to start
with the basic invariants, then add the random invariants and calculate the
scores one-by-one, keeping the random invariant only if it gives a better
score. Then repeat the process of adding random invariants, calculating the
scores, and picking the best random invariant that minimizes the score until
it cannot be further improved, or a preset maximum number of trials is
reached. This subset of random invariants, which may or may not be truly
optimal, will then be used together with the basic invariants for the next
step.

input : A set of random invariants $R$, a set of models $M$, and maximum
trials $T$

output : A set $K\subseteq R$ of random invariants with $|K|<T$

1

2$K\leftarrow\emptyset$

3 $\textnormal{{bestScore}}\leftarrow\infty$

4 $\textnormal{{done}}\leftarrow\textnormal{{false}}$

5 while  _$\neg{\textnormal{{done}}}\land|K| <T$_ do

6 $\textnormal{{done}}\leftarrow\textnormal{{true}}$

7 $a\leftarrow\emptyset$

8 foreach  _$r\in R\smallsetminus K$_ do

9 $\textnormal{{trialScore}}\leftarrow$ score of $K\cup\\{r\\}$ on $M$
according to equation (2)

10 if  _$\textnormal{{trialScore}} <\textnormal{{bestScore}}$_ then

11 $\textnormal{{bestScore}}\leftarrow\textnormal{{trialScore}}$

12 $a\leftarrow r$

13

14

15 if  _$a\neq\emptyset$_ then

16 $\textnormal{{done}}\leftarrow\textnormal{{false}}$

17 $K\leftarrow K\cup\\{a\\}$

18

19

20return $K$

Algorithm 2 Selecting Random Invariants with Greedy Algorithm

Note that the main purpose of adding randomly generated invariants is not to
divide the models into more blocks in all cases, but to increase the
robustness of the algorithm by the automatic discovery of important invariants
in some cases.

##  5 The Invariant Algorithm

First, we describe the algorithm without the randomly generated invariants.
For each domain element of a model, we calculate the basic invariants and put
them into an ordered list, which is called the invariant vector of that
element. If the model has multiple unary, binary, or ternary operations, then
invariant vectors are calculated for each of them for all elements, and all
the invariant vectors of the same domain element are concatenated to form a
combined invariant vector for that domain element. It follows that each model
with $n$ domain elements will be associated with $n$ combined invariant
vectors. Isomorphic models must have the same set of invariant vectors.

To facilitate comparisons of invariant vectors, we sort the elements by their
invariant vectors lexicographically. It follows that models isomorphic to each
other must have the same sorted invariant vectors.

Our goal is not only to compare two models for isomorphism but to extract all
non-isomorphic models from a list of models. In that case, we set up a hash
map to store blocks of the models where models in different blocks are
guaranteed to be non-isomorphic. We use the invariant vectors for each model
to send the model efficiently to the block (in the hash map) to which it
belongs. That is, the keys in this hash map are the invariant vectors, and the
values are the blocks of the models. After all models are hashed into the hash
map, the blocks stored in the hash map can be processed separately, and
possibly in parallel, to extract one representative model from each
isomorphism class. An example of construction and use of invariants can be
found in [2].

To add random invariants to the algorithm, a preprocessing step is added to
select an optimal subset of random invariants before the normal process. As
described in Section 4.3, we construct a list of random invariants, calculate
basic invariants and the random invariants on a small sample of the input
models. Then apply the greedy algorithm to find an optimal subset of random
invariants for further processing (see Section 4.3). Finally, proceed to
normal processing with the basic invariants and the optimal random invariants
together.

Note that our invariant-based algorithm does not compare models for
isomorphism. It only cuts down the size of the problem to improve the
performance of existing isomorphism filters such as Mace4’s isofilter.

Invariants have the potential to cope with the increasing size of the order of
the algebra very well as illustrated in the following example. Suppose an
invariant with extremely low discriminating power gives only 2 values, 0 and
1. However, when applied to the models of an algebra of order 2, it could
actually give 4 possible invariant vectors: [0,0], [0,1], [1,0], [1,1]. It is
easy to generalize this observation: applying an invariant that gives at most
$m$ values to the models of an algebra of order $n$ could result in a maximum
of $m^{n}$ distinct invariant vectors. Furthermore, if $k$ invariants give
{$m_{1},m_{2},\cdots,m_{k}$} values, then the maximum number of invariant
vectors would be

$\prod_{i=1}^{k}{m_{i}}^{n}$ (3)

From the above analysis on the intricate interactions between invariants, we
can make two more important observations:

  1. 1.

Combining invariants of low discriminating powers could give an invariant
vector of surprisingly high discriminating power if they are targeting
different areas of the algebraic structures.

  2. 2.

In general, the number of non-isomorphic models increases rapidly as the order
of the algebra increases, but so does the maximum number of possible invariant
vectors. This helps invariants to retain their discriminating powers to some
extent as the order of the algebra increases. This explains why the invariant-
based algorithm is very scalable.

##  6 Experimental Results

We have implemented an invariant-based preprocessor to Mace4’s isomorphic
models filters. We run experiments on a 6-core Intel® Core™ i7-9850H CPU
computer, with 32 Gb RAM installed.

The ALF database [3] contains a collection of 158 algebras of high interest to
the research community of algebra. Their definitions are conveniently given in
first-order formulas that Mace4 can directly process. We use Mace4 to generate
models for each algebra of the highest possible order that it can complete
within 2 minutes. Mace4 is not able to generate models for 5 of them within
that time limit, and they are excluded from the tests. The excluded algebras
are: #112 Kleene algebra, #113 Concurrent Kleene algebra, #114 Omega algebra,
#137 Steiner quasigroup, and #138 Steiner loop. In addition, Mace4’s isofilter
is not able to handle two of the largest algebras (#8 BL-algebras and #56
Linear Heyting algebras), each has between 1 to 3 million models. These two
algebras are also excluded from most of the statistics of the experimental
results. So, we end up with 151 algebras in many of our analyses.

When random invariants are used in the experiment, the number of randomly
generated invariants is 50, but at most 20 of the best of them will be used.
The maximum depth of the expression tree (see Section 4.1) is 4, and the
maximum number of variables in it is 3. In this section, random invariants are
used unless otherwise specified.

Since we run a large comprehensive set of test cases for comparison, the size
of each test case is necessarily limited (uniformly and systematically to make
comparisons of results meaningful) by the computing resources available.
However, even for the small model sizes used in our experiments, the addition
of the invariant-based algorithm improves the overall speed by an order of
magnitude, without using parallel processing (see Table 1).

The overheads of calculating invariants are observed to be on average about 20
to 30% of the total run time in our experimental setting (see the third column
in 1). However, invariants improve the speed by orders of magnitudes for big
algebras. For example, for the longest (in terms of runtime) 10 algebras in
our experiment, the invariant-based algorithm improves the overall speed by
over 50 times (see Table 1). In fact, a very desirable feature of the
invariant-based algorithm is that the improvement increases dramatically as
the size of the set of models grows. Granted, for algebras with short runtime,
the use of invariants may not pay off. But for those cases, the degradation is
really insignificant (see Fig. 2). Thus, in general, there is no need to have
special logic to decide when not to use invariants.

Furthermore, Mace4’s isofilter is not able to handle two of the largest data
sets, but our invariant-based algorithm can partition these models into
smaller blocks to fit in Mace4’s limits (see Table 1).

Table 1: Isomorphism Filtering, w/ vs. w/o Invariants |  |  | Total Runtime (s)
---|---|---|---
|  #Mace4 Outputs |  Invariant Calc. Time (s) |  With Invariants |  Without Invariants
Shortest 10 Algebras | 600 | 0.2 | 0.5 | 0.1
Longest 10 Algebras | 9,239,818 | 430 | 1,982 | 87,591
All 151 Algebras | 33,643,548 | 1,500 | 5,030 | 95,952
2 Isofilter Failed Algebras | 4,075,054 | 208 | 727.3 | N/A
$1$$10$$100$$1{,}000$$10{,}000$$1$$10$$100$$1{,}000$$10{,}000$w/ invariantsw/o
invariantstime (s)time(s) Figure 2: Runtimes: w/ vs. w/o Invariants (151 ALF
Algebras)

The performance of the invariant-based algorithm relies heavily on the
discriminating power of its invariants. The best possible case is that only 1
non-isomorphic model is in every block, in which case, only $m-1$ comparisons
of models are needed to eliminate all isomorphic models from a block of $m$
models. Our invariants are quite powerful as evidenced by the fact that the
average number of non-isomorphic models per block is very close to 1 for the
151 algebras in the experiment (see Table 2).

Table 2: Discriminating Power (153 ALF Algebras) | Avg #Non-isomorphic Models per Block
---|---
Percentile | w/ Random Invariants | w/o Random Invariants
95th | 1.346 | 2.677
80th | 1.036 | 1.179
60th | 1.003 | 1.018
40th | 1.000 | 1.005
$0$$1$$2$$3$$4$$5$$6$$7$$8$$9$$10$$11$$12$$13$$14$$15$$16$$17$$18$$19$$10$$20$$40$$60$$80$$90$$100$#
Random InvariantsCumulative Frequency (%)# Random Invariants UsedCum.
Frequency Figure 3: # of Random Invariants (153 ALF Algebras)

###  6.1 Basic Invariants vs. Basic Invariants + Random Invariants

As shown in Table 2, the hand-crafted basic invariants have very good
discriminating power (see the last column in the table). Nevertheless, the
addition of random invariants improves the discriminating powers (see the
middle column of the table). This increase in discriminating power comes with
a small overhead in processing time as the number of random invariants is
quite small, usually just a few. For example, 6 or fewer random invariants are
used in about 90% of the algebras (see Figure 3). For the case when the basic
invariants are already doing a very good job, the addition of random
invariants may not pay off. But the degradation is minimal because the job
would finish fast when the discriminating powers of the invariants are high
(See the scatter plot Fig. 4). Therefore, there is no need for special logic
to decide when not to use random invariants. In our experiment, the overall
run time for all 151 algebras is reduced when random invariants are added,
with most of the improvements coming from the top 3 algebras, which are among
the algebras that take the longest to finish (see Table 3 and Fig. 4).

$0.1$$1$$10$$100$$1{,}000$$0.1$$1$$10$$100$$1{,}000$w/ random invariantsw/o random invariantstime (s)time(s) Figure 4: Runtimes: w/ vs. w/o Random Invariants Table 3: Isomorphism Filtering Time, w/ and w/o Random Invariants | Total Time (s)
---|---
| With Random Invariants | Without Random Invariants
Top 3 Improved Algebras | 760 | 1,882
All 151 Algebras | 5,758 | 6,525

###  6.2 Larger Data Sets

As remarked earlier, to cover a large variety of algebras, we have to limit
the order of each algebra in the experiments. Small datasets do not adequately
show the true advantage of the invariant-based algorithm. Here we present
three examples in which we go two orders higher in each of the algebras,
giving us test datasets of over a hundred million models. The first algebra
(#88 Quasi-MV-algebra) is defined by one binary operation and 1 relation, the
second one (#15 Brouwerian semilattices) by two binary operations, and the
third one (#4 BCK-join-semilattice) by two binary operations and 1 relation.
As shown in Table 4, at the baseline when the order of the algebra is small,
the invariant algorithm slows down the process very slightly. However, as the
order of the algebra goes higher, the invariant-based algorithm improves the
speed by orders of magnitudes. In some cases, Mace4 is not able to handle a
large number of models. In all the tests, we also observe that the
discriminatory powers of the invariants hold up quite well in large datasets
(see Table 5).

Table 4: Isomorphism Filtering, w/ vs. w/o Invariants for Higher Orders

|  |  | Total Runtime (s)
---|---|---|---
| Order |  #Mace4 Outputs |  With Invariants |  Without Invariants
#88 Quasi-MV-algebra | 7 | 10,902 | 1.6 | 0.7
| 8 | 4,793,924 | 558 | 30,701
| 9 | 29,799,618 | 3,666 | N/A1
#15 Brouwerian semilattices | 6 | 47,349 | 12 | 4
| 7 | 2,247,564 | 440 | 1,964
| 8 | 146,875,177 | 40,017 | N/A
#4 BCK-join-semilattice | 9 | 122,754 | 23 | 15
| 10 | 1,175,784 | 305 | 532
| 11 | 12,307,002 | 1,213 | 54,524

  * 1

Isofilter fails after processing 4.5 million (15% of all) models in 11.5
hours.

Table 5: Discriminating Power of Invariants for Higher Orders |  |  | Non-isomorphic Models
---|---|---|---
| Order |  #Blocks |  Total |  Avg per Block
#88 Quasi-MV-algebra | 7 | 567 | 477 | 1.19
| 8 | 153,163 | 55,544 | 2.76
| 9 | 264,972 | 141,750 | 1.87
#15 Brouwerian semilattices | 6 | 745 | 745 | 1.00
| 7 | 8,272 | 8,272 | 1.00
| 8 | 115,801 | 114,943 | 1.01
#4 BCK-join-semilattice | 9 | 26 | 26 | 1.00
| 10 | 47 | 47 | 1.00
| 11 | 82 | 82 | 1.00

###  6.3 Parallel Processing

The invariant-based algorithm is very scalable since the data are divided into
blocks that can be processed independently as long as resources are available.
In this experiment, we apply parallel processing to the top 3 algebras with
the longest runtimes (close to 500s or more). We run each of them with 5
parallel threads and see about a 50 - 60% reduction in run times (see Table
6). The results would be even better if more resources are available as a
large number of blocks are available in these cases.

Table 6: Isomorphism Filtering, Serial vs. Parallel |  |  | Runtime (s)
---|---|---|---
| Order | #Blocks | Serial | Parallel
#8 BL-algebras | 5 | 735,820 | 574 | 254
#20 Commutative lattice-ordered monoids | 7 | 15,499 | 510 | 240
#145 Digroup | 12 | 17 | 488 | 177

##  7 Related Work

Classes of algebras can often be defined in first-order formulas. For these
algebras, a finite model finder, such as Mace4 [22], SEM [30], and FALCON
[29], FMSET [7], etc., can work on finding all their models. A well-known
issue with this approach is that first-order formulas introduce symmetries
into the problem, which leads to the generation of a huge number of isomorphic
models in the outputs [27]. These isomorphic models can either be suppressed
in the search phase or be removed in a postprocessing step after the models
are generated.

Past work in enumerating non-isomorphic finite models has focused on not
generating isomorphic models in the search phase. Symmetry breaking is thus a
central focus of their research [10, 27, 11]. An excellent example of a
simple, powerful, and general algorithm to break symmetry dynamically is the
least number heuristic (LNH) [29, 4], which picks the smallest one not used so
far when a new domain element is to be selected during the search. This is
implemented in many solvers such as Mace4, SEM, FMSET, and FALCON. Another
symmetry breaker, the eXtended least number heuristic (XLNH) [4, 5], is based
on similar ideas as the LNH, but could give better performance if there is at
least one unary operation in the FOL clauses that define the model. It is also
implemented in many finite model enumerators such as SEM.

The underlying idea of LNH can also be applied to break symmetries statically.
This is necessary for approaches where we do not wish to modify the underlying
solver. This is the case for finite model finders based on SAT solvers [27,
10, 17]. The issue is the overhead of encoding LNH in conjunctive normal form
(CNF) as well as its complex interaction with the SAT solver. Originally, LNH
was only encoded for constants [10]. Later, with additional effort, it was
shown that other terms can also be considered [27].

The addition of symmetry-breaking input clauses could be useful in steering
the searcher away from the needless exploration of sub-search space [11]. For
example, it is well-known that a finite semigroup has at least one idempotent
element, so we may add the clause 0 * 0 = 0 to the list of input clauses to
cut off the search of the branch 0 * 0 = 1, etc. However, this kind of
symmetry breaking often requires deep knowledge of the algebra in question,
which may not be available when the algebra is first studied.

Most importantly, these symmetry-breaking techniques do not guarantee
isomorph-freeness. While not generating isomorphic models would be ideal, but
to guarantee that isomorphic models are not produced in the search phase is a
hard problem that few modern-day solvers attempt to do. Systems that do try to
do so, such as SEMK [8, 23] and SEMD [18], are either yet-to-be-completed or
are better off allowing some isomorphic models in the outputs for some cases
for better efficiency.

When isomorphic models are not totally suppressed in the search phase, they
would need to be removed in the post-processing steps. Many of them use a
limited number of invariants to help speed up the process. Mace4, for example,
has a program, isofilter, to filter out isomorphic models that it generates in
the search phase. It calculates one invariant, frequency of occurrence of
domain element, that is, the number of times a domain element appears in the
operation tables. It uses this invariant to help separate non-isomorphic
models and to help guide the construction of isomorphic functions between
potentially isomorphic models. Needless to say, the discriminating power of
one single invariant is limited. Indeed, it fails miserably when the operation
table is a Latin square, which is the case for quasigroups. To alleviate this
issue, Mace4 has another program, isofilter2, which does not try to construct
isomorphic functions between models, but to convert models to their canonical
forms based on the same algorithm [23] used by SEMK. Isofilter2 works very
well with quasigroups, but the overhead in computing the canonical forms of
the models is so high that it becomes slower than isofilter for many algebraic
structures such as semigroups.

The loops package [25] in GAP [14] is not a finite model enumerator but
provides a stand-alone function to extract non-isomorphic models from a list
of quasigroups. It uses 9 invariants, some of which are expensive to
calculate, to help separate non-isomorphic models, and to guide the
construction of isomorphic functions between models having the same invariant
vectors. These 9 invariants exploit the specific properties of the quasigroup,
and may not be effective for other algebraic structures. On the other hand,
our invariants target many different areas in the common algebraic structures.
Furthermore, their invariant vectors are limited to one binary operation
table. Our invariant vectors can be constructed from multiple unary, binary,
and ternary operation tables.

Invariants are sometimes incorporated into the finite-model enumerating
algorithm for specific algebras. These invariants are sometimes very simple
and easy to compute, such as those in the algorithm for enumerating quandles
[13]. But others may be very complicated, not easy to implement, and not cheap
to compute as in the case of the algorithm for enumerating inverse semigroups
[20] using the constraint solver, Minion [15]. Furthermore, the number of
invariants used in these cases is usually very small, often two or fewer.
Recall expression 3 on page 3 which shows that the number of invariants could
increase the discriminating power drastically. Our invariants are cheap to
calculate, are applicable to more algebraic structures, and are high in number
to provide more opportunities for separating non-isomorphic models. Moreover,
they can easily be incorporated into any finite model enumerator.

Neither Mace4’s nor loops’ isomorphic model filters make use of the hash table
to store the models so that non-isomorphic models will never be compared once
they are separated by their invariant vectors. This introduces some
inefficiencies in their algorithms. Thus, both could benefit immensely from
the reduced number of models in the blocks created by our invariant-based
algorithm as a preprocessing step.

Another important feature in the invariant-based algorithm is randomization.
Using randomization in the search phase in Boolean Satisfiability (SAT) and
Constrained Programming (CSP) algorithms is a tried and tested technique [16,
6, 19]. This strategy is built into many SAT solvers such as Chaff [24].
However, using randomly generated invariants to help separate non-isomorphic
models in the finite model enumeration is a novel idea. It helps solve the
hardest problems in filtering isomorphic models as shown in our experiments,
and consequently, increases the robustness of the invariant-based algorithm.

##  8 Future Work and Conclusions

As pointed out in section 6, the efficiency of the invariant-based algorithm
relies heavily on the discriminating powers of both the hand-crafted and the
randomly generated invariants. Future work will therefore concentrate on
finding powerful invariants to target common algebraic structures, and to find
the best parameters to generate optimal random invariants. For example, what
depth and breadth of the expression tree would be most cost-effective in
generating random invariants? What is the best range of ratios of binary
operations to unary operations in a random invariant? What is the best size of
the sample to use in finding the optimal set of random invariants?

In summary, we present in this paper an algorithm that uses invariants both as
discriminators and as hash keys to partition a set of models into blocks, in
which no models across blocks are isomorphic. The blocks are hashed into a
hasp map so that they will not be processed together. Included in the
algorithm is the novel idea of using randomly generated invariants to
supplement hand-crafted invariants to make the algorithm more robust. We show
that the invariant-based algorithm is simple, efficient, scalable, and
parallelizable. It is also compatible with most, if not all, existing finite
model enumerators. It can be used as a stand-alone preprocessor to split
models into blocks to feed into isomorphic model filters, or it can be
directly incorporated into them. Future research will concentrate on finding
powerful invariants in different areas of algebraic structures, and on the
automatic discovery of optimal random invariants.

## Acknowledgments

The results were supported by the Ministry of Education, Youth and Sports
within the dedicated program ERC CZ under the project POSTMAN no. LL1902 and
Fundação para a Ciência e a Tecnologia, through the projects UIDB/00297-/2020
(CMA), PTDC/MAT-PUR/31174/2017, UIDB/04621/2020 and UIDP/04621/2020. This
scientific article is part of the RICAIP project that has received funding
from the European Union’s Horizon 2020 research and innovation programme under
grant agreement No 857306.

## References

  * [1] Daniel Aloise, Amit Deshpande, Pierre Hansen, and Preyas Popat.  Np-hardness of euclidean sum-of-squares clustering.  Mach. Learn., 75(2):245–248, 2009.
  * [2] João Araújo, Choiwah Chow, and Mikoláš Janota.  Filtering isomorphic models by invariants.  In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), volume 210 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:9, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * [3] João Araújo, David Matos, and João Ramires.  Axiomatic library finder (database).  https://axiomaticlibraryfinder.pythonanywhere.com.
  * [4] Gilles Audemard, Belaid Benhamou, and Laurent Henocque.  Predicting and detecting symmetries in FOL finite model search.  J. Autom. Reason., 36(3):177–212, 2006.
  * [5] Gilles Audemard and Laurent Henocque.  The eXtended least number heuristic.  In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of Lecture Notes in Computer Science, pages 427–442, Berlin, Heidelberg, 2001. Springer.
  * [6] Luís Baptista and João P. Marques Silva.  Using randomization and learning to solve hard real-world instances of satisfiability.  In Rina Dechter, editor, Principles and Practice of Constraint Programming - CP 2000, 6th International Conference, Singapore, September 18-21, 2000, Proceedings, volume 1894 of Lecture Notes in Computer Science, pages 489–494, Berlin, Heidelberg, 2000. Springer.
  * [7] Belaid Benhamou and Laurent Henocque.  A hybrid method for finite model search in equational theories.  Fundam. Informaticae, 39(1-2):21–38, 1999.
  * [8] Thierry Boy de la Tour and Prakash Countcham.  An isomorph-free SEM-like enumeration of models.  Electronic Notes in Theoretical Computer Science, 125(2):91–113, 2005.  Proceedings of the 5th International Workshop on Strategies in Automated Deduction (Strategies 2004).
  * [9] Stanley Burris and Hanamantagouda P. Sankappanavar.  A course in universal algebra, volume 78 of Graduate texts in mathematics.  Springer, New York, NY, 1981.
  * [10] Koen Claessen and Niklas Sörensson.  New techniques that improve MACE-style finite model finding.  In Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003.
  * [11] James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy.  Symmetry-breaking predicates for search problems.  In Luigia Carlucci Aiello, Jon Doyle, and Stuart C. Shapiro, editors, Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 148–159, San Francisco, CA, 1996. Morgan Kaufmann.
  * [12] John D. Dixon and Brian Mortimer.  Permutation Groups.  Springer, New York, NY, 1996.
  * [13] Mohamed Elhamdadi, Jennifer Macquarrie, and Ricardo Restrepo.  Automorphism groups of quandles.  J. Algebra Appl., 11(1), 2012.
  * [14] The GAP Group.  GAP – Groups, Algorithms, and Programming, Version 4.11.1, 2021\.
  * [15] Ian P. Gent, Christopher Jefferson, and Ian Miguel.  Minion: A fast scalable constraint solver.  In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors, ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, Including Prestigious Applications of Intelligent Systems (PAIS 2006), Proceedings, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 98–102, Amsterdam, Netherlands, 2006. IOS Press.
  * [16] Carla P. Gomes, Bart Selman, and Henry A. Kautz.  Boosting combinatorial search through randomization.  In Jack Mostow and Chuck Rich, editors, Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 98, IAAI 98, July 26-30, 1998, Madison, Wisconsin, USA, pages 431–437, Menlo Park, CA / Cambridge, MA, 1998. AAAI Press / The MIT Press.
  * [17] Mikoláš Janota and Martin Suda.  Towards smarter MACE-style model finders.  In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, pages 454–470, Manchester, UK, 2018. EasyChair.
  * [18] Xiangxue Jia and Jian Zhang.  A powerful technique to eliminate isomorphism in finite model search.  In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, pages 318–331, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.
  * [19] I. Lynce, L. Baptista, and J. Marques-Silva.  Complete unrestricted backtracking algorithms for satisfiability.  In In Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, pages 214–221, 2002.
  * [20] Martin E. Malandro.  Enumeration of finite inverse semigroups.  Semigroup Forum, 99:679–723, 2019.
  * [21] David Marker.  Model Theory: An Introduction.  Springer, New York, NY, 2002.
  * [22] William McCune.  Mace4 reference manual and guide.  (Technical Memorandum No. 264):20, August 2003.
  * [23] Brendan D McKay.  Isomorph-free exhaustive generation.  Journal of Algorithms, 26(2):306–324, 1998.
  * [24] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik.  Chaff: Engineering an efficient SAT solver.  In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530–535, New York, NY, 2001\. ACM.
  * [25] Gábor Nagy and Petr Vojtěchovský.  LOOPS, computing with quasigroups and loops in GAP, Version 3.4.1.  https://gap-packages.github.io/loops/, Nov 2018.  Refereed GAP package.
  * [26] Christos H. Papadimitriou and Kenneth Steiglitz.  Combinatorial Optimization: Algorithms and Complexity.  Prentice-Hall, Upper Saddle River, NY, 1982.
  * [27] Giles Reger, Martin Riener, and Martin Suda.  Symmetry avoidance in MACE-style finite model finding.  In Andreas Herzig and Andrei Popescu, editors, Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings, volume 11715 of Lecture Notes in Computer Science, pages 3–21, Switzerland AG, 2019. Springer.
  * [28] Neil J. A. Sloane and The OEIS Foundation Inc.  The on-line encyclopedia of integer sequences, 2020.
  * [29] Jian Zhang.  Constructing finite algebras with FALCON.  Journal of Automated Reasoning, 17:1–22, 08 1996.
  * [30] Jian Zhang and Hantao Zhang.  SEM: a system for enumerating models.  In IJCAI, pages 298–303, 1995.