如何使用Python的z3库为关联幻方添加约束条件？

你要新增的中心对称对求和约束可以按坐标映射规则编写，n阶幻方中任意位置(i,j)对应的中心对称位置坐标为(n-1-i, n-1-j)，添加约束时注意避免重复配对即可。

新增约束代码 #

你可以直接在现有代码后添加以下代码段：

symmetric_constraint = []
for i in range(n):
    for j in range(n):
        # 仅对前半部分坐标加约束，避免重复配对
        if i < n - 1 - i or (i == n - 1 - i and j < n - 1 - j):
            symmetric_constraint.append(Square[i][j] + Square[n-1-i][n-1-j] == t)
        # 处理奇数阶幻方的中心单元格
        elif i == n - 1 - i and j == n - 1 - j:
            symmetric_constraint.append(2 * Square[i][j] == t)

约束使用说明 #

把生成的symmetric_constraint列表和你原有普通幻方的约束合并后传入z3求解器即可，完整的约束集合示例：

s = Solver()
s.add(distinct + cell + row + col + firstDiagonal + secondDiagonal + symmetric_constraint)

• 上述配对逻辑同时兼容奇数阶和偶数阶幻方，不会出现重复约束或者漏约束的问题
• 奇数阶幻方的中心单元格没有配对点，单独设置两倍值等于t，符合关联幻方的对称和规则

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