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.
Best Answer
What you would need is a translation between HORNSAT and 2SAT that let's you translate a witness for the satisfiability of the Horn formula into a witness for the 2SAT (or the other way around? But this doesn't really matter.). In any case, a cheap way to reduce HORNSAT to 2SAT is to solve your instance of HORNSAT in polynomial time, i.e., to check satisfiability, and then return a trivially satisfiable instance of 2SAT or a trivially not satisfiable instance of 2SAT. In other words, you throw away all information about the Horn formula, other than whether it is satisfiable or not. In particular, the terms that describe the role of the new variables that you add have no meaning relative to the 2SAT instance you get from the Horn formula.