問題タブ [satisfiability]

誰かが最も簡単な方法で私に説明できます3-SATかVertex Cover? こちらの説明に従っています(4 ページ下部までスクロール)。2 ノード変数ガジェットと 3 ノード節ガジェットの 2 つの「ガジェット」を持つ基本的なセットアップを理解しています。k = variables + 2 clausesまた、すべてのエッジをカバーするために必要なノードの最小数として式を理解しています。私が理解していないのは、この設定が存在する場合k-covering、CNFのブール式が満足できることを証明する方法です。充足可能な式と充足不可能な式の例が役立ちます。また、3-SAT問題が に変換されるとk-covering、どの値(trueまたはfalse) を各変数に割り当てて、ブール式 ? を満たす必要があります。助けてくれてありがとう。

I have a .cnf file which contains numbers as Conjunctive Normal Form.

I need to read and store them in a data structure (matrix or list) to be able to work with them as index. (I need this to solve a 3-SAT problem.)

How can I read and store them in Java?

私は、ゴルファーの問題に一連のセットを持っています (各週に、2 人のプレーヤーが 2 回以上一緒にプレーせず、全員が毎週 1 回だけプレーするように、グループを形成する必要があります)。

私の制約は次のとおりです（すべてが正しく機能するかどうかはまだわかりません）：

私の問題は、制約番号 5 にあります。「int の var セット: x」で min を使用することはできません。「int のセット: x」で使用する必要があります。残念ながら、私はこれら2つの違いを理解していません(私が読んだことから、これは各セットのサイズの定義に関連している可能性がありますが、よくわかりません)。

誰かが私に問題を説明し、解決策を提案してもらえますか? とても感謝しています。ありがとう！

true に設定された最小量の変数を使用してブール充足可能性問題を解決するための疑似コードを考え出すのに問題があります。

ブール式を満足できるものにするために true に設定する必要がある変数の最小数を取得するために呼び出すことができるメソッド satisfiable number(H) があります。

}

これが私の現在のロジックです。私が正しい軌道に乗っているかどうか教えてください。

実際にコーディングする前に、DPLL手順を理解しようとしています。

たとえば、次の句があります。

ここで、決定変数を d = 0、b = 0 とします。節は次のようになります。

ここで、ユニットの伝播と純粋なリテラル規則がどのように役割を果たすのでしょうか?

また、C3 : {1, !a}- を とるa = 1と、これは になり{1, 0}ます。この句の最終的な値は何ですか? {1} にする必要がありますか?

そして、決定変数を適用した後、いずれかの節に value {!b}、つまりリテラルの否定がある場合、どのように処理を進めればよいでしょうか?