Horn clauses and satisfiability It is well known that satisfiability of Horn formulae can be checked in polynomial time using unit propagation.
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? 
 A: I think 3SAT can be reduced to your problem, since
($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 ...
is satisfiable iff
(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 ...
is.
A: In the paper The complexity of satisfiability problems MR0521057, 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:


*

*Every relation in S is satisfied when all variables are 0.

*Every relation in S is satisfied when all variables are 1.

*Every relation in S is definable by a CNF formula in which each conjunct has at most one negated variable.

*Every relation in S is definable by a CNF formula in which each conjunct has at most one unnegated variable.

*Every relation in S is definable by a CNF formula having at most 2 literals in each conjunct.

*Every relation in S is the set of solutions of a system of linear equation over the two-element field {0,1}.
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.
