On Compiling CNFs into Structured Deterministic DNNFs

Abstract We show that the traces of recently introduced dynamic programming algorithms for #SAT can be used to construct structured deterministic DNNF (decomposable negation normal form) representations of propositional formulas in CNF (conjunctive normal form). This allows us prove new upper bounds on the complexity of compiling CNF formulas into structured deterministic DNNFs in terms of parameters such as the treewidth and the clique-width of the incidence graph.

Authors

• Simone Bova
• Florent Capelli
• Stefan Mengel
• Friedrich Slivovsky

Keywords

No keywords are indexed for this paper.