1 Introduction↩︎

Model counting (MC), also known as \(\#\mathsf{SAT}\), is the problem of computing the number of models (satisfying assignments) of a given propositional formula, typically in CNF. Its direct extension, weighted model counting (WMC), is of tremendous importance in a wide range of AI applications, including probabilistic inference [1], [2], planning under uncertainty [3], and neural network verification [4]. Beyond AI, model counting is critical in domains such as hardware testing and reliability estimation [5]–[9].

The computational hardness of model counting is underscored by Toda’s theorem [10], which establishes that \(\mathsf{P}^{\#\mathsf{P}}\) encompasses the entire polynomial hierarchy (PH). Despite this theoretical hardness, significant progress has been made in the design of efficient sequential model counters. Modern search-based solvers, such as D4 [11], GANAK [12], and SharpSAT-TD [13], leverage Conflict-Driven Clause Learning (CDCL), component caching, and implicit Boolean Constraint Propagation (BCP) to prune the search space effectively. However, sequential performance is increasingly constrained by the physical limits of single-core clock speeds and the memory required to maintain massive component caches.

The importance of \(\#\mathsf{SAT}\) has driven significant research into scalable algorithms, evidenced by recent model counting competitions [14]. To handle the growing complexity of real-world instances, parallel and distributed computing offers a promising path forward. However, distributing \(\#\mathsf{SAT}\) is fundamentally harder than distributing \(\mathsf{SAT}\). In \(\mathsf{SAT}\), the search can stop as soon as one solution is found, allowing for aggressive, speculative strategies. In \(\#\mathsf{SAT}\), the entire solution space must be covered, meaning the total runtime is determined by the slowest worker (the ‘straggler’ problem). While GPU-accelerated approaches exist [15], they represent a distinct architectural paradigm; this paper focuses on distributed CPU-based solving.

State-of-the-art parallel and distributed solvers, such as dCountAntom [16] and the more recent DisCount [17], typically rely on a Cube-and-Conquer strategy. These methods decompose the search space into independent subproblems (cubes) which are then distributed across nodes. However, this approach has several limitations. First, the initialization overhead is significant; as noted in [17], the decomposition phase can be costly enough to negate performance gains on medium-hard instances. Second, static decomposition suffers from redundancy: separate workers may unknowingly explore identical search spaces. For instance, when different cubes lead to the same connected component, resulting in duplicated effort. Finally, achieving effective load balancing requires generating a massive number of cubes, a parameter that is notoriously difficult to tune and highly instance-dependent.

The distributed solver DMC [18] offers a compelling alternative to static partitioning by employing a dynamic work-stealing mechanism. Unlike dCountAntom, DMC avoids the exchange of formula fragments and learned clauses, significantly minimizing communication overhead. However, its implementation is tightly coupled to the D4 solver, requiring invasive modifications to the sequential core that hinder modularity and maintenance. Additionally, DMC uses double-precision floating-point arithmetic for aggregation; this induces precision loss on instances with large model counts, rendering it unsuitable for exact counting tasks.

To overcome these limitations, we propose a novel C++ framework that leverages generic programming (via Concepts and Templates) to enable efficient, solver-agnostic distributed model counting within the class of DPLL-style counters. Our architecture employs a modular stack that separates distributed orchestration from core solving logic, enabling state-of-the-art solvers to be parallelized with minimal modification. By resolving communication types at compile time, this design ensures zero-cost abstractions with negligible runtime overhead. Furthermore, we formally establish the conditions necessary for safe and complete work sharing.

Specifically, our contributions are threefold. First, we provide a generic, template-based architecture that simplifies the integration of work-stealing into existing DPLL-style model counters. Second, we identify the formal requirements for valid work transfer, establishing the theoretical guarantees necessary for the soundness and completeness of the distributed search. Finally, we demonstrate through extensive experiments that our solution outperforms both static partitioning (e.g., DisCount) and existing work-stealing solvers (e.g., DMC), achieving near-linear speedups and solving significantly more instances.

2 Preliminaries ↩︎

Let \(\mathcal{L}\) represent the propositional language formed from a finite set \(\mathcal{P}\) of propositional variables, using the standard logical connectives (\(\neg\), \(\vee\), \(\wedge\)) and the Boolean constants \(\top\) (true) and \(\bot\) (false). A literal \(\ell\) is either a variable \(x \in \mathcal{P}\) or its negation \(\bar{x}\). A cube (or term) is a conjunction of literals, and a clause is a disjunction of literals. When convenient, clauses and cubes are regarded as sets of literals. A CNF formula is a conjunction of clauses, also viewed as a set of clauses.

Formulas are interpreted in the classical way: an interpretation \(\omega\) is a mapping from \(\mathcal{P}\) to \(\{0, 1\}\). An interpretation \(\omega\) is a model of a formula \(\Sigma\) if \(\Sigma\) evaluates to \(1\) under \(\omega\) (denoted \(\omega \models \Sigma\)). We use \(\models\) to denote logical entailment and \(\equiv\) for logical equivalence. The notation \(\left\|\Sigma\right\|\) denotes the number of models (i.e., satisfying assignments) of the formula \(\Sigma\) over its variables \(Var (\Sigma)\). The #SAT problem asks to compute \(\left\|\Sigma\right\|\) for a given formula and is the canonical example of a \(\#\mathsf{P}\)-complete problem.

The Boolean Constraint Propagator, \({\tt BCP}(\Sigma)\), performs unit propagation by iteratively enforcing unit clauses within the formula \(\Sigma\). \({\tt BCP}(\Sigma)\) returns \(\bot\) (conflict) if unit propagation derives the empty clause (a unit refutation). Otherwise, it returns the set of literals \(S\) derived from \(\Sigma\). The conditioning of \(\Sigma\) by a literal \(\ell\), denoted \(\Sigma|_{\ell}\), is obtained by replacing every occurrence of \(\ell\) with \(\top\) and every occurrence of its negation \(\bar \ell\) with \(\bot\). This is followed by standard Boolean simplifications to remove satisfied clauses and removing \(\bot\) literals from the remaining clauses until the formula is minimal. This notion extends to a set of literals \(S = \{\ell_1, \ldots, \ell_m\}\) by iterative application: \(\Sigma|_{S} = (\dots(\Sigma|_{\ell_1})\dots)|_{\ell_m}\).

State-of-the-art exact model counters typically extend the CDCL architecture used in SAT solving. Unlike SAT solvers, which terminate upon finding a single model, model counters must traverse the entire solution space. To do this efficiently, they rely on three key techniques: Clause Learning, where the solver learns a new clause upon conflict to prune future search; Component Caching, which stores results of previously solved subproblems to avoid redundant computations [19]; and Component Decomposition, which exploits independent sub-formulas \(\Sigma_1, \dots, \Sigma_k\) by computing the product of their counts \(\prod_{i=1}^k \left\|\Sigma_i\right\|\).

The standard model counting procedure generally follows the structure of Algorithm [alg:count] (presented in Section 3, ignoring the modifications highlighted in blue and red). First, \({\tt BCP}(\Sigma)\) is executed to gather the set of implied literals \(S\), and the formula is simplified to \(\Sigma' = \Sigma|_S\). If a conflict arises (i.e., \(\Sigma' = \bot\)), the function returns \(0\). If all clauses are satisfied (i.e., \(\Sigma' = \emptyset\)), the algorithm returns \(2^{|Var (\Sigma)| - |S|}\), which accounts for the single model of the implied literals and the \(2^k\) combinations of any remaining variables. Otherwise, the algorithm checks the cache. If the instance is new, it decomposes the formula into connected components. If multiple components exist, they are solved recursively, and their results are multiplied. If the formula forms a single component, the algorithm selects a branching variable \(x\), computes the sum of the counts for the two branches (\(\Sigma' \wedge x\) and \(\Sigma' \wedge \bar x\)), and caches the result. Finally, in both the component and branching cases, the computed value \(val\) is scaled by \(2^{|Var (\Sigma)| - |Var (\Sigma')| - |S|}\). This factor corrects for variables that were present in \(\Sigma\) but eliminated during simplification (e.g., variables that became free), ensuring the count remains correct with respect to the original variable set.

Crucially, the interaction between dynamic clause learning and component caching requires careful management. When a conflict occurs, a learned clause is added to the formula. Although this clause is a logical consequence of the original formula, its presence modifies the implication landscape. As established in [19], naively retrieving cached components in the presence of different learned clauses can lead to incorrect counts. We explicitly address this constraint in Section 4, where we define the necessary conditions for safe job sharing in a distributed setting.

The efficiency of the solver heavily relies on the variable selection heuristic (\(\mathsf{chooseVariable}\)). Modern approaches exploit the formula’s primal graph and its tree decomposition \((T, \{B_t\})\), a mapping of variables into a tree structure satisfying standard connectivity properties [20]. Although real-world instances often have high treewidth (defined as \(\max |B_t| - 1\)), heuristics that prioritize variables appearing in the “top” bags of the decomposition significantly improve performance by fostering component decomposition [13].

3 The Explicit Stack Framework ↩︎

Exact model counting traverses an AND-OR Tree, summing results at OR-Nodes (decisions) and multiplying at AND-Nodes (decompositions). In standard DFS solvers, pending work remains implicit within the recursion stack. This implicit representation creates a major barrier for distribution, as recursion frames cannot be easily “detached” to offload tasks to other workers.

3.1 The Explicit Search State↩︎

To enable flexible work-stealing, gDMC reifies the recursion stack into a manageable data structure: the Explicit Stack \(\mathcal{S}\). Crucially, we do not materialize the entire tree (which grows exponentially); we maintain only the current active path. Any node on this path with an unexplored sibling represents a potential job that can be offloaded.

It is important to note that \(\mathcal{S}\) does not behave strictly as a standard Last-In-First-Out (LIFO) stack during distributed execution. In a purely sequential setting, a node is popped as soon as its local sub-problems are solved. In gDMC, however, a node \(\nu\) may have offloaded portions of its work to other solvers. Consequently, the node serves a dual purpose: it is both a controller for local iteration and a dependency tracker for remote jobs. Even if the local set of tasks is empty, the node must persist in the stack if it is still waiting for remote results. It acts as an aggregation point, waiting to combine the local accumulator with the results of the outstanding shared tasks. Only when all local and remote obligations are met is the node considered fully resolved and removed from \(\mathcal{S}\).

While the formal definition describes nodes as containing explicit formulas \(\mathcal{F}\), materializing these is inefficient in practice. Instead, gDMC leverages the fact that any search tree sub-problem is uniquely determined by its path from the root. Specifically, a task \(\Sigma_{sub}\) is represented implicitly by: the original formula \(\Sigma_{root}\), the current partial assignment (unit literals from decisions and propagations), and the set of relevant variables restricted to the current connected component.

Consequently, when we describe “pushing a formula \(\Sigma \wedge x\)” onto the stack, the implementation simply records the decision literal \(x\), the set of propagated unit literals, and the variables identifying the current component. The solver reconstructs the effective formula by applying the current assignment to \(\Sigma_{root}\) and filtering by the component’s variables. Similarly, when a job is offloaded to a remote worker, we transmit only the sequence of decisions (the “cube”) that defines the path to that node, along with the set of variables for the component, allowing the remote worker to reconstruct the exact same state locally.

3.2 The Challenge of Distributed Caching↩︎

Integrating work-stealing into model counting is complicated by Component Caching. The standard caching invariant requires that if a formula \(\Sigma\) is solved, its count \(\left\|\Sigma\right\|\) is stored for immediate retrieval. However, offloading \(\Sigma\) to a remote worker creates a broken dependency: the local solver cannot wait for the result without losing parallelism, nor can it cache a “future” result without prohibitive overhead. This “hole” propagates upward, preventing all parent nodes from being cached.

To mitigate this, gDMC restricts sharing to the root of the stack (the least recently generated sub-problems). This topological constraint ensures the active frontier at the top of the stack remains entirely local and free of remote dependencies, allowing sub-trees to be computed and cached synchronously. Furthermore, anchoring sharing to the stack base preserves a low-overhead linear structure, avoiding the need to manage a complex AND-OR dependency tree in memory.

3.3 Stack Primitives↩︎

As \(\mathcal{S}\) retains persistent nodes awaiting remote results, the logical frontier diverges from the physical top. We bridge this by maintaining a pointer \(pos\) to the active context, denoted \(\nu_{curr} = \mathcal{S}[pos] = \langle \mathcal{F}, v, \mathcal{I}, \mu \rangle\).

• \(\mathcal{S}.\mathsf{pushOr}(\Sigma_1, \Sigma_2)\): Pushes a new Decision Node onto \(\mathcal{S}\). This operation is valid only if \(pos\) corresponds to the physical top of the stack. We increment \(pos\) and initialize the new tuple as \(\langle \{\Sigma_1, \Sigma_2\}, 0, \emptyset, 1 \rangle\).

• \(\mathcal{S}.\mathsf{pushAnd}(\{\Sigma_1, \dots, \Sigma_k\})\): Pushes a new Decomposition Node onto \(\mathcal{S}\). This operation is valid only if \(pos\) refers to the physical top of the stack. We increment \(pos\) and initialize the tuple as \(\langle \{\Sigma_1, \dots, \Sigma_k\}, 1, \emptyset, 1 \rangle\).

• \(\mathcal{S}.\mathsf{alreadyShared}(\Sigma)\): Checks if the sub-problem \(\Sigma\) is present in the pending formula set \(\mathcal{F}\) of \(\nu_{curr}\). Returns \(\mathtt{true}\) if \(\Sigma \notin \mathcal{F}\) (implying \(\Sigma\) has been stolen or removed by a concurrent worker). Returns \(\mathtt{false}\) otherwise.

• \(\mathcal{S}.\mathsf{process}(\Sigma)\): Begins local processing of \(\Sigma\) by removing it from \(\mathcal{F}\) in \(\nu_{curr}\). If \(\mathcal{F}\) becomes empty, local work for the node is complete. If the remote identifier set \(\mathcal{I}\) is also empty, the node is fully resolved and popped from \(\mathcal{S}\) (with \(pos\) decremented). Otherwise, the node persists as a dependency tracker for remote results, and we only decrement \(pos\) to return control to the parent context.

• \(\mathcal{S}.\mathsf{identity}()\): Returns the neutral element for the operation associated with \(\nu_{curr}\) (\(0\) if \(\nu_{curr}\) is a Decision Node, \(1\) if it is a Decomposition Node).

• \(\mathcal{S}.\mathsf{isShared}()\): Checks if the current node \(\nu_{curr}\) has partially offloaded its work. Returns \(\mathtt{true}\) if the set of remote identifiers \(\mathcal{I}\) is not empty.

• \(\mathcal{S}.\mathsf{complete}(c \times \mu)\): Updates the accumulator \(v\) of \(\nu_{curr}\) with the result of a sub-computation. The value to aggregate is derived from \(c\) (the raw count computed by the solver) and \(\mu\) (the scaling factor, typically \(2^k\), for variables free in the sub-problem).

3.4 Integration in the Counting Algorithm↩︎

Algorithm [alg:count] illustrates the integration of the gDMC framework into a standard DPLL-style model counter. The implementation utilizes two global controllers: the explicit stack manager \(\mathcal{S}\), which maintains the search state and aggregates results, and the communication manager (referenced as co), which handles network protocols and work redistribution. The core counting logic (comprising unit propagation, component analysis, and variable branching) is shown in black and adheres to the classical formulation. The blue blocks mark the synchronization points with \(\mathcal{S}\), while the red block orchestrates the interaction with remote workers to enable dynamic load balancing.

The first interaction occurs immediately upon entering the function. Before performing any propagation, the solver queries \(\mathcal{S}.\mathsf{alreadyShared}(\Sigma)\). This acts as a guard clause: if the current sub-problem \(\Sigma\) has been removed from the stack (stolen by another worker), the function aborts immediately by returning the neutral element \(\mathcal{S}.\mathsf{identity}()\). This prevents the local worker from solving a task that is no longer its responsibility. If the task remains, \(\mathcal{S}.\mathsf{process}(\Sigma)\) is called to mark \(\Sigma\) as “busy,” ensuring it cannot be stolen while the local worker is actively solving it.

Whenever the solver decomposes the problem, it registers the new sub-problems in the stack to expose the frontier of work. Specifically, before iterating over a set of connected components, the algorithm calls \(\mathcal{S}.\mathsf{pushAnd}\) to create a new decomposition node containing these components. Similarly, prior to making a decision on a variable \(x\), \(\mathcal{S}.\mathsf{pushOr}\) is invoked to record the two resulting branches (\(\Sigma \wedge x\) and \(\Sigma \wedge \bar x\)). These operations ensure that the explicit stack always reflects the current available tasks for potential thieves.

After the recursive calls return, the local solver has computed a partial result \(val\). However, before returning this value, it must query \(\mathcal{S}.\mathsf{isShared}()\). If this check returns \(\mathtt{true}\), it indicates that sibling tasks were offloaded and the local result is incomplete. In this case, the algorithm calls \(\mathcal{S}.\mathsf{complete}\) to aggregate \(val\) into the persistent stack node and returns \(\mathcal{S}.\mathsf{identity}()\), ensuring that the parent recursive call aggregates only the neutral element. Conversely, if the node was not shared, it implies the sub-problem was processed entirely locally. The stack node is effectively popped, and the computed \(val\) is returned normally to the parent to continue the standard aggregation.

We defer the discussion of the red block in Algorithm [alg:count] to Section 4, where we detail the Master-Worker coordination and the network protocols required to interconnect individual solver instances.

4 Distributed Orchestration ↩︎

Algorithm [alg:gdmc] employs a centralized master-worker architecture. Initialization (lines 1–3) follows the discount protocol [17]: the Master broadcasts \(\Sigma\) and enforces the cluster’s best tree decomposition as a static branching order. The root task (\(idTask = 0\)) is then assigned to a single worker (line 5). Once initialized, the full problem is assigned to a single root worker via a blocking \(\mathtt{sendJob}\) call with an initial task identifier \(idTask = 0\) (line 5), while remaining workers enter an idle state. To simplify synchronization, gDMCimplements a point-to-group sharing strategy: the Master targets only one active worker for work-stealing at a time, tracked by the variable \(\mathit{contacted}\).

While at least one worker is active, the Master monitors the cluster. If \(\mathit{contacted} = \mathsf{nil}\), the Master selects a new target and sends a work request. Upon a positive non-blocking \(\mathtt{isResponding}\) check, the Master facilitates direct transfers from the target to multiple idle workers (lines 11–13), assigning each sub-task a unique \(idTask\) for aggregation. This one-to-many transfer mitigates latency and rapidly re-integrates workers. Finally, completed workers return to the \(\mathit{idle}\) set; if the \(\mathit{contacted}\) worker finished, the pointer is reset.

When all workers return to the idle state, the Master initiates result aggregation (line 18). Unlike DMC, which streams partial expressions to the Master, gDMCmaintains stacks locally. To resolve a task, a worker must complete any previously shared nodes. When two workers communicate, the “thief” tracks the “victim” to return the computed value once the sub-stack for that \(idTask\) is resolved. This propagates values back through the dependency chain until the root task (\(idTask=0\)) is completed.

4.1 Worker-Master Integration↩︎

We now detail the integration logic (the red block in Algorithm [alg:count]) that links the individual solver to the global orchestrator. To minimize communication overhead, the function \(\mathsf{shouldPoll}\) acts as a throttle, ensuring the worker polls for Master requests only periodically (e.g., every \(k=1,000\) decisions) to avoid system-call degradation.

The functions \(\mathsf{shareRequest}\) and \(\mathsf{transferWorkToThiefs}\) manage the worker’s network interaction. \(\mathsf{shareRequest}\) checks for an incoming \(\mathtt{requestWork}\) signal. If detected, the worker begins a blocking communication to indicate if it has viable work. A worker may refuse to share if it is processing its last available formula or if the remaining sub-problems are too small to justify the communication cost. To prevent a “ping-pong” effect between active and idle states, we enforce a granularity threshold; for instance, formulas with fewer than 30 variables are solved locally rather than shared.

Finally, \(\mathsf{transferWorkToThiefs}\) handles the offloading of a pending node to a thief. The victim performs a blocking send of the task data (variables and partial assignments) to the thief. Crucially, the victim does not wait for the result. It simply adds the assigned \(idTask\) to the set of remote identifiers \(\mathcal{I}\) of the current stack node (marking it as persistent) and immediately resumes its local search.

4.2 Distributed Caching and Soundness↩︎

Sharing arbitrary nodes from the stack is not permissible. As previously mentioned, sharing is restricted to nodes whose parents have already been shared. However, this topological constraint is insufficient to prevent cache inconsistency, particularly when dealing with unsatisfiable sub-formulas.

Cache inconsistency occurs when the value \(c\) stored in the cache for a formula \(\Sigma\) satisfies \(c \neq \left\|\Sigma\right\|\). This phenomenon is a byproduct of conflict-driven clause learning. While learned clauses are treated as part of the formula for \({\tt BCP}\), they are not necessarily part of the original local sub-problem \(\Sigma\). If a learned clause \(\alpha\) is derived from variables in \(Var (\Sigma)\) but is not a logical consequence of \(\Sigma\) (i.e., \(\Sigma \not\models \alpha\)), using \(\alpha\) to simplify \(\Sigma\) can result in an incorrect model count.

This issue is well-documented in the context of component caching [19]: when a sub-formula is found to be unsatisfiable, any cache entries added after the initial conflict must be invalidated. In a local solver, this cleaning is straightforward. In a distributed setting, however, sharing a sub-problem may prevent a worker from ever detecting the specific conflict that would have triggered a cache invalidation, leading to the propagation of “poisoned” results.

We demonstrate that such inconsistencies only arise in branches containing an unsatisfiable connected component, thus ensuring soundness.

Cache inconsistency has been addressed in distributed model counting. In CountAntom [21], the authors ignore the problem; however, their architecture differs. CountAntom manages a single global search tree at the Master, whereas our approach involves multiple workers independently constructing portions of the search space. In DMC, this issue does not arise because D4 invokes a SAT solver at every decision node to ensure branch satisfiability.

However, most modern model counters forgo satisfiability checks at every decision node to avoid computational overhead. This design choice complicates the direct integration of our distributed framework with such solvers, as unverified branches can lead to cache inconsistencies. Fortunately, this can be mitigated by ensuring that all connected components of an AND node are verified as satisfiable before the node is marked as eligible for sharing. While this introduces a cost exceeding standard BCP, the overhead remains negligible in practice because the solver is not invoked at every decision. Moreover, since work sharing is restricted to the upper levels of the search tree, the number of AND nodes requiring verification is relatively small. Consequently, the total number of calls to the SAT oracle is minimized, ensuring that these safety checks do not degrade global search performance.

4.3 Worker Invocation↩︎

Following the protocol established by DisCount [17], our framework invokes underlying model counters in assumptions mode, a technique derived from incremental SAT solving [22]. In this configuration, the sub-problem assigned to a worker is defined by a set of assumptions (literals asserted only for the duration of a specific solver invocation). This approach is particularly advantageous for distributed model counting as it allows the underlying solver to retain its internal state across successive tasks. Since the base formula \(\Sigma\) remains static, workers can preserve variable activity data and learnt clauses, which remain logically valid for any sub-problem derived from \(\Sigma\). Furthermore, maintaining a persistent component cache across multiple counting queries has been shown to be highly beneficial [23]. By utilizing incremental invocations, gDMCenables workers to reuse cache entries and variable weights, significantly accelerating the processing of related sub-problems.

Unlike distributed counters that treat each task as an isolated query, each worker in gDMCmanages a local collection of stacks. Upon receiving a sub-problem with a specific \(idTask\), a worker initializes a corresponding stack to track the search and any internal decompositions. Rather than returning partial counts immediately to the Master, workers accumulate these solved sub-stacks locally to avoid frequent transfers of large arithmetic values. Once the Master determines that the entire search space has been covered (signaled by all workers entering the idle state) it triggers the final reduction phase. During this phase, workers perform a decentralized reduction, propagating computed values back to the original victims via the stored \(idTask\) dependencies. This strategy minimizes network congestion and ensures that the final model count for the entire formula (\(idTask=0\)) is only resolved once all dependencies are satisfied.

5 Experiments ↩︎

Our framework is implemented in C++ as an extension of DisCount, leveraging concepts [24] and templates. We utilize concepts to define strict interfaces for the model counter, enabling seamless interchangeability of the stack manager and communication protocols. gDMC supports arbitrary-precision aggregation. Furthermore, this template-based architecture simplifies MPI integration by eliminating the need for invasive modifications to the solver’s build configuration. The source code and experimental logs are available on Zenodo (https://zenodo.org/records/20157902).

We use Glucose 3.0 [25] in incremental mode and FlowCutter [26] (PACE 2017) for tree decompositions (10s budget). Preprocessing utilizes B+E [27] with the equiv option (vivification, backbone, occurrence elimination). To prevent worker idle time caused by slow, serial definability checks, we limit this phase to 5 s. Finally, we upgraded SharpSAT-TD [13] to support incremental assumptions.

We evaluated our approach against state-of-the-art distributed model counters dCountAntom [16], dmc [18], and DisCount [17]. For a fair and accurate comparison, DisCount use SharpSAT-TD as the base solver. For our experiments, work-stealing requests are issued periodically every \(k=1,000\) decisions, and we do not share formulas with fewer than 30 variables. The benchmarks were taken from the most recent competition [14]. All experiments ran on a cluster of thirty-two Intel^® Xeon^® E5-2643 v4 CPUs at 3.30 GHz, with Rocky Linux 9.5 (Linux kernel 5.14). Nodes are connected by 1 GiB/s Ethernet. The software environment used GCC 11.5 and Open MPI 5.1.0a1. Finally, a wall-clock time limit of 900 seconds and a memory limit of 32 GiB were imposed on each run.

Figure 3 presents a cactus plot of solved instances over time for dCountAntom, DMC, DisCount, and gDMC. To assess the scalability of gDMC, we evaluated configurations of \(2, 3, 5, 9, 17, 33, 65\) and \(128\) cores. Since gDMC requires a dedicated master node, these configurations correspond to \(1, 2, 4, \dots, 64\), and \(127\) active workers, respectively. The competing solvers dCountAntom, DMC, and DisCount were executed using the full 128-core allocation.

The results demonstrate that increasing the core count significantly reduces the solving time for gDMC, maximizing the number of instances solved within the limit. In the 128-core comparison, dCountAntom is the least efficient (35 solved), followed by DisCount (104) and DMC (108), with gDMC achieving the best performance in both count and speed. Notably, contrary to findings in [17], DisCount trails slightly behind DMC in this evaluation. We attribute this discrepancy to two distinct factors. First, the increased difficulty of this year’s benchmarks hinders DisCount’s ability to effectively partition the search space into cubes. Second, DMC uses double-precision arithmetic, thereby avoiding the computational overhead of the arbitrary-precision arithmetic employed by DisCount.

Figure 4 compares solving times of DisCount and gDMC; points above the diagonal favor gDMC. gDMC solves more instances, evidenced by top-border points (DisCount timeouts), and is consistently faster. This gap widens with instance difficulty. We attribute this efficiency to two factors: gDMC avoids cube-generation overhead on simple instances, while dynamic work-stealing balances load on complex ones, mitigating the long-tail latency of static partitioning.

Figure 5 depicts the distribution of speedups achieved by gDMC as computational resources scale from 2 to 128 cores. The \(y\)-axis represents the speedup factor relative to a baseline configuration of 2 cores (1 master and 1 worker). For any instance solved in \(t_n\) seconds using \(n\) cores, the speedup is computed as \(\frac{\min(t_{\text{2}}, 900)}{t_n}\), where \(t_{\text{2}}\) is the baseline solving time. Since \(t_{\text{2}}\) is capped at the 900-second timeout, these reported values constitute a conservative lower bound on the actual speedup for instances that time out in the baseline configuration. The results demonstrate robust scalability. We observe a consistent upward trend in the median speedup (indicated by the orange line) as the number of cores increases, confirming that gDMC effectively utilizes additional worker nodes. Furthermore, the presence of high-performing outliers indicates that for many complex instances, the framework achieves near-linear speedups. This suggests that the dynamic work-stealing strategy successfully mitigates the idle time and communication overhead typically associated with distributed exact counting.

6 Conclusion and Perspectives ↩︎

In this paper, we presented gDMC, a generic, solver-agnostic framework for DPLL-style distributed exact model counting. By leveraging C++ concepts and templates, we decoupled distributed orchestration from the core solving logic, enabling zero-overhead integration with state-of-the-art counters like SharpSAT-TD. Our approach employs a novel point-to-group work-stealing strategy and a local aggregation mechanism that ensures soundness and cache consistency without the bottleneck of global result streaming.

Future work focuses on three key directions. First, we plan to integrate probabilistic counters such as GANAK. Second, we aim to exploit our solver-agnostic design for DPLL-style counters to implement a heterogeneous portfolio, running distinct solvers concurrently to dynamically leverage their respective strengths on sub-problems. Finally, we intend to evaluate the scalability of our architecture on high-performance computing clusters with thousands of cores, testing the limits of our synchronization protocols in massively parallel environments.

Acknowledgments↩︎

This work has been partly supported by the CERADOC project of the French National Agency for Research (ANR-25-CE23-3078), National Natural Science Foundation of China (No. 62532014), Jilin Province Science and Technology Department Project (20240602005RC), Scientific Research Project of the Education Department of Jilin Province (JJKH20250334KJ).

References↩︎