Search code examples
z3py

Creating associative magic squares z3 python

So Im working with magic squares. I've created conditions for a regular magic square. Now I need to add the constraints to make it associative.

I'm using the z3 python module. To be associative, the sum of the opposite numbers need to be equal to the same number 't'. the sum of all the rows and columns and diagonals need to be equal to this number t as well. So I'm struggling with accessing the numbers individually from each list in the list of lists.

enter image description here

For example, these are the constraints I have for a regular magic square:

t = Int('t')
  Square = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(n) ] for i in range(n) ]  
  distinct = [ Distinct([ Square[i][j] for i in range(n) for j in range(n) ]) ]
  cell = [ And(1 <= Square[i][j], Square[i][j] <= n**2) for i in range(n) for j in range(n) ]
  row = [(sum(Square[i]) == t) for i in range(n)]
  col = [(sum([Square[j][i] for j in range(n)]) == t) for i in range(n)]
  firstDiagonal = [ (sum([Square[i][i]  for i in range(n)]) == t) ]
  secondDiagonal = [ (sum([Square[n-i-1][i] for i in range(n)]) == t) ]

So how do I associative conditions?

Solution

  • I amended your model and added associative constraints:

    from z3 import *

def ShowSquare(model, square, rows, cols):
    print()
    print("Square")
    for row in range(rows):
        s = ""
        for col in range(cols):
            s = s + str(model.eval(square[row][col])).ljust(4)
        print(s)

s = Solver()

n = 3
t = Int('t')
 
magicSquare = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(n) ] for i in range(n) ]  
distinctConstraints = [ Distinct([ magicSquare[i][j] for i in range(n) for j in range(n) ]) ]
cellConstraints = [ And(1 <= magicSquare[i][j], magicSquare[i][j] <= n**2) for i in range(n) for j in range(n) ]
rowConstraints = [(sum(magicSquare[i]) == t) for i in range(n)]
colConstraints = [(sum([magicSquare[j][i] for j in range(n)]) == t) for i in range(n)]
firstDiagConstraints = [ (sum([magicSquare[i][i]  for i in range(n)]) == t) ]
secondDiagConstraints = [ (sum([magicSquare[n-i-1][i] for i in range(n)]) == t) ]

AssocSum = Int('AssocSum')
assocRowConstraints = [((magicSquare[0][i] + magicSquare[n-1][n-i-1]) == AssocSum) for i in range(n) ] 
assocColConstraints = [((magicSquare[i][0] + magicSquare[n-i-1][n-1]) == AssocSum) for i in range(1, n-1) ] 

# performance tweak
# the magic sum is known in advance
s.add(2*t == n*(n*n+1))

s.add(distinctConstraints)
s.add(cellConstraints)
s.add(rowConstraints)
s.add(colConstraints)
s.add(firstDiagConstraints)
s.add(secondDiagConstraints)
s.add(assocRowConstraints)
s.add(assocColConstraints)
print(s.check())
model = s.model()
print("magic sum %s" % model.eval(t))
print("assoc sum %s" % model.eval(AssocSum))
ShowSquare(model, magicSquare, n, n)

    The result is a transposed version of the Lo Shu Square linked in the question:

    sat
magic sum 15
assoc sum 10

Square
4   3   8   
9   5   1   
2   7   6

    For n=5, a solution is:

    magic sum 65
assoc sum 26

Square
8   7   12  15  23  
17  20  22  1   5   
16  2   13  24  10  
21  25  4   6   9   
3   11  14  19  18