parker_square.snt

int8 m, n, p, q;

m2 = m.square;
n2 = n.square;
p2 = p.square;
q2 = q.square;

# ceil(log2(sqrt((2 ** (bits - 1)) ** 2 ** 2 * 3)) + 1)
int16 inner, outer1, outer2;
int2 i;

invariant inner * inner == m2 * n2 + m2 * p2 + n2 * p2;
invariant outer1 * outer1 == m2 + n2 + p2 + i * 2 * inner;
invariant i == 1 || i == -1;

mn = m * n;
mp = m * p;
mq = m * q;
np = n * p;
nq = n * q;
pq = p * q;

a = (m2 + n2 - p2 - q2).abs;
b = (2 * np - 2 * mq).abs;
c = (2 * mp + 2 * nq).abs;
d = (2 * mq + 2 * np).abs;
e = (m2 - n2 + p2 - q2).abs;
f = (2 * pq - 2 * mn).abs;
g = (2 * nq - 2 * mp).abs;
h = (2 * mn + 2 * pq).abs;
i = (m2 - n2 - p2 + q2).abs;

a2 = a.square;
b2 = b.square;
c2 = c.square;
d2 = d.square;
e2 = e.square;
f2 = f.square;
g2 = g.square;
h2 = h.square;
i2 = i.square;

square = [a, b, c, d, e, f, g, h, i];

row1 = a2 + b2 + c2;
dia1 = a2 + e2 + i2;
dia2 = c2 + e2 + g2;
sum = row1;

invariant sum == dia1 || sum == dia2;
invariant square.uniq?;

# Symmetry breaking constraints:
invariant 0 <= m, m <= n, n <= p, p <= q;

expose m, n, p, q, sum, square;

