# Model Counting in the Wild

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 42 references that are in the map.
- First posted on arXiv 13 Aug 2024.

## Builds on (most cited first, 8 of 8)

- [The Model Counting Competition 2020](https://mlsanity.com/paper/2012.01323/) (2020)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [ADDMC: Weighted Model Counting with Algebraic Decision Diagrams](https://mlsanity.com/paper/1907.05000/) (2019)
- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [Computing Tree Decompositions with FlowCutter: PACE 2017 Submission](https://mlsanity.com/paper/1709.08949/) (2017)
- [Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation](https://mlsanity.com/paper/2206.02775/) (2022)
- [Quantitative Verification with Neural Networks](https://mlsanity.com/paper/2301.06136/) (2023)

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

- [Numerical Considerations in Weighted Model Counting](https://mlsanity.com/paper/2508.06264/) (2025)
- [CSB: A Counting and Sampling tool for Bit-vectors](https://mlsanity.com/paper/2607.04142/) (2026)

## Abstract (arXiv)

Model counting is a fundamental problem in automated reasoning with applications in probabilistic inference, network reliability, neural network verification, and more. Although model counting is computationally intractable from a theoretical perspective due to its #P-completeness, the past decade has seen significant progress in developing state-of-the-art model counters to address scalability challenges. In this work, we conduct a rigorous assessment of the scalability of model counters in the wild. To this end, we surveyed 11 application domains and collected an aggregate of 2262 benchmarks from these domains. We then evaluated six state-of-the-art model counters on these instances to assess scalability and runtime performance. Our empirical evaluation demonstrates that the performance of model counters varies significantly across different application domains, underscoring the need for careful selection by the end user. Additionally, we investigated the behavior of different counters with respect to two parameters suggested by the model counting community, finding only a weak correlation. Our analysis highlights the challenges and opportunities for portfolio-based approaches in model counting.