square_z3.py

from z3 import *

s = Solver()
thesum = 15

square = [[Int('x[{0}][{1}]'.format(i,j)) for j in range(3)] for i in range(3)]

# Each cell must be an int between 1 and 9
s.add([And(square[i][j] >= 1, square[i][j] <= 9) for i in range(3) for j in range(3)])

# Each cell must be unique number
s.add([Distinct([square[i][j] for i in range(3) for j in range(3)])])

# Each row must sum to thesum
s.add([(sum(square[i]) == thesum) for i in range(3)])

# Each col must sum to thesum
s.add([(sum([square[j][i] for j in range(3)]) == thesum) for i in range(3)])

# There are many solutions, just print a few

solutions = 10
models = []
while s.check() == sat and len(models) < solutions:
    models.append(s.model())

for model in models:
    for row in range(3):
        for col in range(3):
            print(str(model.eval(square[row][col])), end = ' ')
        print()

    print('--------')

square_z3_output.txt

2 4 9
6 8 1
7 3 5
--------
3 4 8
5 9 1
7 2 6
--------
3 4 8
5 9 1
7 2 6
--------
3 4 8
5 9 1
7 2 6
--------
2 4 9
6 8 1
7 3 5
--------
2 4 9
6 8 1
7 3 5
--------
3 4 8
5 9 1
7 2 6
--------
3 4 8
5 9 1
7 2 6
--------
3 4 8
5 9 1
7 2 6
--------
3 4 8
5 9 1
7 2 6
--------