問題タブ [z3]

制限付きプログラム検証のバックエンドソルバーとしてZ3を使用します。異なるオペレーティングシステム、Windows7X64とSuSe10.3X64のZ3に同じ数式をフィードします。どちらのZ3も、バージョン3.2です。

それらの入力は次の とおりです。run.z3、ネストされた数量詞が含まれています。

明示的なオプションが有効になっていない場合（デフォルトモード）、Z3はWindowsで非常にうまく機能しますが、Linuxでは「セグメンテーション違反」が発生します。

../solvers/z3/bin/z3：行11：27951セグメンテーション違反

次に、唯一のオプションを追加します

（set-option：PULL_NESTED_QUANTIFIERS true）

数式に追加して再実行すると、今回はLinuxで動作し、Windowsでも動作し、より高速に解決されます。このオプションは、Linuxでの私の問題を解決します。

WindowsとLinuxのバージョン3.2のZ3は異なる機能を提供しますか？それは本当です、他に何の違いがありますか？前もって感謝します！

「knapsack.smt2」というファイルに、ナップザックの問題に対する次のサンプル コードがあります。これは smt2 形式であると思われ、最新バージョンの Z3 を使用しています。

ただし、「z3 -m knapsack.smt2」を実行すると、次のエラー メッセージが表示されます。

ここで、46 行目は最後の行「(get-model)」です。

これが機能しない理由を誰か教えてもらえますか?

ありがとう。

マルチセットを、合計が等しい 2 つのセットに分割する必要があります。たとえば、マルチセットが与えられた場合:

2 つのセットを出力します。

どちらも合計すると 7 になります。

Z3 (smt2 入力形式) と「線形演算ロジック」を使用してこれを行う必要があります。これは次のように定義されています。

正直なところ、これをどこから始めればよいかわかりません。アドバイスをいただければ幸いです。

よろしく。

次の Perl スクリプトを作成して、論理制約を smt2 形式で生成し、特定の入力ファイルの数独パズルを解きました。入力ファイルは次の形式です。

大きな醜い Perl スクリプトは次のとおりです。

セグメント障害を引き起こしているスクリプトの部分は次のとおりです。

しかし、このフラグメントは次のようなものを出力するだけです:

これは、次と論理的に同等である必要があります。

アドバイスをいただければ幸いです。

よろしく。

これを達成する方法についての提案を期待しています:

定義: 無向グラフ G は、頂点の集合 V と辺の集合 E によって定義されます。ここで、各辺はサイズ 2 の V のサブセット、つまり頂点の順序付けられていないペア {u, v} です。G の長さ k のサイクルは、{v_1, v_2}, {v_2, v_3}, ..., {v_k-1, v_k}, {v_k, v_1 の異なる頂点のシーケンス v_1, ..., v_k です。 G のハミルトニアン サイクルは、長さ n = |V| のサイクル、つまり、グラフの各頂点を 1 回だけ通過する chcle です。ハミルトニアン サイクルを持つ場合、G ハミルトニアンと呼びます。

問題: 次の決定問題の命題論理定式化を提供します: 無向グラフ G が与えられた場合、G はハミルトニアンですか? 製剤は Z3 によってチェックされます。

入力形式は次のとおりです。

ここで、最初の数字は頂点の数を表し、残りのペアはすべて G のエッジです。

出力は次のようになります: 0 1 2 3

明らかに、出力は常に数値 1、...、n-1 の順列になります。ここで、n = |V| です。しかし、命題論理のみを使用して整数を操作する方法がわかりません。

アドバイスをいただければ幸いです。

よろしく。

これは、指定された入力に対して機能するソリューションです。エッジの組み合わせ (n Choose k) を生成する perl ルーチンを書くことができれば、これを任意の数の入力に一般化できます。

無向グラフでハミルトン閉路を見つける問題をハッキングしています。しかし、最近の実験では、不可能なモデルになるはずだったものが作成されました。入力は次のとおりです。

入力の xor ステートメントが明確にこれを禁止しているにもかかわらず、e1、e2、e3、e4、および e5 のすべてが true であることを示す出力を次に示します。

ここで何がうまくいかないかについて誰か意見がありますか？

よろしく。

Z3の数式が不飽和で、（get-proof）が指定されている場合、それが何であるかについての情報が見つからない出力があります。それに関するドキュメントはどこにありますか？

私にはまったく読めないようですが、これを入力として受け取るツールはありますか？

乾杯、マット

QFBV フォーミュラで Z3 を使用しています。SATソルバーがブール句でできるように、Z3がそのような式で段階的に機能できるかどうか疑問に思っていました。基本的に、次のループを実装する方法が必要です。

Z3 は学習した情報を維持しますか? z3 を段階的に使用できますか?

ありがとう。

UFBVクエリでZ3を実行しています。現在、クエリには2つの呼び出しが含まれていますcheck-sat。push 1直後に置くとcheck-sat、Z3は30秒でクエリを解決します。私が何も入れていない場合、つまりそれらの間に何も入れずpush 1に2つの呼び出しがある場合、Z3は200秒でそれを解決します。面白い。特定の理由または単なる偶然の一致？check-satpush 1

私の質問を例で説明しましょう：

たとえば、-1、0、2、3、5、および 6 などの可能な離散整数の領域があるとします。ここで、次の制約を満たす変数 x の解 (またはモデル) を探しています。

(x > 0) && (x < 6) && (x != 3) && (x > 2)

答えは (ソリューション ドメインから) = 5 になりますね。

Z3でこれを行うにはどうすればよいですか？

つまり、個別のエンティティを使用して解空間を定義し、いくつかの制約をアサートして、Z3 に充足可能性を確認するように依頼します。満足できる場合は、モデルが必要です。

誰かが例を手伝ってくれますか?

ありがとう、イシュティアク