Solving magic squares using SMT solving

generate_smt.py

# generates SMTLIB input for SMT solvers such as [MiniSmt](http://cl-informatik.uibk.ac.at/software/minismt/)
rows = range(1, 8)
cols = ['a', 'b', 'c', 'd', 'e', 'f', 'g']

def assert_sum(v, cells):
  print(f':assumption (= {v} (+ {cells}))')

print('(benchmark none')
print(':logic QF_NIA')

# cells are of type natural numbers
for r in rows:
  for c in cols:
    print(f':extrafuns (({c}{r} Nat))')

# each row/col contains 1..7
for r in rows:
  for val in rows:
    print(':assumption (or ', ' '.join([f'(= {val} {c}{r})' for c in cols]), ')')
for c in cols:
  for val in rows:
    print(':assumption (or ', ' '.join([f'(= {val} {c}{r})' for r in rows]), ')')

# assert additional hints
assert_sum(4, 'd2 d3') # hint 1
assert_sum(5, 'd7 e7') # hint 2
assert_sum(7, 'a1 b1') # hint 3
assert_sum(8, 'a6 a7') # hint 4
assert_sum(12, 'b2 c2 d2') # hint 5
assert_sum(13, 'c6 c7') # hint 6
assert_sum(3, 'g5 g6') # hint 7
assert_sum(7, 'c1 c2 c3') # hint 8
assert_sum(8, 'f6 f7') # hint 9
assert_sum(12, 'g1 g2 g3') # hint 10
assert_sum(13, 'e2 e3') # hint 11
assert_sum(14, 'b4 b5 b6 b7') # hint 12
assert_sum(16, 'a4 b4 c4 d4') # hint 13
assert_sum(17, 'a6 b6 c6') # hint 14

print(':formula true')
print(')')

magic_squares.smt

