# 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? Sep 22, 2011 at 11:38
• isn't this better asked at SO or Computational theory at SE? Sep 22, 2011 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. Sep 22, 2011 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. Sep 22, 2011 at 13:16