ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams

We compute exact literal-weighted model counts of CNF formulas. Our algorithm employs dynamic programming, with Algebraic Decision Diagrams as the primary data structure. This technique is implemented in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We also compare ADDMC to state-of-the-art exact model counters (Cachet, c2d, d4, miniC2D, and sharpSAT) on the two largest CNF model counting benchmark families (BayesNet and Planning). ADDMC solves the most benchmarks in total within the given timeout.