Блог

У меня есть 2 матрицы, каждая из которых 3 на 3 (назовем их M1 и M2, каждая из их записей имеет тип Int в Z3. Мне нужно добавить ограничение, в котором говорится, что все пары формы ([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(массив), но, похоже, это не работает, так как я получаю сообщение об ошибке

«По крайней мере один из аргументов должен быть выражением Z3»

Есть ли способ проверить, различны ли 2 пары целых чисел в Z3 для Python? И если нет, то каков хороший способ включить ограничение, что пары, описанные выше, различны?

Что-то вроде этого?

 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)  

Ограничения для попарного неравенства добавляются в четырехкратном вложенном цикле. Для матриц 3×3 это приводит к 81 ограничению.