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 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 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 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>