gDMC: A Generic Distributed Model Counting Framework via Work-Stealing
arXiv:2607.13634
The paper introduces gDMC, a generic framework that uses work‑stealing to distribute exact propositional model counting across multiple cores, allowing existing #SAT solvers to be parallelized with minimal changes and achieving near‑linear speedup.
Abstract
Propositional Model Counting () 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.