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.