5

前の質問に答えてくれたJoshとLeonardoに感謝します。

もう少し質問があります。

<1>別の例を考えてみましょう。

(exists k) i * k > = 4 and k > 1.

これには、i> 0の単純な解があります。（IntとRealの両方の場合）

しかし、フォローしてみると、

(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))

Z3ここで数量詞を削除できませんでした。

ただし、実際のケースでは排除できます。（iとkが両方とも実数の場合）量化記号消去法は整数の方が難しいですか？

<2>システムでZ3CAPIを使用しています。システム内の数量詞を使用して、整数にいくつかの非線形制約を追加しています。Z3は現在、充足可能性をチェックし、システムが充足可能であるときに正しいモデルを提供します。

量化記号消去法の後、これらの制約は線形制約に還元されることを私は知っています。

z3は、充足可能性をチェックする前に、自動的に量化記号消去法を実行すると思いました。しかし、上記のケース1ではそれができなかったので、今では、通常、量化記号消去法のないモデルが見つかると思います。私は正しいですか？

現在、z3は私のシステムの制約を解決できます。ただし、複雑なシステムでは失敗する可能性があります。このような場合、z3を使用せずに他の方法で量化記号消去法を実行し、後でz3に制約を追加することをお勧めしますか？

<3>システムに整数非線形制約の代わりに実非線形制約を追加することを考えることができます。その場合、C-APIを使用して量化記号消去法を実行するようにz3を強制するにはどうすればよいですか？

<4>最後に、これは量化記号消去法を実行するためにz3を強制するための良い考えですか？または、通常、量化記号消去法を実行せずに、よりインテリジェントにモデルを検索しますか？

ありがとう。

4

1 に答える 1

6

<1> 非線形整数演算の理論では、量指定子の消去 (qe) は認められません。さらに、非線形整数演算の決定問題は決定不能です。

Z3 では、非線形の実数算術式の量指定子の削除に対するサポートが制限されていることを思い出してください。現在の手順は、仮想用語置換に基づいています。将来のバージョンでは、非線形の実数演算が完全にサポートされる可能性があります。

<2> 量指定子の削除は、デフォルトでは有効になっていません。ユーザーはそれを要求する必要があります。Z3 は、量指定子の削除が有効になっていない場合でも、充足可能な式のモデルを見つけることがあります。モデルベースの量指定子のインスタンス化 (MBQI) と呼ばれる手法を使用します。Z3 オンライン チュートリアルには、 この手法の機能と制限を説明するいくつかの例があります。

<3> Z3_context オブジェクトを作成するときに有効にする必要があります。コマンド ラインで設定された任意のオプションは、Z3_context オブジェクトの作成中に指定できます。モデルの構築と量指定子の削除を可能にする例を次に示します。

Z3_config cfg = Z3_mk_config();
Z3_context ctx;
Z3_set_param_value(cfg, "MODEL", "true");
Z3_set_param_value(cfg, "ELIM_QUANTIFIERS", "true");
Z3_set_param_value(cfg, "ELIM_NLARITH_QUANTIFIERS", "true");
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);

その後、ctxモデルの構築と量指定子の削除をサポートする Z3 コンテキスト オブジェクトを指しています。

<4> MBQI モジュールは、線形演算フラグメントに対しても完全ではありません。Z3 オンライン チュートリアルでは、完成したフラグメントについて説明しています。MBQI モジュールは、解釈されない関数を含む問題に適したオプションです。問題が算術演算のみを使用する場合、量指定子の除去は通常、より適切で効率的です。そうは言っても、MBQI を使用すると、いくつかの問題をすばやく解決できます。

于 2012-05-03T19:10:54.213 に答える