z3（論理QF_BV）で「不良」コアを取得する

Question

私は、SMTLIB 2言語を使用して、論理QF_BVで表現した問題を解決するのにZ3 SMTソルバを使用しています。

モデルが満足できないため、ソルバーにunsat-coreを生成させようとしています。

私のモデルは、いくつかの「必須」制約から成ります。これはassertステートメントを使って指定します。

アサーションは、コアの生成には、(assert (! (EXPR) :named NAME))を使用して指定されています。

Z3は、期待通りに私にunsatを与えます。しかし、Z3は常に、すべての名前付きアサーションで構成される「些細な」unsat-coreをダンプするようです。

私は名前のついたアサーションのサブセットが存在することを知っています。これは、unsat-coreです。私はYicesのSMTソルバーを使ってこのコアを見つけました。これは、比較的小さなunsatコアを頻繁に提供します。 YicesモデルはZ3モデルと同じです（ほとんどSMT2からYices入力言語への行単位変換）。

"良い" unsat-coresをソルバー固有の機能として生成しているか、Z3がより良いコアを提供できるように一般的な提案や変更がありますか？

Answer 1

Z3とYices 1.xは、unsatコアを計算するために同じ手法を使用します。不満の証拠として使われたすべてのアサーションを追跡します。しかし、各システムによって構築された証明は全く異なる場合があります。 Z3およびYicesによって提供される機能の上に、最小の未実装コアを計算するためのアルゴリズムがあります。ここにはreferenceがあります。

EDIT：デフォルトでは、Z3は問題を解決する前に複数の前処理ステップを使用します。これらのステップのいくつかは、unsatコアの生成に影響する可能性があります。特に、問題の方程式を使用して定数を削除します。我々は、Z3が方程式を "解き"、変数を排除すると言う。 scriptでは、この手順を無効にすることでより小さなコアを取得できます。

(set-option :auto-config false) 

Z3は非常に一般的な構成を実行します。 「relevacy伝播」を無効にするには、通常は良いアイデアであるビット・ベクトルの問題については：

(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