1

Z3 の実数を使用してエンコードされた問題を考えるとZ3 /smt2 /st、実数エンジンに「問題がある/多くの作業を行う」かどうかを判断するために、生成される統計のどれが役立つでしょうか?

私の場合、問題の 2 つのほぼ同等のエンコーディングがあり、どちらも実数を使用しています。ただし、エンコーディングの「小さな」違いは、実行時間に大きな違いをもたらします。つまり、エンコーディング A は 2:30 分、エンコーディング B は 13 分かかります。Z3 の統計によるとconflicts、 とquant-instantiationsはほぼ同等ですが、 と など、他のものはそうではありませgrobnerん。pivotsnonlinear-horner

2 つの異なる統計がgistとして利用可能です。


編集（レオのコメントに対処するため）：

両方のバージョンで生成される SMT2 エンコーディングは約 3 万行で、実数が使用されるアサーションがコード全体に散りばめられています。主な違いは、エンコーディング B では、不等式によって境界付けられた範囲0.0からの範囲の指定されていない実数型の定数が多数使用されることです。 、または。両方のエンコーディングは、非線形実数演算を使用します。1.00.0 < r1 < 1.00.0 < r3 < 0.75 - r1 - r20.10.75 - 0.01r1 * (1.0 - r2)

2 つのエンコーディングからのいくつかのランダムな例がgistとして利用可能です。上で説明したように、発生するすべての変数は指定されていない実数です。


PS: 固定実数値のエイリアスを導入します。たとえば、

(define-sort $Perms () Real)
(declare-const $Perms.$Full $Perms)
(declare-const $Perms.$None $Perms)
(assert (= $Perms.Zero 0.0))
(assert (= $Perms.Write 1.0))

パフォーマンスに重大なペナルティを課しますか?

4

1 に答える 1

5

新しい非線形算術ソルバーは、算術のみを含む問題でのみ使用されます。問題は量化子を使用しているため、新しい非線形ソルバーは使用されません。したがって、Z3 は、Simplex (pivots stat)、Groebner Basis (groebner stat)、および Interval Propagation (horner stat) の組み合わせに基づく古いアプローチを使用します。これは完全な方法ではありません。さらに、Gist に投稿したフラグメントに基づいて、Groebner の基礎はあまり効果的ではありません。この方法は通常、多くの等式を含む問題で効果的です。したがって、それはおそらく単なるオーバーヘッドです。オプションを使用して無効にすることができますNL_ARITH_GB=false。もちろん、これはあなたが投稿した問題の断片に基づく単なる推測です。

Aエンコーディングとの違いBはかなりのものです。Aいくつかの定数が実際の値に固定されているため、エンコードは本質的に線形の問題です。Z3 は、線形算術の問題に対して常に完全でした。したがって、これはパフォーマンスの違いを説明するはずです。

エイリアスに関する質問に関しては、エイリアスを導入するための推奨される方法は次のとおりです。

(define-const $Perms.$Zero $Perms 0.0)
(define-const $Perms.$Write $Perms 1.0)

Z3 には、線形方程式を使用して変数を消去するプリプロセッサも含まれています。このプリプロセッサは、量指定子を含む問題ではデフォルトで無効になっています。この設計上の決定は、量指定子のトリガー/パターンを広範に使用するプログラム検証ツールによって動機付けられています。変数除去プロセスは、慎重に設計されたトリガー/パターンを変更し、合計実行時間に影響を与える可能性があります。Z3 の新しい戦術/戦略フレームワークを使用して、このプリプロセッサを強制的に適用できます。コマンドを置き換えることができます

(check-sat)

と

(check-sat-using (then simplify solve-eqs smt))

この戦略は、Z3 に単純化を実行し、方程式を解いて (変数を削除して)、デフォルトのソルバー エンジンを実行するように指示していますsmt。戦術と戦略の詳細については、次のチュートリアルを参照してください。

于 2012-06-11T15:09:10.780 に答える