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? 



Horn clauses and satisfiability
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.


