Horn clauses and satisfiability - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T07:15:02Z http://mathoverflow.net/feeds/question/34989 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/34989/horn-clauses-and-satisfiability Horn clauses and satisfiability Akshar Prabhu Desai 2010-08-09T10:52:53Z 2010-08-09T15:29:49Z <p>It is well known that satisfiability of Horn formulae can be checked in polynomial time using unit propagation.</p> <p>But suppose we relax the condition for horn clauses from at most one un-negated literals to two un-negated literals. Then is it possible to prove that satisfiability of such a formula can be checked in time polynomial in the size of the formula? </p> http://mathoverflow.net/questions/34989/horn-clauses-and-satisfiability/34991#34991 Answer by darij grinberg for Horn clauses and satisfiability darij grinberg 2010-08-09T11:20:08Z 2010-08-09T11:25:09Z <p>I think 3SAT can be reduced to your problem, since</p> <p>(\$a_1\$ OR \$a_2\$ OR \$a_3\$) AND (\$b_1\$ OR \$b_2\$ OR \$b_3\$) AND (\$c_1\$ OR \$c_2\$ OR \$c_3\$) AND ...</p> <p>is satisfiable iff</p> <p>(NOT \$A_1\$ OR \$a_2\$ OR \$a_3\$) AND (\$A_1\$ OR \$a_1\$) AND (NOT \$B_1\$ OR \$b_2\$ OR \$b_3\$) AND (\$B_1\$ OR \$b_1\$) AND (NOT \$C_1\$ OR \$c_2\$ OR \$c_3\$) AND (\$C_1\$ OR \$c_1\$) AND ...</p> <p>is.</p> http://mathoverflow.net/questions/34989/horn-clauses-and-satisfiability/35006#35006 Answer by François G. Dorais for Horn clauses and satisfiability François G. Dorais 2010-08-09T14:47:47Z 2010-08-09T15:29:49Z <p>In the paper <em>The complexity of satisfiability problems</em> <a href="http://www.ams.org/mathscinet-getitem?mr=521057" rel="nofollow">MR0521057</a>, Tom Schaefer characterizes exactly which general classes of satisfiability problems are in P and which are NP-complete. Those problems which are in P fall into six cases:</p> <ul> <li><p>Every relation in S is satisfied when all variables are 0.</p></li> <li><p>Every relation in S is satisfied when all variables are 1.</p></li> <li><p>Every relation in S is definable by a CNF formula in which each conjunct has at most one negated variable.</p></li> <li><p>Every relation in S is definable by a CNF formula in which each conjunct has at most one unnegated variable.</p></li> <li><p>Every relation in S is definable by a CNF formula having at most 2 literals in each conjunct.</p></li> <li><p>Every relation in S is the set of solutions of a system of linear equation over the two-element field {0,1}.</p></li> </ul> <p>Here, S is a set of boolean relations that one takes as primitives for the language; the associated satisfiability problem is then deciding the satisfiability of a finite conjunction of such primitives. Schaefer moreover shows that any set of relations which does not fall into one of the above has a NP-complete satisfiability problem. In your example, S would be a set of boolean relations definable by a CNF formulas in which each conjunct has at most two unnegated variables. This is not in the above list, so the corresponding satisfiability problem is NP-complete.</p>