= 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>. Consequently
$$
\boxed{\mathrm{2UN\text{-}SAT}\text{ is NP-complete}}.
$$
The condition limits positive <literals>, without limiting total <clause> length.
Back to article page
