Knowledge Compilation: Decomposable Negation Normal Form versus Linkless Formulas?

Abstract. Decomposable negation normal form (DNNF) was developed primar-ily for knowledge compilation. Formulas in DNNF are linkless, in negation nor-mal form (NNF), and have the property that atoms are not shared across conjunc-tions. Full dissolvents are linkless NNF formulas that do not in general have the latter property. However, many of the applications of DNNF can be obtained with full dissolvents. Two additional methods — regular tableaux and semantic factor-ing — are shown to produce equivalent DNNF. A class of formulae is presented on which earlier DNNF conversion techniques are necessarily exponential; path dissolution and semantic factoring handle these formulae in linear time.