python - 行列を定義する方法は?

Question

Microsoft が "rise4fun" Web サイトを完全に盗み、Z3 Python チュートリアルが読み込まれなくなったようです。

Z3 for Python で行列を定義し、それにいくつかの制約を課すにはどうすればよいですか?

Answer 1

一例: 整数変数の 9x9 行列

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

例: 行列 X のいくつかの制約

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