問題タブ [smt]

SAT と SMT について読みました。実際のプログラミング シナリオでどのように適用できるのか、常に疑問に思っています。

次に例を示します。

それが真であるとすれば、真か偽var a = 20; var b = a;かを知りたいのです。b = 20

それをブール代数式に変換してSATを適用するにはどうすればよいですか?

Z3 で、特定のモデルが一意であり、他のソリューションが存在しないことを証明/表示する方法はありますか?

実証する小さな例

次のモデルがユニークであることは知っていますが、Z3 オプションを使用するか、アサーションを追加することでこれを保証できますか?

明確にするために、JAVA APIを介してZ3を使用しています

(get-assignment) コマンドは、シンボルのリストと、ブール型の場合はその true/false 値を返す必要があります。私の理解では、これは :produce-assignments が true に設定されていて、(check-sat) が sat を返す場合にのみ実行できます。ただし、Z3 でこれをテストするために小さなスクリプトを実行すると、(get-assignment) は () - 空白を返すだけです。これが私のスクリプトです：

Z3 が問題を段階的に解決する方法について質問があります。ここでいくつかの回答を読んだ後、次のことがわかりました。

1. インクリメンタル ソルビングに Z3 を使用するには 2 つの方法があります。1 つはプッシュ/ポップ (スタック) モードで、もう 1 つは仮定を使用する方法です。Z3 のソフト/ハード制約。
2. スタック モードでは、z3 はグローバル(そうですか? ) スコープで学習したすべての補題を、1 回のローカル "ポップ" 後でも忘れますSMT ソルバーでの制約強化の効率
3. 仮定モード (名前はわかりません。それが頭に浮かんだ名前です) では、z3 は値の伝播などの一部の数式を単純化しません。unsat コアの要求に応じて z3 の動作が変更される

いくつかの比較を行いました (数式についてお問い合わせください。rise4fun に載せるには大きすぎます) が、ここに私の所見を示します: 量指定子を含む一部の数式では、仮定モードの方が高速です。多くのブール変数 (仮定変数) を含む一部の数式では、スタック モードは仮定モードよりも高速です。

それらは特定の目的のために実装されていますか? Z3 でインクリメンタル ソルビングはどのように機能しますか?

私は集合を関係として符号化し、集合に対する操作を普遍的に定量化された含意として符号化しています。単項述語 p (例: v<4, v>4, ..) を満たす要素を選択することによって新しいセットを生成するセットに対する選択演算子があります。この演算子のおかげで、数式に単純な算術述語が含まれています。このような式の Z3 エンコーディングの例を以下に示します。

予想どおり、Z3 は上記の式に対して UNSAT を返します。しかし、私の質問は -

1. 数式を前置正規形で記述できるとすれば、それはまだ EPR クラスですか?
2. そのような式は決定可能ですか？z3 はそのような式の決定手順ですか? 式が決定可能になるように述語を制約するにはどうすればよいですか?

更新 - 前述の式のセットは、リレーショナル代数の結合クエリとして表現できますが、不等式があります。

jSMTLIB を API として使用する必要があります。

しかし、私を助けることができるチュートリアルが見つかりません。

私が見つけた唯一のものは、完全ではないユーザー ガイドです。( http://www.grammatech.com/resource/smt/jSMTLIBUserGuide.pdf )

Javaでソルバーを作成し、いくつかのアサートを実行することを知っている人はいますか?

それがどのように機能するかの例を見せてもらえますか?

ありがとう。

次のコードがあります: (declare-const L4 (_ BitVec 6)) (declare-const L1 (_ BitVec 6)) (declare-const L0 (_ BitVec 6)) (declare-const l2 (_ BitVec 6) )))

このコードを実行すると、モデルは次のようになります。 L0 () (_ BitVec 6) #b000100) (define-fun L4 () (_ BitVec 6) #b000100) (define-fun l2 () (_ BitVec 6) #b001000) ) unsat

の結果minは次のとおりです。

L1 の最小値はこれであり、b000011 ではないため、b001000 ではありません。

誰かが私を説明できますか？

最後に、S x < l 内のすべての x についてチェックする関数 Lt_l を定義しますが、S l < x 内のすべての x についてチェックする GT_l を実行したいと思いました。次のコードがあります。

しかし、これはなぜうまくいきませんか？

ありがとう

SMT における理論の組み合わせを扱おうとしている研究がいくつかあることは知っています。ただし、SMT-Lib 2.0 言語 ( http://smtlib.cs.uiowa.edu/docs.html ) は、この点に関して何も述べていません。私の質問は、それがサポートされているかどうかです。また、複数の理論を同時に処理する機能を提供するソルバーは何ですか?

ありがとう、

次の SMT-LIB コードは、Z3、MathSat、および CVC4 では問題なく実行されますが、Alt-Ergo では実行されません。どうなるか教えてください。よろしくお願いします。