5

私の状況

私は次のことが必要なプロジェクトに取り組んでいます。

  • 行列演算を含む3D 行列変換式の正しさを証明する
  • 未知の行列エントリの値を持つモデルを見つけます。

私の質問

  • で解くことができるように、行列演算を使用して式を表現する最良の方法は何z3ですか? ( Z3Py の Sudoku Exampleで使用されている方法はあまり洗練されておらず、より複雑な行列演算には適していないようです。)

ありがとう。- 何か不明な点がありましたら、質問コメントを残してください。

4

1 に答える 1

3

Z3 はこのような行列をサポートしていないため、それらをエンコードする最良の方法は、それらが表す式をエンコードすることです。これは、数独の例で物事をエンコードする方法とほぼ同じです。たとえば、2x2 の実数行列を使用した簡単な例を次に示します (Z3py リンク: http://rise4fun.com/Z3Py/MYnB ):

# nonlinear version, constants a_ij, b_i are variables
# x_1, x_2, a_11, a_12, a_21, a_22, b_1, b_2 = Reals('x_1 x_2 a_11 a_12 a_21 a_22 b_1 b_2')

# linear version (all numbers are defined values)
x_1, x_2 = Reals('x_1 x_2')

# A matrix
a_11 = 1
a_12 = 2
a_21 = 3
a_22 = 5

# b-vector
b_1 = 7
b_2 = 11

newx_1 = a_11 * x_1 + a_12 * x_2 + b_1
newx_2 = a_21 * x_1 + a_22 * x_2 + b_2

print newx_1
print newx_2

# solve using model generation
s = Solver()
s.add(newx_1 == 0) # pointers to equations
s.add(newx_2 == 5)
print s.check()
print s.model()

# solve using "solve"
solve(And(newx_1 == 0, newx_2 == 5))

Z3 で未知の行列エンティティを解決するには、2 行目のコメントを外し (a_11、a_12 などの記号名を使用)、5 行目の x_1、x_2 のその他の記号定義をコメント化し、a_11 への特定の割り当てをコメント化します。 = 1 など。次に、これらの変数への満足のいく割り当てを見つけることで、Z3 に未知数を解決させます。または x_i 変数。例: Z3 4.0: get complete modelを参照)。

ただし、共有したリンクに基づいて、一般的に超越的な正弦波 (回転) を使用した操作の実行に関心があり、この時点で Z3 は超越 (一般指数など) をサポートしていません。これは、たとえば、操作が機能する回転の角度の選択を証明したり、回転を単にエンコードしたりすることなど、あなたにとって難しい部分です。スケーリングと変換は、エンコードが難しくなりすぎないようにする必要があります。

また、線形微分方程式をエンコードする方法については、次の回答を参照してください。これは、x' = Ax の形式の方程式です。ここで、A は n * n 行列で、x は n 次元ベクトルです。注文式

于 2013-03-24T14:18:45.157 に答える