ADDMC: Weighted Model Counting with Algebraic Decision Diagrams
This provides a more efficient solution for computational tasks in areas like artificial intelligence and verification, though it is incremental as it builds on existing model counting methods.
The paper tackles exact weighted model counting for Boolean formulas by introducing ADDMC, an algorithm using Algebraic Decision Diagrams and dynamic programming, which significantly outperforms existing state-of-the-art solvers on 1914 benchmarks.
We present an algorithm to compute exact literal-weighted model counts of Boolean formulas in Conjunctive Normal Form. Our algorithm employs dynamic programming and uses Algebraic Decision Diagrams as the primary data structure. We implement this technique in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We then compare ADDMC to state-of-the-art exact weighted model counters (Cachet, c2d, d4, and miniC2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver.