Z3 Python 检查对是否不同

Question

我有 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 对整数是否不同？如果不是，什么是启用上述对不同的约束的好方法？

Answer 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 个约束。

Z3 Python 检查对是否不同

Z3 Python Check whether pairs are distinct

python

z3

z3py