Function Repository Resource:

FindFiniteModels

Find finite models consistent with the set of relations

Contributed by: Nikolay Murzin

ResourceFunction["FindFiniteModels"][rels]

finds models in form of multiplication tables consistent with the relations rels for each operator in rels, assuming each variable can have one of two values.

ResourceFunction["FindFiniteModels"][rels,k]

allows k≥2 values for each variable.

ResourceFunction["FindFiniteModels"][rels,k,prop]

returns a specified property prop of found models.

Details and Options

The relations rels can be given in terms of operators in logical form with equalities/inequalities or string relations.

There are k^{k^a} models for each operator of arity a.

Property prop may be one of following:

"Association"

returns an association with multiplication tables as values and indices as keys for each found model (default)

"Indices"

returns a list of indices for models

"Models"

returns a list of models

The following options can be given:

Method

"ExpressionPrune"

the method to use

"Parallelize"

False

whether to run some operations in parallel

MaxItems

Infinity

limit the number of returned models

"ReverseOrdering"

False

ordering of indices

The following values can be given for the Method option:

"ExpressionPrune"

pruned search over relations converted to a conjunction of DNFs

"BruteForce"

a complete search over all possible models

Automatic

same as "ExpressionPrune"

Examples

Basic Examples (7)

Find binary models for a nullary operator:

In[1]:=

Out[1]=

Find ternary models for a nullary operator:

In[2]:=

Out[2]=

Find binary models for unary operators:

In[3]:=

Out[3]=

In[4]:=

Out[4]=

In[5]:=

Out[5]=

Find binary models for a binary operator:

In[6]:=

Out[6]=

Find ternary models for a binary operator:

In[7]:=

Out[7]=

Find binary models for a ternary operator:

In[8]:=

Out[8]=

Include constants:

In[9]:=

Out[9]=

Scope (8)

In absence of operators, FindFiniteModels assumes all atoms are nullary operators:

In[10]:=

Out[10]=

Multiple operators with different arities is supported:

In[11]:=

Out[11]=

Inequalities:

In[12]:=

Out[12]=

In[13]:=

Out[13]=

In[14]:=

Out[14]=

Alternatives:

In[15]:=

Out[15]=

Disjunctions:

In[16]:=

Out[16]=

Quantifiers:

In[17]:=

Out[17]=

In[18]:=

Out[18]=

String relations have additional axioms:

In[19]:=

Out[19]=

String relations form a monoid with binary associative operator ∘ (\[SmallCircle]) and nullary identity 1:

In[20]:=

$ResourceFunction["FindFiniteModels"]["A" -> "AA", 3] == ResourceFunction[ "FindFiniteModels"][{"A" == "A"\[SmallCircle]"A", ("A"\[SmallCircle]"B")\[SmallCircle]"C" == "A"\[SmallCircle]("B"\[SmallCircle]"C"), "1"[]\[SmallCircle]"A" == "A", "A"\[SmallCircle]"1"[] == "A"}, 3]$

Out[20]=

Options (8)

Method (1)

"BruteForce" method may be useful if a relation is very general so that enumerating models and finding a small subset of them returns faster:

In[21]:=

Out[21]=

In[22]:=

Out[22]=

Parallelize (1)

Setting the option "Parallelize" to True may speed up computation:

In[23]:=

$Length@ResourceFunction["FindFiniteModels"][ b\[SmallCircle](a\[SmallCircle]a) == a, 8, "Parallelize" -> False] // AbsoluteTiming$

Out[23]=

In[24]:=

$Length@ResourceFunction["FindFiniteModels"][ b\[SmallCircle](a\[SmallCircle]a) == a, 8, "Parallelize" -> True] // AbsoluteTiming$

Out[24]=

In[25]:=

$ResourceFunction[ "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 4, "Parallelize" -> False] // AbsoluteTiming$

Out[25]=

In[26]:=

Out[26]=

MaxItems (1)

Limiting a number of returned models reduces an amount of performed computation:

In[27]:=

Out[27]=

ReverseOrdering (5)

By default, models are indexed by their corresponding inputs (shifted by 1). For example, a model of Not for BooleanAxioms is {1, 0} because {1, 0}[[0+1]] ==1 and {1, 0}[[1+1]] ==0:

In[28]:=

Out[28]=

For some cases, like the default ordering of truth tables for boolean expressions, the convention is to use a reversed ordering {1,0}<->{True,False}:

In[29]:=

Out[29]=

For the first {8, 14, 1}, with "ReverseOrdering"→True, model indices correspond exactly to BooleanFunction indices and models to truth tables. Here CirclePlus is a model of And:

In[30]:=

Out[30]=

In[31]:=

Out[31]=

CircleTimes is a model of Or:

In[32]:=

Out[32]=

In[33]:=

Out[33]=

OverBar is a model of Not:

In[34]:=

Out[34]=

In[35]:=

Out[35]=

Neat Examples (3)

Define functions to be used throughout this example:

In[36]:=

$NestedTupleFromIndex[index_, k_, n_] := ArrayReshape[IntegerDigits[index, k, k^n], Table[k, n]] plotRelationConstraints // ClearAll plotRelationConstraints[expr_, k_ : 2, limit_ : Infinity, n_ : UpTo[6]] := Module[{indices = ResourceFunction["FindFiniteModels"][expr, k, "Indices", "Parallelize" -> True, MaxItems -> limit], sampleIndices, tables}, sampleIndices = Take[indices, n]; tables = Map[NestedTupleFromIndex[#[[1]], k, 2] &, sampleIndices]; Framed@Row[ Append[ ArrayPlot[#, Mesh -> True, ImageSize -> 32] & /@ tables, If[Length[sampleIndices] == 0, Row@{"(", 0, ")"}, If[Length[indices] - Length[sampleIndices] > 0, Row@{"\[Ellipsis]", "(", Length[indices], ")"}, Nothing]] ] ] ]$

Find models for abelian semigroup theory axioms:

In[37]:=

$Row[Riffle[ plotRelationConstraints[{a\[CenterDot]b == b\[CenterDot]a, (a\[CenterDot]b)\[CenterDot]c == a\[CenterDot](b\[CenterDot]c)}, #] & /@ Range[2, 4], Spacer[8]]]$

Out[37]=

Reproduce and extend some :

In[38]:=

$Scan[relation |-> Print[AbsoluteTiming@ Row[Riffle[ Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 4], Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == a, b\[SmallCircle](a\[SmallCircle]b) == a, b\[SmallCircle](b\[SmallCircle]a) == a}]$

In[39]:=

$Scan[relation |-> Print[AbsoluteTiming@ Row[Riffle[ Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 6], Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == a, b\[SmallCircle](a\[SmallCircle]b) == a}]$

In[40]:=

$Scan[relation |-> Print[AbsoluteTiming@ Row[Riffle[ Prepend[plotRelationConstraints[{relation}, #, 2] & /@ Range[2, 10], Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == a, b\[SmallCircle](a\[SmallCircle]b) == a}]$

In[41]:=

$Scan[relation |-> Print[AbsoluteTiming@ Row[Riffle[ Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 3], Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == 0}]$

In[42]:=

$Scan[relation |-> Print[AbsoluteTiming@ Row[Riffle[ Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 10], Framed[relation, Background -> LightGray]], Spacer[8]]]], {a\[SmallCircle]b == a, b\[SmallCircle]a == a}]$