3-Horn Satisfiability Decision Problem

Definition

3-Horn Satisfiability Decision Problem

Instance: A Boolean formula $F={\bigwedge }_{j=1}^m{C}_j$ in conjunctive normal form, with at most three positive literals in each clause. Here “3-Horn” denotes this positive-literal bound; the number of negative literals is unrestricted.

Question: Does there exist a truth assignment $\alpha :\mathrm{Var}(F)\to \{\top ,\perp \}$ such that

$$\alpha \models F?$$

Unlike 3-SAT, this restriction does not bound the total clause size. It relaxes the at-most-one-positive-literal condition of a Horn formula.