Python Z3环境下marvellous square网格约束编写问题

前置变量声明 #

你需要先定义求和目标值t为Z3整数变量：

from z3 import *
t = Int("t")

行和约束 #

直接遍历每一行，对整行元素求和等于t即可，列表推导式写法简洁直观：

conditionRow = [ Sum(row) == t for row in aGrid ]

列和约束 #

外层遍历列索引，内层取所有行对应列的元素求和：

conditionCol = [ Sum([aGrid[i][j] for i in range(n)]) == t for j in range(n) ]

对角线和约束 #

分别对两条对角线的元素求和，不需要多层循环：

conditionDiag = [
    # 左上到右下对角线：行索引等于列索引
    Sum([aGrid[i][i] for i in range(n)]) == t,
    # 右上到左下对角线：行索引 + 列索引 = n-1
    Sum([aGrid[i][n - 1 - i] for i in range(n)]) == t
]

补充优化提示 #

你当前的conditionOne仅限制了元素取值在1~n²区间，若要满足「填充1到n²所有整数」的规则，还需要补充去重约束，避免重复值出现：

conditionDistinct = [ Distinct([aGrid[i][j] for i in range(n) for j in range(n)]) ]

约束合并使用 #

将所有约束传入求解器即可开始求解：

solver = Solver()
solver.add(conditionOne + conditionRow + conditionCol + conditionDiag + conditionDistinct)
# 求解示例
if solver.check() == sat:
    print(solver.model())

内容的提问来源于stack exchange，提问作者Oluwasayo