問題タブ [z3py]

上記のコードを書きましたが、うまくいきません。入力として文字列を使用していないため、受け入れる入力の種類を見つけることができません。

与えられc == a + 4たt == c + b、もしb == -4、そしてt == a。私は反対のことをしようとしています。つまり、上記の 2 つの方程式 と が与えられた場合t == a、b

これは関連する質問aとかなり似ていますが、今回はとを切り替えるだけbで、コードが異なる結果を返すことに本当に混乱しています。

上記のリンクに投稿されたコードに続いて、以下のコードがあります（類似、唯一a、b切り替え）：

ただし、Ubuntu では、上記のコードを実行すると予期しない結果Unsatが返されますが、値-4 (または0xfffffffc )は返されません。

なぜこれが間違っているのですか？

本当にありがとう。

Z3 を使用して、配列プロパティ フラグメント内の式の充足可能性を確認しています。Z3 が返す配列変数のモデルは通常、他の if 式や if-then-else の場合分けなどを使用して表現されます。 Z3 が出力するモデルを何らかの方法で解析し、入力 SMT-LIB 式を満たす配列を作成したい、明示的に。

たとえば、Z3 が次の形式に出力するモデルを常に単純化できるようにしたいと考えています。

モデルを (C API を使用して) トラバースし、モデルを表す明示的な配列を作成する簡単な方法はありますか?

次のコードを使用しています。

出力は次のとおりです。この例をここでオンラインで実行します

この例では、行列 M は 2-SAT インスタンスを CNF (参照) として定義します。この例では、行列 M が手動で入力として導入されました。行列 M を自動的に導入する方法を教えてください ( matrix )。どうもありがとう。

TL;DR: を使用すると、ビット ベクトル除算ノードが からにZ3_OP_BSDIV変わります。除算操作と未解釈の操作をどのように区別できますか?Z3_OP_UNINTERPRETEDsimplify

説明：

次のセッションは、ビット ベクトル除算が解釈されることを示していますが、 を使用した後は解釈されませんsimplify()。以下の変数で何が起こるかを見てくださいd。

UDiv手動で宣言された未解釈の関数があり、同じ種類もあることがわかります。

ただし、解法には影響していないようです。ソルバーは依然として演算を実際の除算として解釈しているようです。

ノードを種類ごとに処理しようとしていますが、これはその種類について「嘘をついている」ようです。実際に解釈されていることを知る方法はありkindますZ3_OP_UNINTERPRETEDか? これはバグですか？

次の 3-SAT インスタンスと対応するグラフを検討してください。

グラフは他の2つの形式で表示できます

このグラフのトゥッテ多項式は

グラフの独立数が 4 の場合、考慮される 3-SAT インスタンスは充足可能です。この事実は、コードを使用してチェックされます。

対応する出力は次のとおりです。

対応するグラフの補数は

グラフの補数のトゥッテ多項式は

補数のクリーク数は 4 であり、考慮されている 3-SAT インスタンスは充足可能であると言えます。

問題は次のとおりです。トゥッテ多項式を使用して、考慮されている 3-SAT インスタンスが充足可能かどうかを判断できますか?

Z3Py で、変数/式が発生するすべての式のリストを取得することは可能ですか? 例：

z3py を使用して式を単純化しようとしていますが、さまざまな戦術に関するドキュメントが見つかりません。私が見つけた最良のリソースは、すべての戦術を名前別にリストしたスタック オーバーフローの質問です。

利用可能な戦術に関する詳細なドキュメントに私をリンクさせることができる人はいますか? オンラインの python チュートリアルでは不十分です。

または、誰かがこれを達成するためのより良い方法を推奨できますか?

問題の例は、次のような式です。

x < 5, x < 4, x < 3, x = 1これを に簡略化したいと思いx = 1ます。

この例では、タクティックの使用unit-subsume-simplifyが機能しているように見えます。

しかし、結果としてx > 1, x < 5, x != 3, x != 4得x > 1, x < 5, x ≠ 3, x ≠ 4られるようなより複雑な例を試してみると。ご希望の際はx = 2。

z3py を使用してこのタイプの単純化を達成するための最良のアプローチは何ですか?

私の現在の解決策。

ありがとうマット

何年にもわたって、私はテクノロジーの解決法を追跡しており、特定のパズル、つまり「交差するはしご」にそれらを適用することについてのブログ投稿を維持しています。

要点を言えば、たまたま z3 のことを知り、それを具体的な問題に当てはめてみました。私は Python バインディングを使用して、次のように書きました。

残念ながら、z3 レポート...

この問題には、少なくとも次の整数解があります: a=34、b=50、c=42、d=105、e=16、f=40。

私は何か間違ったことをしていますか、それともこの種の連立方程式/範囲制約は z3 が解決できる範囲を超えていますか?

助けてくれてありがとう。

更新、5年後：Z3はこれをすぐに解決できるようになりました。

私はZ3が初めてで、オンラインのpythonチュートリアルをチェックしていました。

次に、BitVecs でオーバーフローの動作を確認できると考えました。

私はこのコードを書きました：

そして、私は [y = 7, x = 7] を期待していました (つまり、値が等しいが、x + 1 が 0 になり、y + 1 が 8 になるため、後続の値が等しくない場合)

しかし、Z3 は [y = 0, x = 0] と答えます。

私は何を間違っていますか？