An Embarrassingly Parallel Model Counter

Model counting (also known as #SAT) is a fundamental problem in knowledge representation and reasoning, with applications ranging from probabilistic inference to formal verification. However, state-of-the-art model counters are limited by computational resources on a single machine. In this paper, we propose a novel distributed framework for model counting, exploiting the embarrassingly parallel nature of the problem. By decomposing the search space into independent subproblems and distributing them across different computation nodes, our approach achieves near-linear scalability on practical instances. Extensive experiments on standard benchmarks demonstrate both the effectiveness and efficiency of our framework.

Authors

• Zhenghang Xu
• Minghao Yin Northeast Normal University
• Jean Marie Lagniez

Keywords

• #SAT
• Distributed Architecture
• Embarrassingly Parallel
• Model Counting