gDMC: A Generic Distributed Model Counting Framework via Work-Stealing
Zhenghang Xu, Minghao Yin, Junping Zhou, Jean-Marie Lagniez
Abstract
Propositional Model Counting (#SAT) is essential for probabilistic reasoning but faces scalability limits on single cores. Existing distributed approaches struggle with high initialization overheads (static decomposition) or precision loss and rigid architecture (dynamic solvers like dmc). We propose a novel, generic framework for distributed 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 load balancing and guarantees exact results via arbitrary-precision arithmetic. Experiments on competition benchmarks show that our approach achieves near-linear scalability and significantly outperforms existing distributed solvers.
BibTeX
@inproceedings{ijcai2026_gdmcagenericdist,
title = {gDMC: A Generic Distributed Model Counting Framework via Work-Stealing},
author = {Zhenghang Xu and Minghao Yin and Junping Zhou and Jean-Marie Lagniez},
booktitle = {IJCAI 2026},
year = {2026}
}