Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces gDMC, a generic framework for distributed propositional model counting that addresses the scalability limitations of traditional single-core approaches. By utilizing C++ templates, the framework separates parallel orchestration from the logic solving process, allowing for minimal modifications to existing solvers while implementing an adaptive work-stealing strategy for effective load balancing. Experimental results demonstrate that gDMC achieves near-linear scalability and significantly outperforms current distributed model counting solvers on benchmark tests.
Achieving near-linear scalability in distributed model counting could revolutionize probabilistic reasoning applications.
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.