6

Z3 SMT ソルバーを使用して、SMTLIB 2 言語を使用してロジック QF_BV で表現した問題を解決しています。

モデルは満足できないので、ソルバーに不飽和コアを生成させようとしています。

私のモデルは、assertステートメントを使用して指定するいくつかの「必須」の制約で構成されています。

unsat-core 生成で考慮したいアサーションは、(assert (! (EXPR) :named NAME))構文を使用して指定されています。

予想どおり、 Z3 は を返しますunsat。ただし、Z3 は常に、すべての名前付きアサーションで構成される「些細な」unsat-core をダンプするようです。

名前付きアサーションのサブセットが存在することを知っています。これは unsat-core です。このコアは、Yices SMT ソルバーを使用して見つけました。これにより、比較的小さな unsat-core が得られることがよくあります。Yices モデルは Z3 モデルと同じです (SMT2 から Yices 入力言語への行ごとの翻訳です)。

「良い」unsat-core を生成することはソルバー固有の機能ですか、それとも Z3 がより良いコアを提供できるようにするための一般的な提案/変更はありますか?

4

1 に答える 1

6

Z3 と Yices 1.x は、unsat コアの計算に同じアプローチを使用します。不満足性の証明に使用されたすべてのアサーションを追跡します。ただし、各システムによって構築された証明はかなり異なる場合があります。Z3 と Yices によって提供される機能に加えて、最小の unsat コアを計算するためのアルゴリズムがあります。ここに参照があります。

編集: デフォルトでは、Z3 は問題を解決しようとする前にいくつかの前処理ステップを使用します。これらの手順の一部は、unsat コアの生成に影響を与える可能性があります。特に、問題の方程式を使用して定数を削除します。Z3 は方程式を「解いて」変数を消去すると言います。スクリプトでは、このステップを無効にすることでコアを小さくできます。オプションを使用してそれを実現できます

(set-option :auto-config false)

Z3 は非常に一般的な構成を実行します。ビットベクトルの問題については、通常、「関連性の伝播」を無効にすることをお勧めします。

(set-option :relevancy 0)

最後に、変数除去ステップを有効/無効にして、unsat コア サイズへの影響を確認できます。

(set-option :solver true) ;; Z3 will generate the core C0 C1 C2
(set-option :solver false) ;; Z3 will generate the core C1 C2
于 2012-02-28T15:25:02.457 に答える