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.

  • $\begingroup$ 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? $\endgroup$ Sep 22, 2011 at 11:38
  • $\begingroup$ isn't this better asked at SO or Computational theory at SE? $\endgroup$
    – Tomas
    Sep 22, 2011 at 12:49
  • 3
    $\begingroup$ 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. $\endgroup$
    – Srivatsan
    Sep 22, 2011 at 13:13
  • 2
    $\begingroup$ @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. $\endgroup$
    – Srivatsan
    Sep 22, 2011 at 13:16

1 Answer 1


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.

  • $\begingroup$ Ok, then as long as such a witness preserving reduction doesn't exist or can't be found, it won't work. That makes sense. Further reading showed me some sort of hint: Satisfying an instance of hornsat simultaneously with an instance of 2sat is np-complete. If I alter my method slightly, I get exactly a reduction from 3sat to hornsat+2sat. $\endgroup$ Sep 22, 2011 at 13:07
  • $\begingroup$ Yes, that sounds about right. I think you basically proved that an satisfiability of an instance of hornsat simultaneously with an instance of 2sat is np-complete. $\endgroup$ Sep 22, 2011 at 13:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.