Z3 Python 检查对是否不同答案

【问题标题】：Z3 Python Check whether pairs are distinctZ3 Python 检查对是否不同
【发布时间】：2021-10-31 20:03:17
【问题描述】：

我有 2 个矩阵，每个矩阵都是 3 x 3（称它们为 M1 和 M2，它们的每个条目都是 Z3 中的 Int 类型。我需要添加表示所有形式对的约束（[M1 [i][j], M2[i][j]) 是不同的（i 和 j 是矩阵的任意索引）。

换句话说，

if   (i1,j1) != (i2,j2) 
then ([M1[i1][j1], M2[i1][j1]) != ([M1[i2][j2], M2[i1][j2])

我尝试创建一个包含所有对的数组，称为数组，然后使用 Distinct(array)，但这似乎不起作用，因为我收到一个错误提示

“至少有一个参数必须是 Z3 表达式”

有没有办法在 Python 的 Z3 中查看 2 对整数是否不同？如果不是，什么是启用上述对不同的约束的好方法？

【问题讨论】：

标签： python z3 z3py

【解决方案1】：

这样的？

from z3 import *

def CreateMatrix(name, rows, cols):
    a=[] 
    for row in range(rows): 
        b=[]
        for col in range(cols): 
            v = Int(name + str(row+1) + str(col+1))
            b.append(v)
        a.append(b)
    return a

def ShowMatrix(model, name, mat, rows, cols):
    print()
    print("Matrix " + name)
    for row in range(rows):
        s = ""
        for col in range(cols):
            s = s + str(model.eval(mat[row][col])).ljust(4)
        print(s)

s = Solver()
rows = 3
cols = 3
M1 = CreateMatrix('M1', rows, cols)
M2 = CreateMatrix('M2', rows, cols)

for row1 in range(rows):
    for col1 in range(cols):
        for row2 in range(rows):
            for col2 in range(cols):
                s.add(M1[row1][col1] != M2[row2][col2])

print(s.check())

ShowMatrix(s.model(), "M1", M1, rows, cols)
ShowMatrix(s.model(), "M2", M2, rows, cols)

成对不等式的约束被添加到四重嵌套循环中。对于 3x3 矩阵，这会产生 81 个约束。

【讨论】：

也可以通过 SMT-Arrays 对矩阵进行建模。但是您给出的编码更可取，因为 SMT 数组与人们通常认为的常规编程语言中的数组/矩阵并不完全匹配。
嘿，感谢您的回复，尽管我需要添加一些更宽松的约束，但这最终帮助我解决了这个问题。真的很感激