9

私は、算術、数量詞、平等の理論を組み合わせたZ3を実験しています。これはあまり効率的ではないようです。実際、可能な場合は、数量詞をすべてのインスタンス化された地上インスタンスに置き換える方が効率的であるようです。f次の例を考えてみましょう。この例では、sortの2つの引数を取りObj、解釈されたsortを返す関数の一意の名前の公理をエンコードしましたS。この公理は、引数の各一意のリストがf一意のオブジェクトを返すことを示しています。

(declare-datatypes () ((Obj o1 o2 o3 o4 o5 o6 o7 o8)))
(declare-sort S 0)

(declare-fun f (Obj Obj) S)
(assert (forall ((o11 Obj) (o12 Obj) (o21 Obj) (o22 Obj))
    (=> 
        (not (and (= o11 o21) (= o12 o22)))
        (not (= (f o11 o12) (f o21 o22))))))

これはロジックでそのような公理を定義する標準的な方法ですが、このように実装すると計算コストが非常に高くなります。これには4つの定量化された変数が含まれ、それぞれが8つの値を持つことができます。これは、これが8^4 = 4096平等になることを意味します。これを証明するには、Z30.69sと2016年の数量詞のインスタンス化が必要です。この式のインスタンスを生成する簡単なスクリプトを書くと、次のようになります。

(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8)))

これらの公理を生成するのに0.002秒かかり、Z3でそれを証明するのにさらに0.01秒（またはそれ以下）かかります。定義域内のオブジェクト、または関数への引数の数をf増やすと、この違いは急速に増加し、定量化されたケースはすぐに実行不可能になります。

これは私に不思議に思います：私たちが有界ドメインを持っているとき、なぜ私たちはそもそもZ3で数量詞を使うのでしょうか？SMTはヒューリスティックを使用して解決策を見つけることを知っていますが、接地されたインスタンスをSMTにフィードする単純なドメイン固有のグラウンダーと効率的に競合することはできないと感じています。これはSATの解決にすぎません。私の直感は正しいですか？

4

1 に答える 1

7

あなたの直感は正しいです。Z3で数量詞を処理するためのヒューリスティックは、ユニバーサル変数が有限/有界ドメインに及ぶ問題に合わせて調整されていません。この種の問題では、問題が満たされないことを示すために必要なインスタンスの割合が非常に少ない場合にのみ、数量詞を使用することをお勧めします。

私は通常、ユーザーがプログラマティックAPIを使用してこの数量詞を拡張することをお勧めします。ここに2つの関連する投稿があります。これらには、このアプローチを実装するPythonコードへのリンクが含まれています。

コードフラグメントの1つは次のとおりです。

VFunctionAt = Function('VFunctionAt', IntSort(), IntSort(), IntSort())

s = Solver()
s.add([VFunctionAt(V,S) >= 0 for V in range(1, 5) for S in range(1, 9)])
print s

この例では、基本的にをエンコードしてforall V in [1,4] S in [1,8] VFunctionAt(V,S) >= 0います。

最後に、エンコーディング(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8))は、数量詞を4096倍に拡張するよりもはるかにコンパクトです。ただし、単純なエンコーディングを使用する場合でも（数量詞を4096回拡張するだけ）、拡張バージョンを解決する方がはるかに高速です。

于 2012-11-07T14:42:55.003 に答える