# ADDMC: Weighted Model Counting with Algebraic Decision Diagrams

arXiv: https://arxiv.org/abs/1907.05000 · HTML: https://mlsanity.com/paper/1907.05000/

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Jul 2019.

## Built on by (most cited first, 13 of 13)

- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Proof Complexity of Symbolic QBF Reasoning](https://mlsanity.com/paper/2104.02563/) (2021)
- [Model Counting in the Wild](https://mlsanity.com/paper/2408.07059/) (2024)
- [flip-hoisting: Exploiting Repeated Parameters in Discrete Probabilistic Programs](https://mlsanity.com/paper/2110.10284/) (2021)
- [CCDD: A Tractable Representation for Model Counting and Uniform Sampling](https://mlsanity.com/paper/2202.10025/) (2022)
- [PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas](https://mlsanity.com/paper/2312.15877/) (2023)
- [Scalable Precise Computation of Shannon Entropy](https://mlsanity.com/paper/2502.01160/) (2025)
- [Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits](https://mlsanity.com/paper/2503.01009/) (2025)
- [Numerical Considerations in Weighted Model Counting](https://mlsanity.com/paper/2508.06264/) (2025)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)
- [Scalable Algorithms for Approximate DNF Model Counting](https://mlsanity.com/paper/2601.10511/) (2026)
- [Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach](https://mlsanity.com/paper/2605.13830/) (2026)
- [CSB: A Counting and Sampling tool for Bit-vectors](https://mlsanity.com/paper/2607.04142/) (2026)

## Abstract (arXiv)

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.