gDMC: A Generic Distributed Model Counting Framework via Work-Stealing
For researchers and practitioners needing exact model counting for probabilistic reasoning, this framework provides a scalable distributed solution that can parallelize existing solvers with minimal modification.
This paper tackles the scalability bottleneck of exact model counting by proposing a generic distributed framework that uses work-stealing for load balancing. The framework achieves near-linear scalability and significantly outperforms existing distributed solvers on competition benchmarks.
Propositional Model Counting ($\#\mathsf{SAT}$) is essential for probabilistic reasoning but faces scalability limits on single cores. Existing distributed approaches struggle with high initialization overheads (static decomposition) or rigid architecture. We propose a novel, generic framework for distributed \emph{exact} model counting. Leveraging C++ templates, our architecture decouples parallel orchestration from solving logic, enabling state-of-the-art solvers to be parallelized with minimal modification. We implement an adaptive work-stealing strategy that ensures effective load balancing. Experiments on competition benchmarks show that our approach achieves near-linear scalability and significantly outperforms existing distributed solvers.