New advances in compiling CNF to Decomposable Negation Normal form

Abstract

We describe a new algorithm for compiling conjunctive normal form (CNF) into Deterministic Decomposable Negation Normal (d-DNNF), which is a tractable logical form that permits model counting in polynomial time. The new implementation is based on latest techniques from both the SAT and OBDD literatures, and appears to be orders of magnitude more efficient than previous algorithms for this purpose. We compare our compiler experimentally to state of the art model counters, OBDD compilers, and previous CNF2dDNNF compilers.