A class of formulas called factored negation normal form is introduced. They are closely related to BDDs, but there is a DPLL-like tableau procedure for computing them that operates in PSPACE.Ordered factored negation normal form provides a canonical representation for any boolean function. Reduction strategies are developed that provide a unique reduced factored negation normal form. These compilation techniques work well with negated form as input, and it is shown that any logical formula can be translated into negated form in linear time.
Reiner Hähnle, Neil V. Murray, Erik Rosenthal