algorithm - 2-CNF SAT は P にあり、3-CNF SAT は NPC にあるのはなぜですか?

Question

なぜ 2-CNF SAT が P にあり、3-CNF SAT が NPC にあるのか、本当に混乱しています。CLRS を読んで、3-CNF SAT が NPC にあることを証明する方法を理解しています。SAT から 2-CNF-SAT への同じ還元可能性を使用して、2-CNF-SAT が NPC にあることを証明することはできませんか? 2-CNF SAT が P にある理由がわかりません。

Answer 1

2-CNF SAT が P にある理由

それを解決するための多項式アルゴリズムがあるからです。

証明の大まかなスケッチ:

2-CNF の句は、 と が変数またはその否定のいずれかであるという形式であることに注意してくださいA => B。したがって、この節は、A が true の場合、B が true になるように強制することを示していることがわかります。また、B が false であることは、A が false になることを意味します。それは後で考えなければなりません。AB

これで、変数を 1 つずつ取得し、それ自体が推移的に負になるかどうか (A => B => C => ... => 非 A) およびその逆 (非 A => . .. => A)。最初が true の場合、A は false でなければなりません。2 番目の場合、A は真です。両方の場合、式は満足できません。

式を充足不能にする変数が見つからない場合、式は充足可能です。

この「残忍な」アルゴリズムは、グラフの強く接続されたコンポーネントを使用する実際のアルゴリズムではないことに注意してください。それでも、それは多項式です（1つの変数の検索は明らかにO（N ^ 2）です。これは、O（N）句を考慮して一度に1つの変数を強制し、O（N）変数を考慮するため、アルゴリズムが多項式であることを意味します） . 節に多くても 2 つのリテラルがあるという事実が重要であることに注意してください。条項がA => B or C何かである場合、それはうまく機能しません。

Answer 2

CNF SAT から 3-CNF SAT への正規の削減は、lit_1 OR lit_2 OR ... OR lit_n のような句を取り、2 つの句 lit_1 OR lit_2 OR ... OR lit_{floor(n/2)} OR に置き換えることです。 var, lit_{floor(n/2) + 1} OR ... OR lit_n OR NOT var. この方法で 3 つのリテラルを含む節をクラックしようとすると、3 つのリテラルを含む別の節が得られるため、同じ証明は 2-CNF SAT では機能しません (おそらく正当な理由があります)。