1

z3が通常数十ミリ秒でunsatを検出するSMTLIB2の例がいくつかありますが、unsatコアを生成するリクエストを追加すると、check-satは数分間戻りません。この動作は予期されるものですか? unsat コアを要求することは、インストルメンテーション記録の依存関係をオンにするだけでなく、z3 が実行する手順とオプションを変更するだけではありませんか? unsat コア生成を使用しているときと使用していないときの動作が同じになるように、さらにオプションを設定することはできますか?

Scientific Linux 6.3 で Z3 4.3.1 (安定版ブランチ) を使用しています。

例は AUFNIRA にありますが、いくつかは実数を含まず、おそらく非線形ではありません。

ありがとう、

ポール。

4

1 に答える 1

5

unsat コアは、「回答リテラル」(別名、仮定) を使用して追跡されます。unsat コア抽出を有効にして、次のようなアサーションを使用する場合

(assert  (! (= x 10) :named a1))

Z3 は内部的に名前の新しいブール変数を作成し、a1アサートします。

(assert  (=> a1 (= x 10)))

が呼び出されると、check-satこれらすべての補助変数が true であると見なされます。つまり、Z3 は問題が unsat/sat modulo これらの仮定であることを示そうとします。満足できるインスタンスの場合、通常どおりモデルで終了します。満たされないインスタンスの場合、これらの仮定されたブール変数のみを含むレンマを生成するたびに終了します。補題は、が想定されるブール変数のサブセットで(or (not a_i1) ... (not a_in))ある形式です。a_i私の知る限り、この手法は MiniSAT ソルバーによって導入されています。ここで説明します(セクション 3)。実装が簡単で、基本的に unsat コアの生成が無料でできるので、とても気に入っています。

ただし、この方法にはいくつかの欠点があります。まず、一部の前処理手順が適用できなくなりました。ただ主張するなら

(assert (= x 10))

Z3はどこでも置き換えxられます。10Z3 は「値の伝播」を行っていると言えます。アサーションが次の形式の場合、この前処理ステップは適用されません。

(assert  (=> a1 (= x 10)))

これは単なる例であり、他の多くの前処理ステップが影響を受けます。計算中は、単純化ステップの一部も無効になります。Z3 ソース ファイルsmt_context.cppを調べると、次のようなコードが見つかります。

   void context::simplify_clauses() {
        // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed.
        if (m_scope_lvl > m_base_lvl)
            return;
        ...
   }

m_scope_lvl > m_base_lvl)「回答リテラル」/仮定が使用されている場合、条件は常に真です。そのため、unsat コアの生成を有効にすると、パフォーマンスに大きな影響を与える可能性があります。本当に無料のものはないようです:)

于 2013-02-21T19:36:56.237 に答える