매트릭스를 정의하는 방법은 무엇입니까?

Question

Microsoft는 "Rise4Fun"웹 사이트와 z3 파이썬 자습서 더 이상로드되지 않습니다.

어떻게 python을 위해 z3에서 매트릭스를 정의하고 그 위에 어떤 제약 조건을 부과 할 수 있습니까?

Answer 1

하나의 예 : 9x9 정수 변수의 매트릭스

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

.

예 : Matrix x

의 일부 제약 조건

cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9) 
         for i in range(9) for j in range(9) ]

.