# Solutions:
# {"m":1,"n":3,"p":4,"q":11,"sum":21609,"square":[127,2,74,46,113,82,58,94,97]}
# {"m":3,"n":5,"p":8,"q":14,"sum":86436,"square":[226,4,188,164,148,194,92,254,116]}
# {"m":7,"n":8,"p":15,"q":26,"sum":1028196,"square":[788,124,626,604,466,668,206,892,436]}
# {"m":2,"n":6,"p":8,"q":22,"sum":345744,"square":[508,8,296,184,452,328,232,376,388]}
# {"m":6,"n":10,"p":16,"q":28,"sum":1382976,"square":[904,16,752,656,592,776,368,1016,464]}
# {"m":11,"n":24,"p":35,"q":62,"sum":33246756,"square":[4372,316,3746,3044,3074,3812,2206,4868,2164]}
# {"m":3,"n":9,"p":12,"q":33,"sum":1750329,"square":[1143,18,666,414,1017,738,522,846,873]}
# {"m":5,"n":15,"p":20,"q":55,"sum":13505625,"square":[3175,50,1850,1150,2825,2050,1450,2350,2425]}
# {"m":5,"n":16,"p":21,"q":38,"sum":4691556,"square":[1604,292,1426,1052,1234,1436,1006,1756,772]}
# {"m":4,"n":12,"p":16,"q":44,"sum":5531904,"square":[2032,32,1184,736,1808,1312,928,1504,1552]}
# {"m":14,"n":16,"p":30,"q":52,"sum":16451136,"square":[3152,496,2504,2416,1864,2672,824,3568,1744]}
# {"m":10,"n":11,"p":48,"q":63,"sum":42172036,"square":[6052,204,2346,2316,1686,5828,426,6268,1644]}
# {"m":9,"n":15,"p":24,"q":42,"sum":7001316,"square":[2034,36,1692,1476,1332,1746,828,2286,1044]}
# {"m":12,"n":20,"p":32,"q":56,"sum":22127616,"square":[3616,64,3008,2624,2368,3104,1472,4064,1856]}
# {"m":8,"n":24,"p":32,"q":88,"sum":88510464,"square":[8128,128,4736,2944,7232,5248,3712,6016,6208]}
# {"m":7,"n":21,"p":28,"q":77,"sum":51883209,"square":[6223,98,3626,2254,5537,4018,2842,4606,4753]}
# {"m":9,"n":27,"p":36,"q":99,"sum":141776649,"square":[10287,162,5994,3726,9153,6642,4698,7614,7857]}
# {"m":16,"n":39,"p":55,"q":98,"sum":207532836,"square":[10852,1154,9404,7426,7844,9532,5884,12028,5314]}
# {"m":18,"n":30,"p":48,"q":84,"sum":112021056,"square":[8136,144,6768,5904,5328,6984,3312,9144,4176]}
# {"m":11,"n":33,"p":44,"q":121,"sum":316377369,"square":[15367,242,8954,5566,13673,9922,7018,11374,11737]}
# {"m":21,"n":35,"p":56,"q":98,"sum":207532836,"square":[11074,196,9212,8036,7252,9506,4508,12446,5684]}
# {"m":13,"n":35,"p":48,"q":86,"sum":123076836,"square":[8306,1124,7268,5596,6148,7346,4772,9166,4036]}
# {"m":15,"n":25,"p":40,"q":70,"sum":54022500,"square":[5650,100,4700,4100,3700,4850,2300,6350,2900]}
# {"m":7,"n":33,"p":40,"q":74,"sum":67469796,"square":[5938,1604,5444,3676,4916,5458,4324,6382,2836]}
# {"m":22,"n":48,"p":70,"q":124,"sum":531948096,"square":[17488,1264,14984,12176,12296,15248,8824,19472,8656]}
# {"m":27,"n":45,"p":72,"q":126,"sum":567106596,"square":[18306,324,15228,13284,11988,15714,7452,20574,9396]}
# {"m":15,"n":48,"p":63,"q":114,"sum":380016036,"square":[14436,2628,12834,9468,11106,12924,9054,15804,6948]}
# {"m":10,"n":32,"p":42,"q":76,"sum":75064896,"square":[6416,1168,5704,4208,4936,5744,4024,7024,3088]}
# {"m":21,"n":24,"p":45,"q":78,"sum":83283876,"square":[7092,1116,5634,5436,4194,6012,1854,8028,3924]}
# {"m":28,"n":32,"p":60,"q":104,"sum":263218176,"square":[12608,1984,10016,9664,7456,10688,3296,14272,6976]}
# {"m":24,"n":40,"p":64,"q":112,"sum":354041856,"square":[14464,256,12032,10496,9472,12416,5888,16256,7424]}
# {"m":10,"n":30,"p":40,"q":110,"sum":216090000,"square":[12700,200,7400,4600,11300,8200,5800,9400,9700]}
# {"m":9,"n":56,"p":65,"q":122,"sum":498450276,"square":[15892,5084,14834,9476,13714,14852,12494,16868,7604]}
# {"m":6,"n":18,"p":24,"q":66,"sum":28005264,"square":[4572,72,2664,1656,4068,2952,2088,3384,3492]}
# {"m":12,"n":45,"p":65,"q":112,"sum":358647844,"square":[14600,3162,11640,8538,10200,13480,8520,15640,6438]}
# {"m":20,"n":22,"p":96,"q":126,"sum":674752576,"square":[24208,816,9384,9264,6744,23312,1704,25072,6576]}
# {"m":14,"n":33,"p":35,"q":72,"sum":59197636,"square":[5124,294,5732,4326,4852,4116,3772,5964,3066]}
#
# Notes:
#
# - many of these are k^2 multiples of other sums, e.g. 86436 = 2^2 * 21609
#
# - many of these are k multiples of m,n,p,q, e.g. {1, 3, 4, 11}, {10, 30, 40, 110}
#
# - there are squares obtained by dividing by k^2 even though no m,n,p,q exists:
#   e.g. [788,124,626,604,466,668,206,892,436] => [394,62,313,302,233,334,103,446,218]
#
# - there are m,n,p,q solutions but their squares have duplicates:
#   e.g. {7, 7, 30, 40} => [2402,140,980,980,700,2302,140,2498,700]
#
# - in almost every case, p is equal to m + n or kq
#
# - the sum 207532836 has two(!) unique m,n,p,q solutions:
#   {"m":16,"n":39,"p":55,"q":98,"square":[10852,1154,9404,7426,7844,9532,5884,12028,5314]}
#   {"m":21,"n":35,"p":56,"q":98,"square":[11074,196,9212,8036,7252,9506,4508,12446,5684]}