How did we manually find 5x5, 11x11, 13x13

Stream: Equational

[Michael Bucko]

How did we find these 3?

1. Table [[0,2,3,0,0],[4,1,4,4,1],[2,2,2,2,2],[3,3,3,3,3],[4,4,4,4,4]]
   Proves [1,3,8,23,47,48,49,99,151,203,255,307,326,359,375,377,378,411,412,413,414,415,416,417,418,614,615,616,617,618,619,620,621,622,625,817,818,819,1020,1022,1023,1025,1223,1426,1427,1428,1629,1832,2035,2238,2240,2243,2441,2644,2847,3050,3253,3254,3255,3318,3319,3320,3456,3522,3659,3715,3721,3722,3724,3725,3862,3915,3925,3927,3928,4065,4118,4120,4121,4127,4128,4130,4131,4380,4470,4472,4473,4598,4599,4629]

2. Table [[0,2,3,4,6,1,8,5,10,7,9],[2,1,6,5,7,4,10,9,0,8,3],[3,6,2,8,1,7,5,10,9,4,0],[4,5,8,3,10,9,2,6,1,0,7],[6,7,1,10,4,8,9,0,3,5,2],[1,4,7,9,8,5,0,3,2,10,6],[8,10,5,2,9,0,6,1,7,3,4],[5,9,10,6,0,3,1,7,4,2,8],[10,0,9,1,3,2,7,4,8,6,5],[7,8,4,0,5,10,3,2,6,9,1],[9,3,0,7,2,6,4,8,5,1,10]]
   Proves [1,3,8,23,43,47,99,151,203,255,307,326,332,359,375,387,411,474,476,614,670,677,817,1020,1112,1119,1223,1288,1315,1426,1629,1832,2035,2238,2257,2264,2441,2450,2460,2644,2847,2910,2937,3050,3076,3113,3253,3319,3342,3456,3522,3545,3659,3715,3722,3724,3749,3751,3758,3862,3915,3964,4065,4118,4167,4283,4343,4358,4380,4398,4405,4435,4442,4470,4482,4531,4544,4608,4635,4677]

3. Table [[0,2,3,4,5,6,7,8,9,10,11,12,1],[2,1,11,7,9,4,8,0,3,12,6,5,10],[3,11,2,12,8,10,5,9,0,4,1,7,6],[4,7,12,3,1,9,11,6,10,0,5,2,8],[5,9,8,1,4,2,10,12,7,11,0,6,3],[6,4,10,9,2,5,3,11,1,8,12,0,7],[7,8,5,11,10,3,6,4,12,2,9,1,0],[8,0,9,6,12,11,4,7,5,1,3,10,2],[9,3,0,10,7,1,12,5,8,6,2,4,11],[10,12,4,0,11,8,2,1,6,9,7,3,5],[11,6,1,5,0,12,9,3,2,7,10,8,4],[12,5,7,2,6,0,1,10,4,3,8,11,9],[1,10,6,8,3,7,0,2,11,5,4,9,12]]
   Proves [1,3,8,23,43,47,99,151,203,255,307,326,332,359,375,387,411,501,503,614,706,713,817,1020,1076,1083,1223,1286,1313,1426,1629,1832,2035,2238,2294,2301,2441,2504,2531,2644,2847,2856,2866,3050,3069,3106,3253,3319,3342,3456,3522,3545,3659,3715,3722,3724,3749,3751,3758,3862,3915,3964,4065,4118,4167,4283,4343,4358,4380,4398,4405,4435,4442,4470,4482,4531,4544,4608,4635,4677]

[Vlad Tsyrklevich]

Is this something git log -p could answer?

[Michael Bucko]

Vlad Tsyrklevich schrieb:

Is this something git log -p could answer?

11x11 gets me here: https://github.com/teorth/equational_theories/pull/337

13x13 gets me here:
https://github.com/teorth/equational_theories/pull/330

I see the question from @Terence Tao on GH "Fascinating! Was the 13x13 example constructed by hand, or created by Z3, or some mix of both?" but there's no answer there.

But I found the relevant Zulip ticket for 13x13 from Zoltan -- it's "A magma of order < 13 - for Equation2531?"

@Zoltan A. Kocsis (Z.A.K.) Is there a script or a group of scripts that I can check out related to 5x5, 11x11, and 13x13?

[Michael Bucko]

Also, are there any such solutions to larger magmas? 20x20,50x50, 100x100, and so on?

[Vlad Tsyrklevich]

Magmas for some equations are trivially constructible, e.g. any constant law magma, though this is obviously not the rule. Generally the focus has been to find the smallest magmas necessary to make checking satisfiability feasible, though I'm not sure all of what others have found searching for larger magmas

[Michael Bucko]

Vlad Tsyrklevich schrieb:

Magmas for some equations are trivially constructible, e.g. any constant law magma, though this is obviously not the rule. Generally the focus has been to find the smallest magmas necessary to make checking satisfiability feasible, though I'm not sure all of what others have found searching for larger magmas

To share more context:

• I looked at the Vampire proven examples (but still can't run Vampire on a macbook pro; I'll just use a shell for the time being)
• I converted some TPTP to Minizinc to learn more about minizinc,
• I used Z3 API too for one equation, but then the script ran indefinitely,
• I looked at FinSearch, Confluence, Greedy, all these simpler rewrites etc. (I guess many of the implications have been established by those methods)
• ..
  and I hope to know deeply understand the exact process of how those particular three (or more such bigger ones) have been found? (if this is Z3+Vampire, then how exactly? is there a TPTP for it?)

I think we'd need to extremely well document those very special cases (others may perhaps judge better which cases are truly special / unique). It'd be great if more people could reproduce them.