問題タブ [sat]

私はSATの問題を解決しなければなりません。その問題には 2 つのカーディナリティ制約があります。最初の 1 つは、1 日あたり最大 6 つの「同じステージのクラス」、「大学」は 1 日 12 時間「開いている」ため、制約を生成して SAT ソルバーに適用する必要があります。

2 番目のカーディナリティ制約は次のとおりです。すべての被験者は、週に少なくとも X 時間必要です。

私は読んでいて、最初の最良の方法は「ネットワークアルゴリズムのソート」かもしれません.2番目についてはわかりませんが、実装方法もプロローグでの実装も開始していません。

aiZ3 には、SAT 問題を定式化するためにbj、 、 、 などのブール変数がたくさんあります。ckただし、私の問題では、考慮すべき 3 つの算術制約があります。

Z3 API を使用して、変数の型を変更せずにこれら 3 つの算術制約を定式化するにはどうすればよいでしょうか (つまり、デフォルトではすべてブール型)。

私は調査ツールのコンポーネントに取り組んでいます。取得に興味があります (QF_LRA の場合)

- 複数の (最小限またはそれ以外の) UNSAT コアおよび -
複数の SAT 割り当て

このトピックに関する以前の議論についてフォーラムをチェックしました 。

z3 Python チュートリアルを参照しています。たとえば、http://rise4fun.com/Z3Py/tutorial/musmssです。

今のところオフラインのようです。上記のチュートリアルを見つけるために github などの他の提案を試みましたが、うまくいきませんでした。

z3 Java API を使用しています。しかし、代替手段に切り替えて喜んでいます。

SMTLIB2 構文を使用して、満足のいくすべての割り当てを取得する方法はありますか?

私が使用しているソルバーは Z3 と CVC4 です。

私は sat4j ソルバーがまったく初めてで、ブール値の満足可能な問題を研究しています。そして私は立ち往生しています。ブール式の整数変数を解くプログラムを作りたいです。

x1 < x2 + x3 ユーザーがその数式を入力すると、私のプログラムは x1 = 5 、 x2 = 3 、 x3 = 4 のようにこの数式を満たします (true を返します)。したがって、数式は true を返し、ユーザーは数式を満たすこの整数値を取得します。私はJavaでEclipseで作業しているため、sat4jで作成することは可能です。

この質問を再投稿して申し訳ありません。z3 が複数の未飽和コア、複数の満足のいく割り当てを返すようにする方法

完全を期すために、上記のリンクからの元の質問は次のとおりです。

取得に興味があります (QF_LRA の場合)

- 複数の (最小限またはそれ以外の) UNSAT コアおよび - 複数の SAT 割り当て

このトピックに関する以前の議論についてフォーラムをチェックしました。これらは、現在オフラインのように見えるhttp://rise4fun.com/Z3Py/tutorial/musmssなどの z3 Python チュートリアルを参照してい ます。上記のチュートリアルを見つけるために、githubなどの他の提案を試みましたが、うまくいきませんでした。

以前の質問に対する回答を投稿してくれた Nikolaj Bjorner に感謝します。ただし、回答に掲載されているコード フラグメントが完全かどうかはわかりません。誰かがこれについてコメントできますか？

元の質問への回答で参照されている、参照された論文と Mark Liffiton の Web ページを調べました。完全なコード フラグメントを再投稿または明確化できる場合は、最も役に立ちます。

どうもありがとう

ここから始めましょう: すべてのNP 問題はSAT (ブール充足可能性問題)に還元できると言われています。Circuit SATに対してより正確に言うと、NP のようなすべての意思決定問題は最終的にYesまたはNoの答えになるはずです。

しかし、ランダム NP の問題がある場合、テストするブール回路を作成する方法、入力をグループ化する方法、それらの入力を接続するゲート(AND、NOT、OR など) の種類について説明します。したがって、基本的に、私の質問は、 TRUE または FALSEの答えを与えるブール回路を設計する方法です。

最後に、その答えが何を意味するか。この NP 問題は多項式時間で解くことができ、FALSE はできないため、TRUE は理解できますか?

私の質問を説明する論理的な間違いを犯したとしても、本当にとんでもないことをしないでください:)あなたがそれを理解してくれることを願っています.

興奮して答えを待っています。

ブール式 (NNF、CNF ではない) のモデルを単純に検索するアルゴリズムを作成しようとしています。

私が持っているコードは既存のモデルをチェックできますが、モデルを見つけるように求められたときに失敗します (または終了しません) member(X, Y)。[X|_], [_,X|_], [_,_,X|_]...

私がこれまでに持っているのはこれです：

のより良いデータ構造F、または部分的にインスタンス化されたリストを切り捨てることができる他の方法はありますか?

編集: 定義と例を追加しました。

z3 -smt2 <filename>'sat' または 'unsat' のみを出力します。制約が満たされている場合は Z3 がモデルを出力し、満たされていない場合は unsat コアを出力することを希望します。Z3 のどのオプションを使用すればよいですか?