4

なぜ？

問題が発生するユースケースのコンテキスト

三角形のランダムなアイテムを 3 つ定義します。Microsoft Z3 は次のように出力する必要があります。

  • 制約が満たされているか、または無効な入力値がありますか?
  • すべての変数が具体的な値に割り当てられている他のすべての三角形アイテムのモデル。

項目を制約するために、assert等式を三角形にする必要があります。ピタゴラスの定理 ( (h_c² + p² = b²) ^ (h_c² + q² = a²)) から始めたかったのです。

問題

Microsoft Z3 には、非線形の算術問題を解決するための限られた機能しかないことを知っています。しかし、一部の手計算機でさえ、次のような非常に単純化されたバージョンを解決できます。

(set-option :print-success true)
(set-option :produce-proofs true)
(declare-const a Real)
(declare-const b Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert
    (exists
        ((c Real))
        (=
            (+
                (* a a)
                (* b b)
            )
            (* c c)
        )
    )
)
(check-sat)
(get-model)

質問

  • 2 つの値が指定されている場合、Microsoft Z3 でピタゴラスの定理を解く方法はありますか?
  • または: 非線形算術のこれらのケースを処理できる別の定理証明者はいますか?

ご協力ありがとうございます - 何か不明な点があれば、コメントしてください。

4

1 に答える 1

4

Z3 には、非線形演算用の新しいソルバー (nlsat) があります。他のソルバーよりも効率的です (この記事を参照してください)。新しいソルバーは、量指定子のない問題に対して完全です。ただし、新しいソルバーは証明の生成をサポートしていません。証明生成を無効にすると、Z3 は nlsat を使用して問題を簡単に解決します。あなたの質問に基づいて、あなたは本当に解決策を探しているようです。したがって、証明生成を無効にすることは問題ではないようです。

さらに、Z3 は (手計算機のように) 近似解を生成しません。実数の正確な表現を使用します。結果を 10 進表記で表示するように Z3 に依頼することもできます (オプション:pp-decimal)。 これがオンラインの例です。

この例では、正確な表現が使用されている場合、Z3 は に対して次の結果を表示しますc。

(root-obj (+ (^ x 2) (- 2)) 1)

それはc多項式の最初の根だと言っていx^2 - 2ます。を使用する(set-option :pp-decimal true)と、表示されます

(- 1.4142135623?)

疑問符は、結果が切り捨てられることを示すために使用されます。結果が負になることに注意してください。ただし、実際に投稿した問題の解決策です。三角形を探しているので、定数がすべて > 0 であると主張する必要があります。

ところで、存在量指定子は必要ありません。単純に定数を使用できますc。以下に例を示します ( rise4fun でもオンラインで入手できます)。

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert (> c 0))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
(get-model)

解決策がない別の例を次に示します ( rise4fun でオンラインでも入手できます)。

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> c 0))
(assert (> a c))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)

ところで、Z3 の Python インターフェイスを検討する必要があります。それははるかにユーザーフレンドリーです。リンクしたチュートリアルには、キネマティクスの例があります。また、非線形演算を使用して、単純な高校物理の問題をエンコードします。

于 2013-02-27T14:35:54.210 に答える