创建关联幻方 z3 python

Question

所以我正在使用幻方。我已经为一个普通的幻方创造了条件。现在我需要添加约束以使其具有关联性。

我正在使用 z3 python 模块。要结合，相反数字的总和需要等于相同的数字't'。所有行和列以及对角线的总和也需要等于这个数字 t。所以我很难从列表列表中的每个列表中单独访问数字。

例如，这些是我对常规幻方的约束：

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) ]

那我怎么关联条件呢？

Answer 1

我修改了你的模型并添加了关联约束：

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)

结果是问题中链接的 Lo Shu Square 的转置版本：

sat
magic sum 15
assoc sum 10

Square
4   3   8   
9   5   1   
2   7   6

对于n=5，一个解决方案是：

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

创建关联幻方 z3 python

Creating associative magic squares z3 python

z3py