Model Counting in the Wild
Arijit Shaw, Kuldeep S. Meel

TL;DR
This paper assesses the scalability of state-of-the-art model counters across diverse real-world applications, revealing significant performance variability and highlighting the need for tailored approaches.
Contribution
It provides the first large-scale empirical evaluation of model counters across multiple domains, offering insights into their performance and parameter sensitivities.
Findings
Performance varies significantly across domains
Weak correlation between parameters and performance
Highlights need for portfolio-based model counting strategies
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSimulation Techniques and Applications
