How is 2-CNF SAT is in P, while 3-CNF SAT is in NPC?

Question

I am really confused why 2-CNF SAT is in P, while 3-CNF SAT is in NPC. I Read CLRS, and I understand how they prove 3-CNF SAT is in NPC. Can't I use the same reducibility from SAT to 2-CNF-SAT to prove 2-CNF-SAT is in NPC. I don't understand why 2-CNF SAT is in P.

Answer 1

why 2-CNF SAT is in P

Because there is a polynomial algorithm to solve it.

A rough sketch of a proof:

Note that any clause in 2-CNF is in the form A => B where A and B are either variables or their negation. Therefore, we can tell that this clause says when A is true, it forces B to be true. It also means that B is false forces A to be false. We have to consider that later.

Now, you can take a variable, one by one, and search if it transitively forces itself to be its negative (A => B => C => ... => non A) and vice versa (non A => ... => A). If the first is true, A has to be false; if the second, A is true. If both, the formula is unsatisfiable.

If you don't find any variable that makes the formula unsatisfiable, it is satisfiable.

Note that this "brutal" algorithm is not the actual one using strongly connected components of a graph, which I recommend you to read on. Yet, it is polynomial (the search for one variable is clearly O(N^2), since you force one variable at a time considering O(N) clauses and you consider O(N) variables, which means the algorithm is polynomial). Note that the fact that we have at most two literals in a clause is crucial. If the clauses were A => B or C or something, it wouldn't work as good.

Answer 2

The canonical reduction from CNF SAT to 3-CNF SAT is to take a clause like lit_1 OR lit_2 OR ... OR lit_n and replace it with two clauses 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. If you try to crack a clause with three literals this way, you'll get another clause with three literals, so the same proof won't work for 2-CNF SAT (and probably for good reason).