mlsanityData to 14 Oct 2026

ADDMC: Weighted Model Counting with Algebraic Decision Diagrams

arXiv 1907.05000 ↗First posted 11 Jul 2019cs.LO cs.AI cs.DScited by 13

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 2; 2022: 2; 2023: 1; 2024: 1; 2025: 4; 2026: 3.

13 papers.

Sort:

  1. 2022DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solvingcited by 3
  2. 2021Proof Complexity of Symbolic QBF Reasoningcited by 2
  3. 2024Model Counting in the Wildcited by 2
  4. 2021flip-hoisting: Exploiting Repeated Parameters in Discrete Probabilistic Programscited by 1
  5. 2022CCDD: A Tractable Representation for Model Counting and Uniform Samplingcited by 1
  6. 2023PBCounter: Weighted Model Counting on Pseudo-Boolean Formulascited by 1
  7. 2025Scalable Precise Computation of Shannon Entropycited by 0
  8. 2025Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuitscited by 0
  9. 2025Numerical Considerations in Weighted Model Countingcited by 0
  10. 2025Attn-JGNN: Attention Enhanced Join-Graph Neural Networkscited by 0
  11. 2026Scalable Algorithms for Approximate DNF Model Countingcited by 0
  12. 2026Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approachcited by 0
1 more
  1. 2026CSB: A Counting and Sampling tool for Bit-vectorscited by 0