Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
    
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
2  
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
1  
@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

1 Answer 1

up vote 4 down vote accepted

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.

share|improve this answer
    
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. –  Tim Seguine Sep 22 '11 at 13:07
    
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. –  Stefan Geschke Sep 22 '11 at 13:10

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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