Authors: Arijit Shaw, Kuldeep S. Meel
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.
Source: http://arxiv.org/abs/2408.07059v1
