問題タブ [satisfiability]

ブール値の充足可能性がNP完全であることは知っていますが、ブール式の最小化/単純化です。これは、特定の式を記号形式で取得し、同等であるが単純化された式を記号形式で生成することを意味します.NP完全ですか？充足可能性から最小化への減少があるかどうかはわかりませんが、おそらくあると思います。誰かが確かに知っていますか？

次のような式がある場合：

(FA = すべての場合 / E = 存在する)

スコーレミゼーションのルールは次のように述べています。

1. E が FA の外にある場合、定数または
2. E が FA の内部にある場合、FA の外部からのすべての変数を引数として含む新しい関数に置き換えます。

では、この場合はどうすればよいでしょうか。Exists 量指定子を単に削除することはできますか、それとも定数に置き換えることはできますか?

ありがとう！

ただの好奇心の質問。クラスのグループワークで、教授が人々を特定の数のグループに分割したことを覚えていますか（n）？

私の教授の何人かは、n一緒に働きたい人と一緒に働きたくない人のリストを各学生から取り、次に、学生が好きな人と一致し、一緒に働くことを避ける場所nのグループを魔法のように見つけますn彼らが好まない人々。

私には、このアルゴリズムはナップサック問題によく似ていますが、この種の問題に対するあなたのアプローチについて質問したいと思います。

編集：私の質問とまったく同じようなものを説明しているACMの記事を見つけました。既視感の2番目の段落を読んでください。

私はCSPに比較的慣れておらず、変数間に課せられた==、>、<、および！=制約に基づいて、それぞれのドメインからすべての変数の値を見つけようとしています。私はChocoとJacopを見ましたが、これらのタイプの問題を解決することについてこれ以上知ることができませんでした。この例の実装を見つけることができる場所を教えていただけますか？私はPrologを使用してこれを解決しましたが、これを行うためにOOPを使用したいと思います。

ありがとうございました。

多項式（またはより現実的にはO（N ^ 2））であることが知られているブール充足可能性問題の特殊なケースについて学ぶことに興味があります。これらのケースには、満足のいくすべてのインスタンスを実際に生成するための効率的なアルゴリズムも必要です。効率的とは、すべてのインスタンスのシーケンスを生成するのにO（N #SAT）が必要であることを意味します。2番目の条件が最初の条件を暗示している可能性はありますが、私にはわかりません。

簡単な例：1SAT :)

簡単な例：2SATに句の「チェーン」があるため、変数と句を結ぶグラフは線になります。

もっとどこかにリストはありますか？ありがとう。

次の問題があります。

論理的に同等にならなければならない 2 つの命題式があります。そのうちの 1 つだけが「変数」を含みます。これは、変数を任意の命題式に置き換えることができるという意味です。ここでの問題は、論理的等価性が真になるように、変数の実際の置換を見つける必要があることです。例：

(a ^ ~b) または x = a

ここで、x は変数を表します。この論理的等価性は、x を a ^ b に置き換えることによって真にすることができるため、次のようになります。

(a ^ ~b) または (a ^ b) = a

これが問題です。入力として「1つの変数xを持つ方程式」を取得し、方程式が論理的に等価になるように変数xの出力値として与えるアルゴリズムが必要です。

変数は常に 1 つです。（実際、複数の変数で問題が発生する可能性がありますが、最初に単純なケースを解決したいと考えています）。問題の数式は、任意の形式を持つことができます (それらは CNF または DNF ではありません)。また、数式は実際には FALSE または TRUE になる可能性があり、解がない場合 (たとえば、"a または x = false" の場合、解がない場合) または複数の解 (たとえば、"a and x = false の場合) があります。 " 誤った命題は有効な答えになります)。

私が持っているのは、式が充足可能かどうかを教えてくれるタブロー推論器だけです。だから私は解決策をテストすることができます。しかし、私の問題は、私に解決策を与えることです。

SATがNP完全であるという証明は構成的証明であるため、プログラムとして実装できるはずです。誰かがこれをしましたか？

プログラム（trueまたはfalseを返す）を入力として受け取り、SAT式を出力するプログラム（コンパイラー）を探しています。

したがって、たとえば、コンパイラは次のプログラム（pythonic構文で表示されますが、どの言語でも問題ありません）を入力として受け取り、SAT式を出力できます。SAT式をSATソルバーにフィードすると、パラメーター「証明書」の解が得られます。この場合、解は[False、True、True、True、False]になり、{-3、-2、5}が解であることを示します。

明らかに、出力SAT式には他の補助変数があるため、コンパイラーはどの変数が証明書に対応するかを示す必要があります。

そのようなコンパイラはすでに存在しますか？それらのいずれかがオープンソースですか？

句データベースで構成される SAT インスタンスの前処理中に、すべての変数に単語を割り当てる必要があります。ハッシュ関数は、変数ごとに 16 の最上位ビット (MSB) の 1 ビットと 16 の最下位ビット (LSB) の 1 ビットを除いて 0 のみで構成される 32 ビット ワードを返します。変数。句の署名は、すべての変数のハッシュ関数値のビットごとの OR です。

このハッシュ関数を実装するにはどうすればよいですか?

問題

私は、SAT 最適化問題の特別なサブセットを見ています。SAT および関連トピックに慣れていない方は、関連するウィキペディアの記事をご覧ください。

NOT はなく、接続詞の標準形です。これは簡単に解決できます。ただし、ステートメント全体を真にするために、真の割り当ての数を最小限に抑えようとしています。その問題を解決する方法が見つかりませんでした。

可能な解決策

私はそれを解決するために次の方法を思いつきました：

1. 有向グラフに変換し、頂点のサブセットのみにまたがる最小全域木を検索します。エドモンドのアルゴリズムがありますが、それは頂点のサブセットではなく完全なグラフの MST を提供します。
   • 頂点のサブセットの問題を解決する Edmond のアルゴリズムのバージョンがあるのではないでしょうか?
   • 元の問題から他のアルゴリズムで解決できるグラフを作成する方法があるのではないでしょうか?
2. SAT ソルバー、LIP ソルバー、または徹底的な検索を使用します。この問題を講義資料として使用しようとしているので、これらの解決策には興味がありません。

質問

アイデアやコメントはありますか？うまくいくかもしれない他のアプローチを考え出すことができますか?

Z3 SMT Solver で次のことを証明しようとしています: ((x*x) + x) = ((~x * ~x) + ~x). これは正しいです。これは、C プログラミング言語のオーバーフロー セマンティックのためです。

今、私は次の smt-lib コードを書きました:

z3 からの出力は次のとおりです。

ここで私の質問: 結果が「unsat」になるのはなぜですか? コード内の simple コマンドは、myfun1 と myfun2 が同じ結果になるように有効な割り当てを取得できることを示しています。

私のコードに何か問題がありますか、それとも z3 のバグですか?

誰でも私を助けてください。どうも