(benchmark none
:logic QF_NIA
:extrafuns ((a1 Nat))
:extrafuns ((b1 Nat))
:extrafuns ((c1 Nat))
:extrafuns ((d1 Nat))
:extrafuns ((e1 Nat))
:extrafuns ((f1 Nat))
:extrafuns ((g1 Nat))
:extrafuns ((a2 Nat))
:extrafuns ((b2 Nat))
:extrafuns ((c2 Nat))
:extrafuns ((d2 Nat))
:extrafuns ((e2 Nat))
:extrafuns ((f2 Nat))
:extrafuns ((g2 Nat))
:extrafuns ((a3 Nat))
:extrafuns ((b3 Nat))
:extrafuns ((c3 Nat))
:extrafuns ((d3 Nat))
:extrafuns ((e3 Nat))
:extrafuns ((f3 Nat))
:extrafuns ((g3 Nat))
:extrafuns ((a4 Nat))
:extrafuns ((b4 Nat))
:extrafuns ((c4 Nat))
:extrafuns ((d4 Nat))
:extrafuns ((e4 Nat))
:extrafuns ((f4 Nat))
:extrafuns ((g4 Nat))
:extrafuns ((a5 Nat))
:extrafuns ((b5 Nat))
:extrafuns ((c5 Nat))
:extrafuns ((d5 Nat))
:extrafuns ((e5 Nat))
:extrafuns ((f5 Nat))
:extrafuns ((g5 Nat))
:extrafuns ((a6 Nat))
:extrafuns ((b6 Nat))
:extrafuns ((c6 Nat))
:extrafuns ((d6 Nat))
:extrafuns ((e6 Nat))
:extrafuns ((f6 Nat))
:extrafuns ((g6 Nat))
:extrafuns ((a7 Nat))
:extrafuns ((b7 Nat))
:extrafuns ((c7 Nat))
:extrafuns ((d7 Nat))
:extrafuns ((e7 Nat))
:extrafuns ((f7 Nat))
:extrafuns ((g7 Nat))
:assumption (or  (= 1 a1) (= 1 b1) (= 1 c1) (= 1 d1) (= 1 e1) (= 1 f1) (= 1 g1) )
:assumption (or  (= 2 a1) (= 2 b1) (= 2 c1) (= 2 d1) (= 2 e1) (= 2 f1) (= 2 g1) )
:assumption (or  (= 3 a1) (= 3 b1) (= 3 c1) (= 3 d1) (= 3 e1) (= 3 f1) (= 3 g1) )
:assumption (or  (= 4 a1) (= 4 b1) (= 4 c1) (= 4 d1) (= 4 e1) (= 4 f1) (= 4 g1) )
:assumption (or  (= 5 a1) (= 5 b1) (= 5 c1) (= 5 d1) (= 5 e1) (= 5 f1) (= 5 g1) )
:assumption (or  (= 6 a1) (= 6 b1) (= 6 c1) (= 6 d1) (= 6 e1) (= 6 f1) (= 6 g1) )
:assumption (or  (= 7 a1) (= 7 b1) (= 7 c1) (= 7 d1) (= 7 e1) (= 7 f1) (= 7 g1) )
:assumption (or  (= 1 a2) (= 1 b2) (= 1 c2) (= 1 d2) (= 1 e2) (= 1 f2) (= 1 g2) )
:assumption (or  (= 2 a2) (= 2 b2) (= 2 c2) (= 2 d2) (= 2 e2) (= 2 f2) (= 2 g2) )
:assumption (or  (= 3 a2) (= 3 b2) (= 3 c2) (= 3 d2) (= 3 e2) (= 3 f2) (= 3 g2) )
:assumption (or  (= 4 a2) (= 4 b2) (= 4 c2) (= 4 d2) (= 4 e2) (= 4 f2) (= 4 g2) )
:assumption (or  (= 5 a2) (= 5 b2) (= 5 c2) (= 5 d2) (= 5 e2) (= 5 f2) (= 5 g2) )
:assumption (or  (= 6 a2) (= 6 b2) (= 6 c2) (= 6 d2) (= 6 e2) (= 6 f2) (= 6 g2) )
:assumption (or  (= 7 a2) (= 7 b2) (= 7 c2) (= 7 d2) (= 7 e2) (= 7 f2) (= 7 g2) )
:assumption (or  (= 1 a3) (= 1 b3) (= 1 c3) (= 1 d3) (= 1 e3) (= 1 f3) (= 1 g3) )
:assumption (or  (= 2 a3) (= 2 b3) (= 2 c3) (= 2 d3) (= 2 e3) (= 2 f3) (= 2 g3) )
:assumption (or  (= 3 a3) (= 3 b3) (= 3 c3) (= 3 d3) (= 3 e3) (= 3 f3) (= 3 g3) )
:assumption (or  (= 4 a3) (= 4 b3) (= 4 c3) (= 4 d3) (= 4 e3) (= 4 f3) (= 4 g3) )
:assumption (or  (= 5 a3) (= 5 b3) (= 5 c3) (= 5 d3) (= 5 e3) (= 5 f3) (= 5 g3) )
:assumption (or  (= 6 a3) (= 6 b3) (= 6 c3) (= 6 d3) (= 6 e3) (= 6 f3) (= 6 g3) )
:assumption (or  (= 7 a3) (= 7 b3) (= 7 c3) (= 7 d3) (= 7 e3) (= 7 f3) (= 7 g3) )
:assumption (or  (= 1 a4) (= 1 b4) (= 1 c4) (= 1 d4) (= 1 e4) (= 1 f4) (= 1 g4) )
:assumption (or  (= 2 a4) (= 2 b4) (= 2 c4) (= 2 d4) (= 2 e4) (= 2 f4) (= 2 g4) )
:assumption (or  (= 3 a4) (= 3 b4) (= 3 c4) (= 3 d4) (= 3 e4) (= 3 f4) (= 3 g4) )
:assumption (or  (= 4 a4) (= 4 b4) (= 4 c4) (= 4 d4) (= 4 e4) (= 4 f4) (= 4 g4) )
:assumption (or  (= 5 a4) (= 5 b4) (= 5 c4) (= 5 d4) (= 5 e4) (= 5 f4) (= 5 g4) )
:assumption (or  (= 6 a4) (= 6 b4) (= 6 c4) (= 6 d4) (= 6 e4) (= 6 f4) (= 6 g4) )
:assumption (or  (= 7 a4) (= 7 b4) (= 7 c4) (= 7 d4) (= 7 e4) (= 7 f4) (= 7 g4) )
:assumption (or  (= 1 a5) (= 1 b5) (= 1 c5) (= 1 d5) (= 1 e5) (= 1 f5) (= 1 g5) )
:assumption (or  (= 2 a5) (= 2 b5) (= 2 c5) (= 2 d5) (= 2 e5) (= 2 f5) (= 2 g5) )
:assumption (or  (= 3 a5) (= 3 b5) (= 3 c5) (= 3 d5) (= 3 e5) (= 3 f5) (= 3 g5) )
:assumption (or  (= 4 a5) (= 4 b5) (= 4 c5) (= 4 d5) (= 4 e5) (= 4 f5) (= 4 g5) )
:assumption (or  (= 5 a5) (= 5 b5) (= 5 c5) (= 5 d5) (= 5 e5) (= 5 f5) (= 5 g5) )
:assumption (or  (= 6 a5) (= 6 b5) (= 6 c5) (= 6 d5) (= 6 e5) (= 6 f5) (= 6 g5) )
:assumption (or  (= 7 a5) (= 7 b5) (= 7 c5) (= 7 d5) (= 7 e5) (= 7 f5) (= 7 g5) )
:assumption (or  (= 1 a6) (= 1 b6) (= 1 c6) (= 1 d6) (= 1 e6) (= 1 f6) (= 1 g6) )
:assumption (or  (= 2 a6) (= 2 b6) (= 2 c6) (= 2 d6) (= 2 e6) (= 2 f6) (= 2 g6) )
:assumption (or  (= 3 a6) (= 3 b6) (= 3 c6) (= 3 d6) (= 3 e6) (= 3 f6) (= 3 g6) )
:assumption (or  (= 4 a6) (= 4 b6) (= 4 c6) (= 4 d6) (= 4 e6) (= 4 f6) (= 4 g6) )
:assumption (or  (= 5 a6) (= 5 b6) (= 5 c6) (= 5 d6) (= 5 e6) (= 5 f6) (= 5 g6) )
:assumption (or  (= 6 a6) (= 6 b6) (= 6 c6) (= 6 d6) (= 6 e6) (= 6 f6) (= 6 g6) )
:assumption (or  (= 7 a6) (= 7 b6) (= 7 c6) (= 7 d6) (= 7 e6) (= 7 f6) (= 7 g6) )
:assumption (or  (= 1 a7) (= 1 b7) (= 1 c7) (= 1 d7) (= 1 e7) (= 1 f7) (= 1 g7) )
:assumption (or  (= 2 a7) (= 2 b7) (= 2 c7) (= 2 d7) (= 2 e7) (= 2 f7) (= 2 g7) )
:assumption (or  (= 3 a7) (= 3 b7) (= 3 c7) (= 3 d7) (= 3 e7) (= 3 f7) (= 3 g7) )
:assumption (or  (= 4 a7) (= 4 b7) (= 4 c7) (= 4 d7) (= 4 e7) (= 4 f7) (= 4 g7) )
:assumption (or  (= 5 a7) (= 5 b7) (= 5 c7) (= 5 d7) (= 5 e7) (= 5 f7) (= 5 g7) )
:assumption (or  (= 6 a7) (= 6 b7) (= 6 c7) (= 6 d7) (= 6 e7) (= 6 f7) (= 6 g7) )
:assumption (or  (= 7 a7) (= 7 b7) (= 7 c7) (= 7 d7) (= 7 e7) (= 7 f7) (= 7 g7) )
:assumption (or  (= 1 a1) (= 1 a2) (= 1 a3) (= 1 a4) (= 1 a5) (= 1 a6) (= 1 a7) )
:assumption (or  (= 2 a1) (= 2 a2) (= 2 a3) (= 2 a4) (= 2 a5) (= 2 a6) (= 2 a7) )
:assumption (or  (= 3 a1) (= 3 a2) (= 3 a3) (= 3 a4) (= 3 a5) (= 3 a6) (= 3 a7) )
:assumption (or  (= 4 a1) (= 4 a2) (= 4 a3) (= 4 a4) (= 4 a5) (= 4 a6) (= 4 a7) )
:assumption (or  (= 5 a1) (= 5 a2) (= 5 a3) (= 5 a4) (= 5 a5) (= 5 a6) (= 5 a7) )
:assumption (or  (= 6 a1) (= 6 a2) (= 6 a3) (= 6 a4) (= 6 a5) (= 6 a6) (= 6 a7) )
:assumption (or  (= 7 a1) (= 7 a2) (= 7 a3) (= 7 a4) (= 7 a5) (= 7 a6) (= 7 a7) )
:assumption (or  (= 1 b1) (= 1 b2) (= 1 b3) (= 1 b4) (= 1 b5) (= 1 b6) (= 1 b7) )
:assumption (or  (= 2 b1) (= 2 b2) (= 2 b3) (= 2 b4) (= 2 b5) (= 2 b6) (= 2 b7) )
:assumption (or  (= 3 b1) (= 3 b2) (= 3 b3) (= 3 b4) (= 3 b5) (= 3 b6) (= 3 b7) )
:assumption (or  (= 4 b1) (= 4 b2) (= 4 b3) (= 4 b4) (= 4 b5) (= 4 b6) (= 4 b7) )
:assumption (or  (= 5 b1) (= 5 b2) (= 5 b3) (= 5 b4) (= 5 b5) (= 5 b6) (= 5 b7) )
:assumption (or  (= 6 b1) (= 6 b2) (= 6 b3) (= 6 b4) (= 6 b5) (= 6 b6) (= 6 b7) )
:assumption (or  (= 7 b1) (= 7 b2) (= 7 b3) (= 7 b4) (= 7 b5) (= 7 b6) (= 7 b7) )
:assumption (or  (= 1 c1) (= 1 c2) (= 1 c3) (= 1 c4) (= 1 c5) (= 1 c6) (= 1 c7) )
:assumption (or  (= 2 c1) (= 2 c2) (= 2 c3) (= 2 c4) (= 2 c5) (= 2 c6) (= 2 c7) )
:assumption (or  (= 3 c1) (= 3 c2) (= 3 c3) (= 3 c4) (= 3 c5) (= 3 c6) (= 3 c7) )
:assumption (or  (= 4 c1) (= 4 c2) (= 4 c3) (= 4 c4) (= 4 c5) (= 4 c6) (= 4 c7) )
:assumption (or  (= 5 c1) (= 5 c2) (= 5 c3) (= 5 c4) (= 5 c5) (= 5 c6) (= 5 c7) )
:assumption (or  (= 6 c1) (= 6 c2) (= 6 c3) (= 6 c4) (= 6 c5) (= 6 c6) (= 6 c7) )
:assumption (or  (= 7 c1) (= 7 c2) (= 7 c3) (= 7 c4) (= 7 c5) (= 7 c6) (= 7 c7) )
:assumption (or  (= 1 d1) (= 1 d2) (= 1 d3) (= 1 d4) (= 1 d5) (= 1 d6) (= 1 d7) )
:assumption (or  (= 2 d1) (= 2 d2) (= 2 d3) (= 2 d4) (= 2 d5) (= 2 d6) (= 2 d7) )
:assumption (or  (= 3 d1) (= 3 d2) (= 3 d3) (= 3 d4) (= 3 d5) (= 3 d6) (= 3 d7) )
:assumption (or  (= 4 d1) (= 4 d2) (= 4 d3) (= 4 d4) (= 4 d5) (= 4 d6) (= 4 d7) )
:assumption (or  (= 5 d1) (= 5 d2) (= 5 d3) (= 5 d4) (= 5 d5) (= 5 d6) (= 5 d7) )
:assumption (or  (= 6 d1) (= 6 d2) (= 6 d3) (= 6 d4) (= 6 d5) (= 6 d6) (= 6 d7) )
:assumption (or  (= 7 d1) (= 7 d2) (= 7 d3) (= 7 d4) (= 7 d5) (= 7 d6) (= 7 d7) )
:assumption (or  (= 1 e1) (= 1 e2) (= 1 e3) (= 1 e4) (= 1 e5) (= 1 e6) (= 1 e7) )
:assumption (or  (= 2 e1) (= 2 e2) (= 2 e3) (= 2 e4) (= 2 e5) (= 2 e6) (= 2 e7) )
:assumption (or  (= 3 e1) (= 3 e2) (= 3 e3) (= 3 e4) (= 3 e5) (= 3 e6) (= 3 e7) )
:assumption (or  (= 4 e1) (= 4 e2) (= 4 e3) (= 4 e4) (= 4 e5) (= 4 e6) (= 4 e7) )
:assumption (or  (= 5 e1) (= 5 e2) (= 5 e3) (= 5 e4) (= 5 e5) (= 5 e6) (= 5 e7) )
:assumption (or  (= 6 e1) (= 6 e2) (= 6 e3) (= 6 e4) (= 6 e5) (= 6 e6) (= 6 e7) )
:assumption (or  (= 7 e1) (= 7 e2) (= 7 e3) (= 7 e4) (= 7 e5) (= 7 e6) (= 7 e7) )
:assumption (or  (= 1 f1) (= 1 f2) (= 1 f3) (= 1 f4) (= 1 f5) (= 1 f6) (= 1 f7) )
:assumption (or  (= 2 f1) (= 2 f2) (= 2 f3) (= 2 f4) (= 2 f5) (= 2 f6) (= 2 f7) )
:assumption (or  (= 3 f1) (= 3 f2) (= 3 f3) (= 3 f4) (= 3 f5) (= 3 f6) (= 3 f7) )
:assumption (or  (= 4 f1) (= 4 f2) (= 4 f3) (= 4 f4) (= 4 f5) (= 4 f6) (= 4 f7) )
:assumption (or  (= 5 f1) (= 5 f2) (= 5 f3) (= 5 f4) (= 5 f5) (= 5 f6) (= 5 f7) )
:assumption (or  (= 6 f1) (= 6 f2) (= 6 f3) (= 6 f4) (= 6 f5) (= 6 f6) (= 6 f7) )
:assumption (or  (= 7 f1) (= 7 f2) (= 7 f3) (= 7 f4) (= 7 f5) (= 7 f6) (= 7 f7) )
:assumption (or  (= 1 g1) (= 1 g2) (= 1 g3) (= 1 g4) (= 1 g5) (= 1 g6) (= 1 g7) )
:assumption (or  (= 2 g1) (= 2 g2) (= 2 g3) (= 2 g4) (= 2 g5) (= 2 g6) (= 2 g7) )
:assumption (or  (= 3 g1) (= 3 g2) (= 3 g3) (= 3 g4) (= 3 g5) (= 3 g6) (= 3 g7) )
:assumption (or  (= 4 g1) (= 4 g2) (= 4 g3) (= 4 g4) (= 4 g5) (= 4 g6) (= 4 g7) )
:assumption (or  (= 5 g1) (= 5 g2) (= 5 g3) (= 5 g4) (= 5 g5) (= 5 g6) (= 5 g7) )
:assumption (or  (= 6 g1) (= 6 g2) (= 6 g3) (= 6 g4) (= 6 g5) (= 6 g6) (= 6 g7) )
:assumption (or  (= 7 g1) (= 7 g2) (= 7 g3) (= 7 g4) (= 7 g5) (= 7 g6) (= 7 g7) )
:assumption (= 4 (+ d2 d3))
:assumption (= 5 (+ d7 e7))
:assumption (= 7 (+ a1 b1))
:assumption (= 8 (+ a6 a7))
:assumption (= 12 (+ b2 c2 d2))
:assumption (= 13 (+ c6 c7))
:assumption (= 3 (+ g5 g6))
:assumption (= 7 (+ c1 c2 c3))
:assumption (= 8 (+ f6 f7))
:assumption (= 12 (+ g1 g2 g3))
:assumption (= 13 (+ e2 e3))
:assumption (= 14 (+ b4 b5 b6 b7))
:assumption (= 16 (+ a4 b4 c4 d4))
:assumption (= 17 (+ a6 b6 c6))
:formula true
)

magic_squares_solution.txt

sat
1.44
a1 = 5
b1 = 2
c1 = 1
d1 = 6
e1 = 4
f1 = 7
g1 = 3
a2 = 3
b2 = 7
c2 = 4
d2 = 1
e2 = 6
f2 = 2
g2 = 5
a3 = 1
b3 = 5
c3 = 2
d3 = 3
e3 = 7
f3 = 6
g3 = 4
a4 = 7
b4 = 1
c4 = 3
d4 = 5
e4 = 2
f4 = 4
g4 = 6
a5 = 4
b5 = 6
c5 = 5
d5 = 7
e5 = 3
f5 = 1
g5 = 2
a6 = 6
b6 = 4
c6 = 7
d6 = 2
e6 = 5
f6 = 3
g6 = 1
a7 = 2
b7 = 3
c7 = 6
d7 = 4
e7 = 1
f7 = 5
g7 = 7