# Why are Hornsat, 3sat and 2sat not equivalent?

I have been reading a little bit about complexity theory recently, and I'm having a bit of a stumbling block. The horn satisfiability problem is solvable in linear time, but the boolean satisfiability problem in general is NP-Hard. So far so good, I understand that.

Apparently Boolean satisfiability is reducible to satisfiability of a boolean expression in Conjunctive Normal form with 3 variables per clause. This problem though is also NP-Hard. That's fine with me too, since it was proven by someone probably much smarter than me.

I am having trouble though because of the following tautology:

$$(a \vee b \vee c) \iff ((\neg a \wedge \neg b)\implies c)$$

Not exactly a Horn clause, but I am not done.

So given a 3SAT problem, apply the above tautology.

then replace each negated boolean $\neg x$ with a new variable $x_n$

This is an instance of HORNSAT, but unfortunately it isn't equivalent to the original problem. This new problem though is polynomial time equivalent to a certain instance of 2SAT(satisfiable iff the HORNSAT is). Now if for each introduced variable $x_n$, we add the following to our 2SAT problem: $$(x \vee x_n)\wedge (\neg x \vee \neg x_n)$$

Shouldn't this 2SAT instance then be equivalent to the original 3SAT instance? The number of variables doubled and it has a linear factor more clauses.

I must be overlooking something, right? I can't for the life of me see the flaw. Can someone explain it to me?

EDIT: and a counterexample would be nice.

-
I'm thinking it has to be something to do with the reduction from hornsat to 2sat. Does such a reduction introduce new variables for example? – Tim Seguine Sep 22 '11 at 11:38
isn't this better asked at SO or Computational theory at SE? – Tomas Sep 22 '11 at 12:49
Some of your clauses are Horn, but the others are 2-CNF clauses. I don't think mixing them both in a single problem is a good idea. – Srivatsan Sep 22 '11 at 13:13
@Tomas No, the question is a better fit at this site. cstheory is for research level questions in theoretical CS. SO is for programming questions and this one is mathematical, it's not about programming. – Srivatsan Sep 22 '11 at 13:16