 Solution

A proposed assignment for 2UN-SAT can be checked in polynomial time, including checking the syntactic restriction, so the language belongs to NP.

For an explicit reduction, parse any Boolean formula into a Boolean circuit over binary AND (logical conjunction), binary OR (logical disjunction) and unary NOT (negation), and apply the gate equivalences in part (a), asserting its output. Every gate clause has at most two positive literals: the AND clauses have respectively one, one and one; the OR clauses have one, one and two; and the NOT clauses have two and zero. The unit output/constant clauses also obey the restriction. Hence the resulting formula is an instance of 2UN-SAT.

The Tseitin transformation is linear in the gate description, and its auxiliary variables enforce the gate values rather than relaxing their relation to the inputs. Therefore the original formula is satisfiable if and only if the transformed restricted formula is satisfiable. This is a polynomial-time many-one reduction from SAT, whose hardness follows from the Cook-Levin theorem. ConsequentlyThe condition limits positive literals, without limiting total clause length.