Distributed model counting is constrained by balancing and caching. We analyze how gDMC addresses this through work-stealing and an explicit stack.
In model counting (#SAT) tasks, the system degrades not due to a single reason, but due to a combination of factors. Sequential solvers hit the limits of single-core: frequencies are not increasing, and the component cache requires more and more memory. Attempts to scale through distributed model counting often shift the problem up the stack. Static decomposition (cube-and-conquer) creates high initialization overhead and struggles with heterogeneous tasks. As a result, the classic straggler problem arises: the total time is determined by the slowest worker because it is necessary to cover the entire solution space, rather than find a single answer.
An alternative is dynamic balancing through work-stealing. In gDMC, this is implemented as a solver-agnostic layer that separates orchestration from solver logic. The architecture using C++ templates allows for the integration of existing DPLL-style solvers with minimal changes. This is an important trade-off: instead of rewriting the core (as in DMC), a generalized interface is introduced with zero abstraction cost at runtime. The price is the necessity to strictly formalize which states can be safely transferred between workers.
The key idea of the implementation is the abandonment of an implicit recursive stack in favor of an explicit structure (explicit stack). This changes the execution model. In a typical DFS, subtasks are “hardcoded” into the call stack and cannot be transferred. In gDMC, each node contains:
- local subtasks
- result accumulator
- references to remote tasks
- scaling factor
This stack simultaneously becomes a scheduler and an aggregation point. A node cannot be removed until results from the “stolen” tasks are returned. This directly affects latency: instead of blocking, the worker continues local work, and synchronization is deferred.
Work-stealing here is limited to the upper part of the stack. This is not a random simplification, but a safeguard against cache thrashing. Component caching in #SAT is sensitive to context (especially due to clause learning). If arbitrary subtasks are shared, inconsistent results can occur. gDMC introduces strict conditions: only nodes whose parent dependencies have already been “exposed” can be transferred. This reduces parallelism but maintains correctness.
An additional complexity is the interaction with learned clauses. They change the output space but do not always logically follow from the local subtask. This can “poison” the cache (cache inconsistency). In a distributed system, the problem is exacerbated: a worker may not see a conflict that should have cleared the cache. gDMC addresses this through a restriction: sharing is allowed only for branches where all components have been checked for satisfiability. This adds overhead (SAT checks), but is applied rarely and at the upper levels of the tree, so it does not become a bottleneck.
From an orchestration perspective, a master-worker model with a point-to-group strategy is used. The master selects one active worker as the source of work and redistributes tasks to several idle nodes. This reduces network overhead and speeds up the “warming up” of the cluster. Workers exchange not formulas, but compact representations (partial assignments and component variables). This reduces bandwidth and latency.
A practical detail is the use of assumptions mode. This allows the solver’s internal state to be preserved between tasks: variable activity, learned clauses, component cache. Unlike systems where each task is isolated, here the worker accumulates knowledge. This is critical for throughput on series of related subtasks.
According to experimental results (competition benchmarks), the system demonstrates near-linear scalability and solves more instances than DisCount and DMC. Exact metrics depend on configuration, but the trend is clear:
- less overhead on simple tasks (no partitioning stage)
- better balancing on complex tasks (dynamic stealing)
At the same time, there are conscious trade-offs. Arbitrary-precision arithmetic is more expensive than double in DMC. Sharing restrictions reduce maximum parallelism. The master remains a coordination point, although it does not become a bottleneck in experiments.
In an industrial context, this appears as an evolutionary improvement of the architecture of distributed solvers. The main shift is not in the counting algorithm, but in managing state and task boundaries. This approach aligns well with modern clusters, where the cost of communication and imbalance often exceeds the cost of computation.
Information source
arXiv is the largest open preprint repository (since 1991, under the auspices of Cornell), where researchers quickly post working versions of papers; the materials are publicly accessible but do not undergo full peer review, so results should be considered preliminary and, where possible, checked against updated versions or peer‑reviewed journals. arxiv.org