Model Counting in the Wild

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 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.