4

数量詞について質問があります。

配列があり、この配列の配列インデックス0、1、2を計算したいとします-

(declare-const cpuA (Array Int Int))
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1)))

または、forall構文を使用して-と同じものを指定できます

(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1)))))

ここで、2つの違いを理解したいと思います。最初のメソッドはすばやく実行され、シンプルで読みやすいモデルを提供します。対照的に、2番目のオプションを使用したコードサイズは非常に小さくなりますが、プログラムの実行には時間がかかります。また、ソリューションは複雑です。

コードが小さくなるので、2番目の方法を使用したいと思います。しかし、読みやすいシンプルなモデルを見つけたいと思います。

4

1 に答える 1

4

数量詞の推論は通常、非常に費用がかかります。あなたの例では、定量化された式は、あなたが提供した3つのアサーションと同等です。ただし、それはZ3が数式を決定/解決する方法ではありません。Z3は、モデルベースの数量詞インスタンス化（MBQI）と呼ばれる手法を使用して数式を解きます。この手法では、多くのフラグメントを決定できます（http://rise4fun.com/Z3/tutorial/guideを参照））。これは主に、このガイドで説明されているフラグメントに効果的です。未解釈の関数、算術およびビットベクトル理論をサポートします。また、配列とデータ型のサポートも制限されています。これはあなたの例を解くのに十分です。同じエンジンを使用してより複雑なフラグメントを決定するため、Z3によって生成されたモデルはより複雑に見えます。モデルは小さな関数型プログラムのように見えるはずです。このアプローチがどのように機能するかについての詳細は、次の記事を参照してください。

配列理論は、主に無制限または大きな配列を表現/モデリングするのに役立ちます。つまり、配列の実際のサイズが不明であるか、大きすぎます。大きな意味で、数式内の配列アクセスの数（つまり、selects）は、配列の実際のサイズよりもはるかに少ないことを意味します。「問題Xをモデル化/解決するために本当に配列が必要なのか」と自問する必要があります。次の代替案を検討できます。

  • （未解釈）配列の代わりに関数。あなたの例は次のようにエンコードすることもできます：

    （declare-fun cpuA（Int）Int）

    （assert（or（=（cpuA 0）0）（=（cpuA 0）1）））
    （assert（or（=（cpuA 1）0）（=（cpuA 1）1）））
    （assert（or（= （cpuA 2）0）（=（cpuA 2）1）））

  • プログラマティックAPI。コンパクトなエンコーディングを提供するために配列（および関数）が使用される多くの例を見てきました。コンパクトでエレガントなエンコーディングは、必ずしも簡単に解決できるとは限りません。実際には、通常はその逆です。Z3用のプログラムAPIを使用して、両方の長所（パフォーマンスとコンパクトさ）を実現できます。次のリンクでは、「配列」の位置ごとに1つの「変数」を使用して例をエンコードしました。マクロ/関数は、次のような制約をエンコードするために使用されます。式はa0または1。 http://rise4fun.com/Z3Py/JF

于 2012-04-05T21:02:33.260 に答える