数量Vs非数量

Question

数量器に関する質問があります。

私は配列を持っていると私は、この配列の配列インデックス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として構築使用して同じことを指定することができます -

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

私のコードが小さくなるので、私は2番目の方法を使いたいと思います。 しかし、わかりやすいシンプルなモデルを探したい。

Answer 1

通常、推論は非常に高価です。あなたの例では、数量化された数式は、あなたが提供した3つのアサーションに相当します。 しかし、これはZ3があなたの数式を決定/解決する方法ではありません。 Z3は、Model-Based Quantifier Instantiation（MBQI）という手法を使用して数式を解きます。 この手法では多くのフラグメントを決定できます（http://rise4fun.com/Z3/tutorial/guideを参照）。これは主に、このガイドで説明されているフラグメントに有効です。 未解釈関数、算術演算、ビットベクトル理論をサポートしています。配列やデータ型のサポートも限られています。 これはあなたの例を解決するのに十分です。同じエンジンがより複雑な断片を決定するため、Z3によって生成されるモデルはより複雑に見えます。 モデルは小さな機能プログラムのように見えるはずです。あなたは、このアプローチは、以下の記事でどのように機能するかについての詳細な情報を見つけることができます。配列の理論は/モデリング無制限かを表現するために、主に有用である、ということ

• Complete instantiation for quantified SMT formulas

• Efficiently Solving Quantified Bit-Vector Formula

注意を大きなアレイ。つまり、配列の実際のサイズは不明であるか、大きすぎます。 bigとは、数式の配列アクセスの数（つまり、selects）が配列の実際のサイズよりもはるかに小さいことを意味します。 「問題Xのモデリングや問題解決のための配列が本当に必要ですか？」

• （未解釈）の機能を配列の代わりに使用することもできます。

  （宣言する-楽しみをCPUA（INT）INT）

  （CPUA 0（=（アサート（または）0）（=（CPUA 0）1）））：あなたの例は、のようにも符号化することができます
  
  （）CPUA 1（=（0）（=（CPUA 1）1））をアサート（または）（0）（=（CPUA 2））CPUA 2（=（アサート（または1）））

• プログラマティックAPI。我々は、コンパクトなエンコーディングを提供するために配列（および関数）が使われる多くの例を見てきました。コンパクトでエレガントなエンコーディングは必ずしも簡単には解決できません。実際には、それは通常、他の方法です。Z3用のプログラム型APIを使用することで、両方の世界（パフォーマンスとコンパクトさ）を最大限に引き出すことができます。次のリンクでは、 "配列"の各位置に1つの "変数"を使用してサンプルをコード化しました。マクロ/関数は、次のような制約をエンコードするために使用されます。式は0または1です。 http://rise4fun.com/Z3Py/JF