Утверждение ограничения на умножение матрицы

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" 

Теперь, есть ли способ в понимании списка, посредством которого я могу утверждать матричное умножение? (Золь == х * у) ...?

Answer 1

Нет, Z3 не имеет встроенной функции для матричного умножения. Это все равно можно сделать простым способом, но ограничения могут стать довольно большими.