2UN-SAT ($\text{at most two positive literals per clause}$)

Satisfiability of conjunctive normal form formulas whose clauses have at most two unnegated variables. It is NP-complete: binary AND/OR and unary NOT gate equivalences in a Tseitin transformation already satisfy that restriction. Clauses may contain arbitrarily many negative literals; the total clause width is not restricted to two.