Bug in Mace4 isofilter (Windows)

Stream: Equational

[Zoltan A. Kocsis (Z.A.K.)]

Jose Brox said:

You mean that they are isomorphic? (Looking at your script, you find the permutation between them, right?). But Mace4's isofilter says they are not isomorphic!

Drive-by comment, but are you sure? When I run mace4/isofilter on the models in models.py, it does return one representative.

$ cat isotest_models.txt | ./get_interps
interpretation( 7, [number=1, seconds=0], [
        function(+(_,_), [
               3, 4, 2, 0, 6, 1, 5,
               5, 3, 4, 1, 0, 2, 6,
               0, 5, 3, 2, 1, 6, 4,
               2, 6, 0, 3, 5, 4, 1,
               1, 2, 6, 4, 3, 5, 0,
               6, 0, 1, 5, 4, 3, 2,
               4, 1, 5, 6, 2, 0, 3 ])
]).
interpretation( 7, [number=2, seconds=0], [
        function(+(_,_), [
               3, 1, 4, 0, 6, 2, 5,
               0, 3, 5, 1, 2, 6, 4,
               5, 4, 3, 2, 0, 1, 6,
               1, 0, 6, 3, 5, 4, 2,
               2, 6, 1, 4, 3, 5, 0,
               6, 2, 0, 5, 4, 3, 1,
               4, 5, 2, 6, 1, 0, 3 ])
]).
interpretation( 7, [number=3, seconds=0], [
        function(+(_,_), [
               3, 4, 5, 0, 2, 1, 6,
               5, 3, 2, 1, 0, 6, 4,
               4, 1, 3, 2, 6, 0, 5,
               6, 2, 1, 3, 5, 4, 0,
               1, 6, 0, 4, 3, 5, 2,
               2, 0, 6, 5, 4, 3, 1,
               0, 5, 4, 6, 1, 2, 3 ])
]).
 $ cat isotest_models.txt | ./get_interps | ./isofilter
interpretation( 7, [number = 1,seconds = 0], [
    function(+(_,_), [
        3,4,2,0,6,1,5,
        5,3,4,1,0,2,6,
        0,5,3,2,1,6,4,
        2,6,0,3,5,4,1,
        1,2,6,4,3,5,0,
        6,0,1,5,4,3,2,
        4,1,5,6,2,0,3])]).
% isofilter: input=3, kept=1, checks=2, perms=218, 0.00 seconds.

[Notification Bot]

A message was moved here from #Equational > Higman-Neumann characterization of groups by Jose Brox.

[Jose Brox]

Zoltan A. Kocsis (Z.A.K.) ha dicho:

Drive-by comment, but are you sure? When I run mace4/isofilter on the models in models.py, it does return one representative

Ok, I had seen some weird things in the Windows GUI isofilter (the model count being 1 more than the actual models listed, too many non-isomorphic models...), and with your feedback now I have made some probing and I think we can say that it has two bugs:

1) The "ignore constants" button does not work properly: if the button is checked, but the list of operators to check includes the constants, the constants are taken into account. This explains why isofilter didn't remove the isomorphic models.

2) If the list of operators to output does not have a space character after the * operator, one model drops out from the list. In practice, if the list of isoclasses has just one model, the list will appear empty! This is solved by adding a space after the * symbol. Weird, huh?

Here there is some visual proof:

Isofilter 1.JPG
Isofilter 2.JPG
Isofilter 3.JPG
Isofilter 4.JPG
Isofilter 5.JPG
Isofilter 6.JPG

[Zoltan A. Kocsis (Z.A.K.)]

Crazy, thanks for tracking these down.
I've never used the Windows version before, and now I'm glad I didn't :)

Can you check whether the mace4 executable, when you run it from the command line, reports version 2009-11A or something earlier?

[Jose Brox]

Zoltan A. Kocsis (Z.A.K.) ha dicho:

Can you check whether the mace4 executable, when you run it from the command line, reports version 2009-11A or something earlier?

It says Dec-2007! The GUI help also says the same: version 0.5 Dec-2007.

[Shreyas Srinivas]

what's the TL;DR?

[Zoltan A. Kocsis (Z.A.K.)]

@Shreyas Srinivas Either the Windows GUI used above has a bug, or an old version of mace4/isofilter does (probably the GUI). Due to the bug, in some cases two isomorphic magmas are not declared isomorphic when tested by this specific gui / mace4 combo. Newer versions of mace4, ran from a Linux terminal, definitely don't display this bug.

I doubt there's any correctness concern and this shouldn't affect any of the conjectures in the repo; in particular no affected versions were used in generating the magma lists in All4x4Tables.

[Jose Brox]

Even if isomorphic magmas were tested, this only adds redudancy, should only amount to lost time.

[Jose Brox]

(@Zoltan A. Kocsis (Z.A.K.) this may interest you)

Thanks to @Douglas McNeil we have found another, more serious bug in Mace4's isofilter in the Windows GUI:

When looking for models of size 7 for 677, Mace4 with selection_order 2, selection_measure 3, skolems_last set finds 4 models, which come in two kinds, with or without constant squares.

When applying isofilter in the GUI, it only returns the model with non-constant squares (see the pictures below).

Isofilter serious bug 1.JPG
Isofilter serious bug 2.JPG

I have checked and isofilter (2009-11A version) in the Ubuntu command line gives the right answer, with two isoclasses.

[Zoltan A. Kocsis (Z.A.K.)]

Thanks for tagging me, this is very interesting indeed!