3

非線形の実数演算で一連の制約を生成するプログラムがあります。次の 2 つの制約を考慮してください。

(<(- (- (- (+ (* (- v0_x v3_x) (- v1_y v3_y) (+ (* (- v2_x v3_x) (- v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y)))))) (* (- v0_y v3_y) (- v2_x v3_x) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y)))) (* (- v1_x v3_x) ( - v2_y v3_y) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v1_y v3_y) (- v2_x v3_x) (+ ( * (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v0_y v3_y) (- v1_x v3_x) (+ (* (- v2_x v3_x) ( - v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y))))) (* (- v0_x v3_x) (- v2_y v3_y)(+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y))))) 0)

(>(- (- (- (+ (* (- v0_x v2_x) (- v1_y v2_y) (+ (* (- v3_x v2_x) (- v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y))))) (* (- v0_y v2_y) (- v3_x v2_x) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y)))) (* (- v1_x v2_x) ( - v3_y v2_y) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v1_y v2_y) (- v3_x v2_x) (+ ( * (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v0_y v2_y) (- v1_x v2_x) (+ (* (- v3_x v2_x) ( - v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y))))) (* (- v0_x v2_x) (- v3_y v2_y)(+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y))))) 0)

それらをZ3にアサートすると、それは満足できると言われますが、2番目の制約を(> ... 0)ではなく(< ... 0)に変更するとすぐに、満足できないはずです.z3は永遠に実行されます。非線形の実数演算を処理するための z3 の制限について疑問に思っています。Z3 が上記の制約を処理できる可能性はありますか?

4

1 に答える 1

4

はい、問題に変わる(< ... 0)と(> ... 0)は満足できなくなりp < 0 and p > 0ます。あなたの投稿の2つの多項式は、単純化後に同一です。しかし、Z3 はこの単純な証明を見逃しています。これは、次のリリースで修正される予定です。それまでの間、カスタム戦略を使用して、この種の単純な証明を持つ例を見つけることができます。

(check-sat-using (then (! simplify :som true) (! simplify :sort-sums true) smt))

p < 0この戦略は、多項式の正規化を行い、との矛盾を検出するエンジンを呼び出しますp > 0。サンプル全体は、http: //rise4fun.com/Z3/JP4でオンラインで入手できます。メッセージの最後にも貼り付けました。

Z3 は、短い/簡単な証明を見逃し、より高価で完全な方法を使用して証明を見つけようとするため、永遠に実行し続けます。Z3 で使用されるアルゴリズムは、ここで説明されています。このアルゴリズムは、部分結果に基づく射影演算子を使用します。この操作は非常に高価で、この例では非常に大きな多項式が生成されます。この手順は、それぞれに小さな変数セットを持つ小さな多項式を含む問題に適しています。将来的には、完全な手法と不完全な手法を組み合わせて、Z3 が妥当な時間内に解決できる一連の問題を改善する予定です。

(declare-const v0_x Real)
(declare-const v1_x Real)
(declare-const v2_x Real)
(declare-const v3_x Real)
(declare-const v4_x Real)
(declare-const v0_y Real)
(declare-const v1_y Real)
(declare-const v2_y Real)
(declare-const v3_y Real)
(declare-const v4_y Real)


(assert
(< (- (- (- (+ (* (- v0_x v3_x) (- v1_y v3_y) (+ (* (- v2_x v3_x) (- v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y)))) (* (- v0_y v3_y) (- v2_x v3_x) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y)))) (* (- v1_x v3_x) (- v2_y v3_y) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v1_y v3_y) (- v2_x v3_x) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v0_y v3_y) (- v1_x v3_x) (+ (* (- v2_x v3_x) (- v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y))))) (* (- v0_x v3_x) (- v2_y v3_y) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y))))) 0.0))

(assert
(< (- (- (- (+ (* (- v0_x v2_x) (- v1_y v2_y) (+ (* (- v3_x v2_x) (- v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y)))) (* (- v0_y v2_y) (- v3_x v2_x) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y)))) (* (- v1_x v2_x) (- v3_y v2_y) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v1_y v2_y) (- v3_x v2_x) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v0_y v2_y) (- v1_x v2_x) (+ (* (- v3_x v2_x) (- v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y))))) (* (- v0_x v2_x) (- v3_y v2_y) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y))))) 0.0))

(check-sat-using (then (! simplify :som true) (! simplify :sort-sums true) smt))
于 2012-12-04T21:48:35.057 に答える