z3 - 检查矩阵值函数的可满足性

Question

我正在尝试将 2 个 2*2 顺序的矩阵相乘。其中一个矩阵包含未知参数“k1”。我想检查一个令人满意的解决方案，即 k1 的值。两个矩阵的乘积将等于第三个矩阵。注意：我不想将乘法转换为线性关系或方程组，我想将其作为矩阵进行操作。

这是我卡住的地方。

k1 = Int ('k1')

x = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(2) ] 
     for i in range(2) ]

a =((1,k1),(3,4))

b =((1,1),(1,1))

c= ((3,3),(7,7))

s = Solver()
s.add(a[0][1]>0)
s.add(a*b==c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(x[i][j]) for j in range(2) ] 
      for i in range(2) ]
print_matrix(r)
else:
print "failed to solve"

有什么出路吗？

Answer 1

一种可能的解决方案是

k1 = Int ('k1')

x = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(2) ] 
 for i in range(2) ]

a =((1,k1),(3,4))

b =((1,1),(1,1))

c= ((3,3),(7,7))

s = Solver()
eq1= a[0][1]>0
eq2 =[[sum(a[i][k]*b[k][j] for k in range(2)) == c[i][j] for i in range(2) ]
         for j in range(2) ]
s.add(eq1)
s.add(eq2[0][0])
s.add(eq2[0][1])
s.add(eq2[1][0])
s.add(eq2[1][1])
print s             
print s.check()             
m = s.model()
print m

相应的输出是

[k1 > 0, 1 + k1*1 == 3, True, 1 + k1*1 == 3, True] 
sat 
[k1 = 2]

请在此处在线运行此示例