Search for magic squares of square numbers that have one mistake, either a row, column or diagonal

magic_square_7_of_8.snt

#!/usr/bin/env sentient -c -o -r -n 0 -m lingeling magic_square_7_of_8.snt

# Based on: https://twitter.com/standupmaths/status/1214921447644250113
# Written in Sentient: https://sentient-lang.org/

function main() {
  int12 a, b, c, d, e, f, g, h, i;

  # Needs to be: ceil(log2((2^(bits - 1))^2 * 3)) + 1
  int25 magicSum;

  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;

  validLines = [
    a2 + b2 + c2 == magicSum,
    d2 + e2 + f2 == magicSum,
    g2 + h2 + i2 == magicSum,

    a2 + d2 + g2 == magicSum,
    b2 + e2 + h2 == magicSum,
    c2 + f2 + i2 == magicSum,

    a2 + e2 + i2 == magicSum,
    c2 + e2 + g2 == magicSum
  ];

  # Seven of the lines must add to the magic sum.
  invariant validLines.countBy(*self) == 7;

  invariant [a, b, c, d, e, f, g, h, i].uniq?;
  invariant [a, b, c, d, e, f, g, h, i].none?(*negative?);

  # Disallow translational and rotation symmetries.
  # See: https://www.cse.unsw.edu.au/~tw/kwecai2010.pdf
  invariant a < [c, g, i].minimum, c < g;

  # TODO: Disallow 'variable symmetries'

  # Disallow multiples of the Jeremy Nehring's solution.
  invariant magicSum % 21609 != 0;

  # Disallow multiples of other solutions.
  invariant magicSum % 257049 != 0;
  invariant magicSum % 1172889 != 0;

  expose a, b, c, d, e, f, g, h, i, magicSum;
};

function minimum (numbers) {
  return numbers.reduce(function (min, n) {
    return min < n ? min : n;
  });
};

main();

# Solutions:
# {"a":58,"b":94,"c":97,"d":46,"e":113,"f":82,"g":127,"h":2,"i":74,"magicSum":21609}
# {"a":62,"b":446,"c":233,"d":313,"e":218,"f":334,"g":394,"h":103,"i":302,"magicSum":257049}
# {"a":386,"b":713,"c":718,"d":503,"e":802,"f":526,"g":878,"h":146,"i":617,"magicSum":1172889}
# ... more to come (hopefully)