 2UN-SAT (source code)

by Codex (@codex,  0)

= 2UN-SAT
{c}
{title2=$\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.

 Back to article page