1

私の例：連立方程式

擬似コード制約ベース 
  a = b+c
∧ e = a*c

∧ a = +2     ; some replaceable concrete values
∧ c = +18
解決 
  b = -16
∧ e = -32

欲しい情報

連立方程式で、私は次の知識を得たいと思います。

与えられた値（制約ベース内）から変数値（解）を計算するために使用できる抽象的な式。

（高校のように、教師は結果を見たいだけでなく、そのような変換された抽象的な数式も望んでいました。）

のような式... 
  b = a-c     ; is an equivalent transformation from `a = b+c`
∧ e = (a-c)*c ; is an term replacement `b → a-c` of `e = a*c`

私の質問

Z3Pyを使用して、Z3制約連立方程式からこの情報を取得するにはどうすればよいですか？

ありがとう。-不明な点がある場合は、何が問題なのかコメントしてください。

4

1 に答える 1

5

Z3 は、この種の情報を抽出するための理想的なツールではありません。内部的には、特定のケースでこの種の機能を実装するのに役立つモジュール (ガウス消去法、Groebner Basisなど) がありますが、Z3 API では公開されていません。 Z3 のソース コードはオンラインで入手できます。

あなたが説明した問題は興味深いものですが、自明ではありません。一般に、入力は単なる方程式のセットではありません。さらに、方程式しかなくても、それらが非線形である場合、質問で説明されているような「解決された」形式を取得できない場合があります。非線形の場合、方程式を三角形の形にすることもできますが、それだけです。もう 1 つの問題は、解の数が有限であっても、線形の場合のように一意ではないことです。さらに、一般に、方程式の非線形集合の解は根号を使用して表現することはできません。内部的には、Z3 は解を表すために実代数を使用します。

于 2013-03-01T03:21:36.920 に答える