断言对矩阵乘法的约束

Question

我正在尝试通过使用 z3py API 断言对矩阵乘法的约束来评估结果矩阵。以下方法适用于矩阵加法。以下是代码，它有 3 个矩阵：x、y 和 sol。 sol 是 x 和 y 的加法（sol==x+y），我有兴趣将结果矩阵（sol）的值限制为零，并检查“x”和“y”中的哪些未知值产生结果矩阵为零。以下是加法的列表理解方法。

from z3 import*

x = [ [Real("x_%s_%s" %(i+1, j+1))  for j in range(2) ] for i in range(2)]
y = [ [Real("y_%s_%s" %(i+1, j+1))  for j in range(2) ] for i in range(2)]
sol = [ [Real("sol_%s_%s" %(i+1, j+1))  for j in range(2) ] for i in range(2)]
addition = [sol[i][j]==x[i][j]+y[i][j]   for i in range(2) for j in range(2) ]


s = Solver()

s.add(addition)
s.add(x[0][0]>=0)
s.add(x[0][1]>=0)
s.add(x[1][0]>=0)
s.add(x[1][1]>=1)

s.add(And(y[0][0]>=0, y[0][0]<=2))
s.add(And(y[0][1]>=0, y[0][0]<=2))
s.add(And(y[1][0]>=0, y[0][0]<=2))
s.add(And(y[1][1]>=0, y[0][0]<=2))

s.add(sol[0][0]==0)
s.add(sol[0][1]==0)
s.add(sol[1][0]==0)
s.add(sol[1][1]==0)


if s.check()==sat:
    m =s.model()
    print  SAT,'\n', m
    result=[[ m.evaluate(sol[i][j]) for i in range (2)] for j in range (2)]
    print result
if (s.check()==unsat):
    print "UNSAT, no model exists"

现在，列表理解中是否有任何方法可以断言矩阵乘法？ (sol==x*y)...？

Answer 1

不，Z3 没有内置的矩阵乘法函数。它仍然可以以直接的方式完成，但限制可能会变得非常大。