5

SMT ソルバーに関する新しい研究を行うことは、利用可能な問題が決定手順に直接関係しない多くのトリックと前処理技術を必要とするという事実によって妨げられることがよくあります。これらは公開されていないか、適切に実装して最適化するのに時間がかかることが多く、さらに、さまざまなソルバーの比較と理解が非常に困難になります。

Z3 をプリプロセッサとして使用して、問題を処理し、前処理された形式 (z3 自体が問題を解決するために使用する形式) でダンプすることは可能ですか?

コマンドラインオプションは表示されませんが、戦略、python インターフェイス、または追加のコードを作成することで、これを達成する方法があるのではないかと推測しています。

4

1 に答える 1

4

はい、Z3 はプリプロセッサとして使用できます。このコマンドapplyにより、ユーザーは戦術を適用し、それを SMT 2.0 ベンチマークとしてダンプできます。以下に例を示します (オンラインでもhttp://rise4fun.com/Z3/eutOから入手できます):

(declare-const x Real)
(declare-const y Real)

(assert (forall ((n Real)) (or (< x n) (< n y))))
(assert (= (< x y) (< x 100.0)))

(apply (then qe nnf) :print false :print-benchmark true)

上記の例では、qe (量指定子の削除) および nnf (否定正規形) タクティックが入力問題に適用されます。

いくつかの追加ポイント:

  • いくつかの戦術は、同等に満足できる結果しか生み出しません。したがって、結果のベンチマークのモデルは、元の式のモデルであるとは限りません。関連する「モデル コンバーター」をダンプするように Z3 に依頼できます (オプション:print-model-converter true)。モデル コンバーターは、Z3 で使用される手順をエンコードして、結果の数式のモデルを元の数式のモデルに変換します。ただし、モデルコンバーターの印刷には規格がなく、Z3 ではこれらの記述を読み取ることができません。もちろん、プログラム API を使用してすべてを結び付けることができます。

  • 戦術の小さなセットは、アンダー (sat の結果のみが信頼できる) またはオーバー (unsat の結果のみが信頼できる) 近似を生成します。それらは通常、モデルまたは証明の発見に使用されます。Z3 が結果のゴールを表示すると、結果が正確であることを通知します (sat と unsat は信頼できます)。

于 2012-12-04T18:50:01.353 に答える