Counting refutations by tiny magmas

Stream: Equational

[Bruno Le Floch]

The script equational_theories/Generated/All4x4Tables/src/check_redundant.py purports to count how many implications are refuted by magmas of size 2, 3, 4. Running it yields output like

When going from ../data/refutations2x2.txt to ../data/refutations3x3.txt
The number of solved equations goes from 12567055 to 13602457 for a delta of 1035402

which supposedly means that magmas of size 2 refute 12567055 implications and magmas of sizes 2 and 3 together refute 13602457 implications. The numbers I get from independent code are different, slightly lower by a couple of thousands. I think the data files equational_theories/Generated/All4x4Tables/data/refutations2x2.txt etc are correct. But I think the Python script check_redundant.py has some off-by-one mistakes. For instance it allocates a matrix of size 4966, two more than the number of equations. It may be behaving as if there were equations numbered 0 and 4965 that are not satisfied by any magma. This could explain getting a bit too many implications.

Can someone check independently of me? We can then compare with what I got: 12560783 refutations by size-2 magmas, 1035338 additional ones by size-3 magmas, 157861 additional ones by size-4 magmas.

[Bruno Le Floch]

Ok, I confirm my numbers: the pre-existing check_redundant.py scripts, corrected to count only entries in matrix[1:4695, 1:4695] instead of matrix (which is matrix[0:4696, 0:4696]), gives the same answer as independent code that runs the Mace4 ATP with domain size ≤4 on every implication one by one. I also got the same data as refutations2x2 using very basic Python code. PR incoming with corrected numbers in section 5 of the paper.

The start of section 5 also claims that 524 magmas are enough for all refutations by small magmas. I've changed this to 523, computed as follows. The three files equational_theories/Generated/All4x4Tables/data/refutations2x2.txt and 3x3 and 4x4 list respectively 10, 299, and 515 magmas. The output of check_redundant.py (given in equational_theories/Generated/All4x4Tables/README.md) ends with a claim that 10 / 10 magmas of size 2 are already covered by magmas of size 4 (which is obvious since a size-2 magma can be squared), and 291/299 magmas of size 3 are covered by magmas of size 4, in the sense that any non-implication with a size-3 model among these 291 has a size-4 model. This means we can get away with the 515 models of size 4, plus 299-291=8 of size 3, for a total of 515+8=523. Does that sound correct?

[Douglas McNeil]

Brute force confirms "12560783 refutations by size-2 magmas, 1035338 additional ones by size-3 magmas"; 178M>>3300 so that one will have to run for a bit..

[Douglas McNeil]

And I can confirm 157861 additional ones by size-4 magmas as well.

[Bruno Le Floch]

Thanks a lot! It's reassuring to have confirmation.