Streamlining Distributed SAT Solver Design

Over the last years, parallel and distributed approaches to propositional satisfiability (SAT) solving have gained significant traction and established themselves as powerful automated reasoning tools to conquer previously infeasible problems [22, 56]. In large parts, this success is due to careful exchange of conflict clauses that are learned by individual sequential SAT solver threads during their search [41]. Recent findings [56] indicate that such clause sharing can serve as its own powerful kind of parallelization, even if all solver threads are initially completely identical, challenging the predominant view that solver threads need to either explicitly operate on different sub-spaces (search space splitting) or be explicitly diversified in terms of their approaches (portfolio) [56]. In light of these new insights, we explore ways to improve both simplicity and performance of distributed SAT solving.

State-of-the-art parallel and distributed solvers commonly employ cutting-edge SAT solvers as sequential building blocks. These sequential solvers, most recently CaDiCaL [11] and Kissat [12] in particular, are highly engineered pieces of software optimized for sequential, general-purpose SAT solving performance [26]. To this end, they feature a large number of simplification or preprocessing techniques, some of which are heuristically scheduled into their solver program (inprocessing) [17]. In most established parallel solvers, these tasks are performed by all solver threads in a fully redundant fashion, with the exception of some coordinated preprocessing [21, 49] and disabling individual techniques for individual threads in the name of diversification [4, 55]. While inprocessing significantly improves sequential SAT solving performance [17], its impact for parallel and distributed clause-sharing solving is largely unexplored (cf. [20]). One notable caveat is that pre– and inprocessing tasks, performed redundantly at all solver threads, are not parallelized and can therefore present a scalability bottleneck. This holds especially if the effort spent on a pre–/inprocessing task is not a fixed, small share of each thread’s CPU time (e.g., 10%) but rather takes up large portions of the total, parallel CPU time – which we do confirm to be the case for some techniques. Another aspect is that simplification techniques often heavily modify the original formula. When two solvers operate on different representations of the problem, efficient and effective information exchange can be obstructed. For instance, Schreiber and Sanders noticed that bounded variable elimination (BVE) can prevent solver threads from importing many incoming clauses because the clauses feature variables that are locally already eliminated [56].

In this work, we diagnose and mend some of the mentioned shortcomings in modern distributed SAT solver design. A large portion of our contributions are of an analytical and observational nature. In particular, we profile the cutting-edge distributed SAT solver MallobSat [55, 56] in terms of the amount of time individual solver threads spend in different tasks. We observe that pre–/inprocessing provides little to no net benefit for distributed solving and that disabling it does in fact improve performance. Similarly, we complement recent findings [35, 50] questioning the significance of the Literal Block Distance (LBD) [2] metric for clause-sharing solving. We subsequently propose first improvements as a reaction to these insights: We implement a single-core preprocessing approach that runs while “pure” CDCL solving is already ongoing, remove LBDs from distributed clause sharing, and drastically cut diversification of solver threads down to two trivial methods (random seeds and variable phases). Our enhanced setup of MallobSat outperforms the prior state of the art, especially on application-oriented benchmarks, while only executing pure, uniform, clause-sharing-powered CDCL search at the parallel cores – further departing from a “portfolio solver”. Going forward, our results call for designing distributed SAT solvers in a more holistic and unified manner, whereas our proposed solving approach opens up new opportunities for understanding, analyzing, and advancing distributed clause-sharing SAT solving.

The paper at hand is structured as follows. Section 2 introduces relevant preliminaries and related work. Two empirical studies follow, first on examining pre–/inprocessing in distributed SAT solving (Section 3) and secondly on the role of LBDs (Section 4). In Section 5, we propose an alternative approach to integrating simplification techniques into distributed SAT solving in a more scalable manner. Section 6 features a thorough experimental evaluation. We discuss results in Section 7 and conclude our work in Section 8.

In the following, we provide some necessary background for the work at hand.

Given a propositional formula $F={\bigwedge }_{i=1}^n{\bigvee }_{j=1}^{k_i}{l}_{ij}$, where each $l_{ij}$ is a Boolean variable or its negation, the propositional satisfiability (SAT) problem is to find a variable assignment that satisfies $F$ or, if impossible, to report unsatisfiability [16]. Most sequential state-of-the-art SAT solvers are based on the Conflict-Driven Clause Learning paradigm [41], which encompasses a heuristic search over the space of partial variable assignments. When a CDCL solver encounters a logical conflict under its current assignment, it can derive a so-called conflict clause and add it to its knowledge base. Intuitively, such a clause represents a pruned sub-space of search space that has been deemed unsatisfiable.

In distributed computing, multiple machines with no shared memory perform a joint computation. They usually coordinate by exchanging messages over a network. Parallel and distributed approaches to SAT solving have mostly been separated into two major classes of approaches: search space splitting and portfolio solving [5]. Search space splitting (a.k.a. search space partitioning, divide&conquer, later cube&conquer [34]) was the earliest parallelization technique, forcing workers to search pairwise disjoint sub-spaces of search space. While this is situationally powerful [31, 33], load balancing problems can occur if the problem is split in an uneven or ineffective manner [57]. Portfolio solving has been proposed to circumvent these problems, instead aiming to achieve speedups by running many different sequential SAT solvers on the same, original, formula [30]. Both parallelization paradigms have been enhanced by clause sharing, i.e., mechanisms to exchange learned conflict clauses across workers [30, 58]. The result is a form of parallel search space pruning: If solver thread A learns clause $c$ and transmits it to thread B, then B will not re-explore the sub-space prohibited by clause $c$. This pruning is imperfect in nature since solver threads periodically forget (i.e., discard) clauses, losing pruning information in the process [2, 43]. Earlier works still showed that clause sharing is beneficial for performance of portfolios [4, 30] (resulting in clause-sharing portfolio solvers) and search space splitting solvers [58].

Modern distributed SAT solving systems include PRS [62], Painless [48], and MallobSat [55, 56], which generally fit the clause-sharing portfolio paradigm. MallobSat in particular features a highly engineered form of periodic all-to-all clause sharing. Its authors demonstrated that this clause sharing is the central driver of the system’s scalability. Notably, MallobSat performs rather competitively even if all solver threads are initially identical – down to the exact same seed – the reason being that individual threads import slightly different clause sets at slightly different points in time due to the non-determinism of the distributed program. This alone suffices for clause sharing to act as effective search space pruning [56]. While this finding does not immediately translate to a new distributed solving approach – usual diversification of solvers still benefits performance – it raises the question of whether the notion of clause-sharing portfolios still applies to a system that does not depend on any actual portfolio. Schreiber & Sanders suggested the term clause-sharing solver [56] to emphasize that clause sharing is, demonstrably, its very own kind of parallelization and should not be considered a mere supplement to portfolio solving or search space splitting.

We refer to the Handbook of Satisfiability [17] for an overview of pre– and inprocessing techniques. Regarding parallel pre- and inprocessing, Gebhardt et al. [27] presented a shared-memory parallelization of certain techniques including subsumption, clause strengthening, and bounded variable elimination (BVE). The scalability of this approach is rather limited due to the employed memory lock schemes. Wieringa et al. [60] showed that vivification-like inprocessing could be elegantly achieved in a parallel fashion by adding a second pure clause strengthening thread to each CDCL solver. The ParKissat system [61] applies some single-core preprocessing prior to parallel solving, including techniques to handle XOR and cardinality constraints, which was adopted by PRS [21] and subsequently by the state-of-the-art shared-memory solver PL-PRS-BVA-KISSAT [48]. The latter system also runs a number of bounded variable addition (BVA) [29, 40] threads next to CDCL [49]. The results from all but one BVA thread are discarded; other threads can seamlessly integrate the “winning” result in their ongoing CDCL search. To our knowledge, the solver threads in the mentioned systems still perform inprocessing during search, on top of the coordinated preprocessing.

Focusing on shared clauses, Vallade et al. [59] proposed to boost sharing efficiency by concurrently strengthening shared clauses since, in a parallel setting, these might be the most rewarding clauses to invest work in. They observed improved performance for unsatisfiable but negative results for satisfiable instances. Iida et al. [35, 36] recently tested several metrics for selecting clauses to share. In contrast to the older LBD metric [2], which depends on the solver state [3], their proposed metrics are based on the formula’s (static) graph structure.

Osama et al. [44] introduced utilizing GPUs for pre-/inprocessing, achieving speedups by more than an order of magnitude for garbage collection and gate detection. For variable elimination however, the speedups were limited to around 1.5, highlighting the difficulty of uniting the rather irregular program flow of SAT solving with monolithic GPU architectures.

In the following, we present and analyze running time profiles of a state-of-the-art distributed clause-sharing solver in order to gain insights in its behavior and directions for improvements.

We use MallobSat, essentially configured as in the International SAT Competition 2024 [51] but using only 2024 Kissat [12] as its solver backend. In the scope of this work, we decided to focus on a single cutting-edge solver backend (Kissat) in order to obtain clean results and keep the experimental design space more manageable. We use the HPC cluster SuperMUC-NG, where each node features a two-socket Intel Skylake Xeon Platinum 8174 processor clocked at 2.7 GHz with 48 physical cores (96 hardware threads) and 96 GB of RAM. For the following experiments, we use 16 nodes (768 cores), which amounts to a decently large scale and still allows us to run more experiments than we could at larger scales.¹¹1 We acknowledge that we spent a total of 709 880 core-hours for all experiments in the paper (including testing and debugging), which amounts to $\approx$2.3 tons of CO₂eq (320 g CO₂eq / kWh) – similar to the emissions caused by six economy passengers on a flight from Frankfurt to New York. The SAT’2021 Mallob paper [55] spent a similar amount of resources (also in the order of 700k ch). In order to obtain profiling results, we make use of Kissat’s integrated profiling capabilities: each solver thread bookkeeps the accumulated time it spends in relevant sub-procedures. Given that used CPU time is challenging to obtain asynchronously for a solver thread in MallobSat’s multi-threaded processes, we changed Kissat’s profiling to use wallclock rather than CPU time.

In terms of problem inputs, we need to balance responsible use of computational resources with instance diversity and robustness of results [51]. To ensure a great variety of benchmark families, we consider all 796 unique instances from the last two SAT Competitions, 2023 and 2024. We then reduce the resulting benchmark set to a random selection of 396 instances – reserving the remaining 400 instances for scaling experiments (Section 6).

Fig. 1 shows the ratio of time the solver threads spend in selected tasks for single-core Kissat (left) and for 768-core MallobSat (right) for each of the 396 instances. Fig. 2 (left) shows according statistics; more details are provided in the appendix (Tab. 2). First, it is worth mentioning that Kissat, as other sequential solvers participating in the SAT Competition, is tuned for running times up to 5000 s. At distributed scales, we usually aim for much lower running times on the order of 300 s [56]. For such time scales, the inprocessing scheduling may turn out suboptimal. We thus ran Kissat for up to 5000 s (vs. 300 s for MallobSat) to aggregate more representative statistics for it.

The label “search” in Fig. 1 denotes actual CDCL search, which is the only parallelized task (via clause sharing). Visually, the markers for sequential Kissat corresponding to search are strongly clustered at about 0.9, while they appear lowered and more scattered for distributed MallobSat. The total ratio of solver time spent in search is 86% for single-core Kissat but only 79% for 768-core MallobSat. By contrast, most pre–/inprocessing techniques [12] take proportionally more time in our distributed setting. Some of the most costly tasks are vivification [39], initial fast variable elimination (“fastel”) and, to a lesser extent, congruence closure, SAT sweeping, and variable elimination during inprocessing. For example, the relative cost of vivification increases from 7% at one core to 8.4% at 768 cores, possibly because of the increased number of vivification candidates due to clause sharing.

Other techniques however, such as initial variable elimination, do not follow this logic and are expected to incur a fixed amount of work. At a distributed scale, where CDCL search profits from speedups, the redundant and non parallelized preprocessing on all cores accounts for increasing portions of the total work performed (from 0.3% to 2.96% for “fastel”). SAT sweeping is an exception to this effect (relative cost decrease from 2.18% to 1.54%), the probable reason being that it only incurs significant relative cost at very low running times ( s), where MallobSat performs similar or even worse than sequential Kissat. Also note how some tasks such as vivification use relatively consistent shares of time since Kissat can control their computational budget in an accurate manner. Other tasks that are highly dependent on problem structure, such as initial variable elimination, show high variances in the time spent and occasionally even account for the majority of compute time.

The impact on solving performance is shown in Fig. 2 (right). We ran MallobSat as before and also in a search-only configuration where pre– and inprocessing is disabled for all threads. At a sequential scale, Kissat with pre–/inprocessing significantly outperforms its search-only variant, as one would expect. At 768 cores, however, many instances are slowed down by the cost of preprocessing and simplification. As such, our “search-only” setup achieves a geometric mean speedup of 3.7% over the default setup (computed over commonly solved instances) and solved 12 more instances. Let us discuss some potential causes for this effect:

• $\mathrm{■}$

  As presented above, certain pre–/inprocessing techniques can constitute a large share of the total (parallel) work performed, whereas their merit remains constant regardless of the number of cores computing it. Due to this scalability bottleneck, the techniques incur increasing opportunity cost that eventually outweighs their benefits: Our search-only setup raises the share of time spent on search from 79.15% to 95.4% (appendix Tab. 2).

• $\mathrm{■}$

  Clause sharing may functionally “simulate” certain pre–/inprocessing techniques to some degree. This is plausible for techniques related to identifying short clauses that are implied by the input formula, such as subsumption or vivification: Since MallobSat’s clause sharing aggregates the globally shortest distinct clauses [56], it may become unlikely that vivifying a clause results in a shorter clause that no other solver thread has found so far. That being said, we are yet to find specific evidence for (or against) this suspicion.

• $\mathrm{■}$

  Deviating preprocessing levels across solver threads may result in “language barriers” across solvers, hindering cooperation and rendering clause sharing less effective. This may especially apply to techniques eliminating variables, which restrict the clauses that a solver thread can subsequently import [56]: In our 768-core experiment with pre–/inprocessing, the geometric mean ratio of incoming clauses that were imported successfully by a solver thread is 62%. The median ratio is higher (75%) since every tenth solver thread is configured to skip variable elimination completely and can therefore import all clauses. Still, about 22% of solver threads could import less than half of their incoming clauses.

In terms of benchmark families [37], we observed that pre–/inprocessing is most beneficial for unsatisfiable miter instances (i.e., combinational circuit equivalence checking; nine instances with mean speedup 3.4 and two more instances not solved by “search-only”), which is unsurprising since Kissat’s SAT sweeping and congruence closure are designed for this exact application [13, 14]. Notable benchmark families where the search-only setup performed better include satisfiable instances on scheduling (9 instances, speedup 1.59) and Folkman graphs (5 instances, speedup 1.83). For the latter, the mean time ratio spent on CDCL search increases from 89.1% to 99.2% when disabling pre–/inprocessing, mostly due to vivification (7.7%). Additional family-specific results are given in the appendix (Table 3).

All in all, the presented results paint a clear picture: Pre– and inprocessing techniques are currently being employed in distributed SAT solving in a suboptimal manner. They are neither designed nor tuned for clause-sharing solving and incur significant cost which limits the attainable speedup and, in many cases, outweighs their benefits.

In sequential solving, the Literal Block Distance (LBD) of a clause indicates the number of distinct decisions involved in the according conflict [2]. LBDs have proven useful as a quality metric, i.e., to decide whether to keep or to discard a clause [43]. LBDs have also been used in many parallel SAT solvers [1, 4, 25, 38] as a metric to decide which learned clauses a solver unit should contribute to clause sharing. However, the usefulness of LBDs does not necessarily translate to parallel clause sharing: A clause’s LBD depends on the solver state and may thus not be meaningful to a different solver (thread) [3]. As recently evidenced, using LBD as a clause selection metric is not beneficial compared to clause length [35, 55]. MallobSat currently uses LBDs only as a tie-breaker, after clause length, when prioritizing clauses to share. Its authors also reported very similar performance for different ways of manipulating the LBD values of incoming shared clauses, just before a solver thread imports them [56]. However, some of the underlying tests have the potential flaw that they do not only change individual LBD values but also their overall distribution. This distribution can be relevant since it influences the volume of kept clauses and, therefore, the propagation speed and search behavior. Changing it, e.g., by assigning random LBD values to incoming clauses, may thus result in side effects which improve or degrade performance.

In the following, we examine two aspects of LBDs in distributed solving separately: The significance of a particular incoming clause carrying a particular LBD, and subsequently the distribution over the LBDs of incoming clauses.

To reexamine the significance of individual LBDs, we suggest the following experiment: After globally aggregating all clauses to share, we shuffle the mapping of clauses to LBD values within each clause length uniformly at random. As such, we can cleanly observe the effect of disconnecting LBDs from their meaning while the distribution over LBD values in solver threads remains fixed.

As Fig. 3 shows, we were unable to discern any meaningful differences in solving performance with vs. without shuffling of LBD scores: Shuffling LBD scores resulted in one additional solved instance (290 vs. 289) and a speedup of 1.27%. This complements recent evidence [35, 56] that communicating and forwarding the LBDs of individual shared clauses does not carry any useful information in parallel clause-sharing.

Given that individual LBD values do not appear to be of any significance, let us now separately evaluate the impact of different distributions over incoming LBD values. Specifically, we explore different strategies to fabricate LBDs synthetically. For a synthetic distribution to be sensible, our intuition is that high-LBD clauses should be more frequent, low-LBD clauses should be rare, and min-LBD clauses (LBD 1 or 2) should be avoided, reflecting the typical three-tier clause management in modern solvers [15, 43]. We refrain from assigning min-LBD clauses because solvers commonly keep them indefinitely, which may lead to overcrowding if too many such clauses arrive from external sources [56]. We compare four strategies:

1. 1.

   Original LBDs: The original LBD values are kept, used as a secondary clause sharing selection metric (after clause length), and incremented upon import [56].

2. 2.

   Deactivated LBDs: When a clause is produced, its LBD value is set to its maximum value possible [24], the size of the clause. This functionally deactivates any logic related to LBDs in the distributed solver.

3. 3.

   Uniform LBDs: When a clause is produced, its LBD value is set to its maximum. When a clause is imported and its size is $|c|\ge 3$, the importing thread randomly draws a new LBD $\in [3,\mathrm{\dots },|c|]$ with uniform probability for each value. Initially setting LBDs to their maximum ensures that they play as little a role as possible during clause sharing.

4. 4.

   Triangular LBDs: When a clause is produced, its LBD value is set to its maximum. When a clause is imported and its size is $|c|\ge 3$ the importing thread randomly draws a new LBD $\in [3,\mathrm{\dots },|c|]$ whereas each LBD value $s$ has a probability weight of $s-2$. Visually, the probability density resembles a triangle; low LBDs receive a lower probablity to be sampled and high LBDs a higher probablity. This distribution produces fewer low-LBD clauses than the uniform distribution, which could affect the clause databases.

We ran each of these four strategies on 396 instances with a timeout of 300 s, distributed on 768 cores. We also deactivate all other sources of diversification (random seeds and sparse random variable phases [4]), as in ref. [56], such that any diversification introduced by just the LBD settings would be most observable. Results are shown in Fig. 4. Overall, all strategies performed similarly; best performance is achieved by using and incrementing original LBD scores or by removing them from the equation entirely. We were unable to observe any positive diversification effect due to randomized LBD scores in the triangular and uniform strategies. We suspect that these two strategies may still result in too many low-LBD clauses, at least at the tested scale and with MallobSat’s default sharing configuration.

Put together, we found that removing LBD scores from clause sharing alltogether (and assigning the maximum LBD score to each incoming clause during import) preserves performance. Together with earlier findings [35, 56], this paints the clear picture that LBDs are not a useful metric for modern clause-sharing solvers. Going forward, we consider to either replace LBD with a different metric, as proposed by Iida et al. [35], or to remove them entirely from MallobSat’s solver interfaces and sharing logic.

Our profiling results (Fig. 1–2) have shown that distributed clause-sharing solving performs pre– and inprocessing in a highly suboptimal manner. We now suggest some first improvements to this situation, incorporating insights from the above discussion and measurements. We can discern several general approaches for any single pre–/inprocessing technique:

1. 1.

   Keep the technique as is, i.e., computed redundantly by all threads. This (non-)approach can be sensible if the technique consistently incurs little cost.

2. 2.

   Disable the technique. This is reasonable especially if the technique is fairly expensive and is difficult or even infeasible to parallelize, or if it causes negative side effects for the parallelization. An example is variable elimination during inprocessing, which prevents the import of many clauses if not performed in a synchronized fashion [56].

3. 3.

   Sequentially apply the technique with a single solver thread, then distribute the result. This can be a practical compromise for techniques that are challenging to parallelize, feasible to perform sequentially in little time, but still costly if performed by all threads.

4. 4.

   Parallelize the technique. This can be an option if the technique is beneficial in a distributed setting and if it is expensive sequentially but feasible to parallelize. While there have been some works in this regard (see Section 2), so far next to no techniques have been explored in the context of state-of-the-art distributed SAT solving.

MallobSat’s default configuration follows options 1 (for most threads) and 2 (for some threads, for the sake of diversification). In the long term, we are interested in finding scalable parallel algorithms for promising inprocessing tasks (option 4). In the scope of this mostly empirical work, we consider options 2 and 3 to obtain a more scalable distributed solver.

Specifically, we propose the following changes to MallobSat’s setup: We drop all pre– and inprocessing, which, for the case of Kissat, amounts to disabling the options preprocess, simplify, probe, and lucky. Since many of MallobSat’s native diversification options for individual solver backends [56] concern specific pre–/inprocessing techniques, we also completely disable this native diversification. This results in a “pure” clause-sharing solver with uniform worker threads (Fig. 5 right) and next to no characteristics of a portfolio (Fig. 5 left). We then configure a single thread to perform a single run of a number of crucial simplification techniques – similar to the preprocessing performed by PRS and PL-PRS-BVA-KISSAT (see Section 2) and also how the early portfolio solver Plingeling used to handle preprocessing [6].²²2 In a sense, Plingeling’s “preprocess-then-fork” model has gotten buried due to HordeSat’s [4] slim and modular solver interface, prohibiting this mode of usage when integrating Plingeling’s solver diversification, and thus never found its way into HordeSat and later MallobSat. Our approach differs in that all distributed resources are tasked immediately with search-only SAT solving as long as preprocessing is still ongoing. In terms of employed preprocessing techniques, we use the out-of-the-box preprocessing capabilities of Kissat, which includes not only bounded variable addition but also congruence closure and SAT sweeping, fast initial variable elimination, backbones, and lucky phases [12].

Once completed, the preprocessor reports the entire preprocessed formula. Since our execution environment Mallob natively supports concurrent execution and flexible load balancing of SAT solving tasks [47], we can simply introduce the preprocessed formula as an additional task that runs next to the original solving task. This raises the question of how to distribute the available computational resources among these two tasks. Assume that the original task $j_o$ has been running for time $t_o$ whereas the preprocessed task $j_p$ has been running for time $t_p$. Given equal time and resources, we assume that the preprocessed task is likely to be easier to solve. Therefore, as $\frac{t_p}{t_o}$ increases and eventually approaches 1, the relative worth of $j_p$ over $j_o$ increases. Following up on this intuition, we suggest to gradually shift computational resources from $j_o$ to $j_p$ until only a single process for $j_o$ is remaining. Eventually, $j_o$ is interrupted completely. A result is reported if the preprocessor manages to solve the formula directly or when either $j_o$ or $j_p$ report a result. A satisfying assignment reported by $j_p$ must be converted to a satisfying assignment to the original formula, using the preprocessor’s data structures for solution reconstruction.

In the following, we provide an evaluation of our improvements.

First of all, we examine the impact of different sources of solver thread diversification. Our search-only setup with prior single-core preprocessing only features a single solver backend (Kissat) and no longer features a hand-crafted sequence of solver configurations that are being cycled over (cf. [55]). This drastically cuts diversity and leaves what can be characterized rather as a uniform array of CDCL searchers than a classical “portfolio” (Fig. 5). In our study on LBDs (Section 4), we found that the diversification introduced by deviating LBD distributions across solver threads does not influence performance even when all other sources of diversification are disabled. We thus follow the “Deactivated” LBD strategy in our new setup. Two other computationally cheap, basic, and uniform diversification techniques we consider are setting different random seeds and variable phases per solver [4, 56]. We thus ran our baseline without any diversification, with seeds only, and with seeds and phases.

Results are reported in Fig. 6. While MallobSat still performs well without any explicit diversification – an effect examined in detail in ref. [56] and attributed to deviating clause imports across solver threads – we see that different random seeds are beneficial for short running times, especially below 10 s. Random seeds essentially provide a warm-start for deviating search behavior rather than having to wait for diversity induced by the first few clause imports. This contrasts randomized LBDs, which can only have any impact after the first sharing(s). Randomized phases only have a minimal effect, but still lead to a net positive and incur no opportunity cost. We also explored some additional diversification, such as randomizing VSIDS score decays or clause database reduction ratios, without observing significant improvements; according results are given in the appendix (Fig. 12–13).

Next, we evaluate different strategies surrounding our single-core preprocessing. An overview is provided in Fig. 7. First, adding sequential preprocessing to an otherwise search-only run and launching a task $j_p$ that operates on the preprocessed formula is highly beneficial to performance. The run with preprocessing solves 19 additional instances and improves performance for several unsatisfiable instances (which incur much less running time variance than satisfiable instances). The preprocessor solved 18 instances directly and mostly finishes in few seconds. Secondly, rather than allotting equal resources to $j_0$ and $j_p$ (as in the prior run), we gradually shift resources from $j_0$ to $j_p$, over a time span corresponding to twice the preprocessor’s running time, and then remove $j_0$ entirely. For long running times, this approach is preferable for unsatisfiable instances since it eventually commits all available resources to a single task. Next, we evict $j_0$ immediately as soon as $j_p$ enters, which results in mildly worse performance (2.4% mean slowdown), indicating that $j_o$ occasionally solves an instance after the arrival of $j_p$. Lastly, omitting $j_o$ entirely, thus deferring distributed solving until a preprocessing result is available, clearly performs worse (14.7% slowdown).

We continue our experiments with the “shift” strategy since it assumedly results in the best scalability in the long term (i.e., eventually allotting all resources to a single task) while not immediately discarding the progress made by the plain searcher task.

We now assess the scaling of our streamlined setup, using the 400 remaining, previously unused instances from the 2023–2024 benchmark sets. We use 1–64 nodes (48–3072 cores), doubling the number of nodes at each step. As points of reference, we use two state-of-the-art configurations of MallobSat: Only running Kissat (“K”), and running Kissat, CaDiCaL, and Lingeling alternatingly (“KCL”). The first configuration is the (prior) single-solver configuration with assumedly best general-purpose performance whereas KCL corresponds to the version of MallobSat submitted to the 2024 SAT Competition Cloud Track (which it won). Notably, the inclusion of Lingeling [7, 9] is known to noticeably boost performance on the 2023–2024 benchmark sets due to some peculiar instances which can be solved immediately by Lingeling’s cardinality constraint reasoning [10] (see also [52]). This circumstance provides KCL with a distinct advantage over Kissat-only configurations in terms of solving performance metrics. Due to native diversification, roughly 13% of solver threads in the K and KCL setups run without or with significantly reduced pre– and inprocessing.

Fig. 8–9 show the scaling behavior of the three considered configurations, with precise statistics given in Tab. 1. In terms of baselines, we included the performance of sequential Kissat (winner of the SAT Competition 2024 Main track) and of PL-PRS-BVA-KISSAT [49] (“painless-2” in SAT Competition 2024, winner of the Parallel track) executed at 48 cores. All configurations of MallobSat show consistent performance improvements up to the largest scale considered (3072 cores). The out-of-the-box Kissat-only configuration results in the worst performance. Notably, it features neither cardinality constraint reasoning (as in Lingeling) nor any reasoning beyond general resolution (as in bounded variable addition, which is part of our preprocessing). The diverse Kissat–CaDiCaL–Lingeling portfolio improves performance substantially (25.8 PAR-2 score points at 3072 cores). Our approach, in turn, outperforms all other approaches, achieving the lowest PAR-2 scores at all scales.

The performance margin to KCL is the smallest at 3072 cores, and mean speedups are consistently the highest for KCL. This raises the question whether we are observing a distinct scalability limit of our new approach. A direct comparison of the runs at 3072 cores (Fig. 10) suggests that this is not the case: Compared to both K and KCL, our approach clearly tends to perform better as running times increase. A distinct advantage of the KCL setup is that it solves a number of unsatisfiable instances in the sub-second range which are challenging or even infeasible to solve with Kissat only. At 3072 cores, we identified 17 such instances; all of them are in fact solved by a Lingeling solver thread. The concerned instances are eleven register allocation graph coloring problems [28], four Tseitin formulas [19], and two Pidgeon hole problems [8]. Our approach compensates for this disadvantage with generally better scalability, solving other instances which KCL fails to solve; however, at the largest scale, our approach runs out of such instances while KCL manages to close the gap.

A second advantage of KCL is the dedicated Stochastic Local Search solver YalSAT [9] in Lingeling’s portfolio. KCL outperforms our new setup by a factor of $\ge 5$ for 21 satisfiable instances; 18 of them were solved by a Lingeling instance, and 14 of them specifically by YalSAT. This includes seven instances surrounding Folkman graphs [32] and six set covering problems [63]. On the flipside, our new approach performs remarkably well on many benchmarks adjacent to real-world applications (see also appendix Tab. 4), such as bitvectors (4 instances, 67% mean speedup over KCL), verifying floating-point commutativity (6$\times$, 66%), hashtable safety (7$\times$, 48%), software (5$\times$, 38%) and hardware verification (7$\times$, 38%), school timetabling (9$\times$, 26%), and hash function properties (18$\times$, 23%). We attribute this success to our streamlined solver design (cf. Fig. 2); while KCL is missing BVA, this technique is highly unlikely to cause such scaling improvements on such kinds of instances [29].

The overall, direct geometric mean speedup of our configuration over KCL at 3072 cores is 0.815 (i.e., a slowdown). Removing the 17 instances solved immediately by Lingeling results in a speedup of 0.907 (still a slowdown). When we additionally remove the 14 instances where YalSAT found a solution $\ge 5\times$ faster than our approach did, the speedup is 1.036.

Fig. 11 provides insights into MallobSat’s weak scaling for the “K” baseline and our new setup (cf. [56]). Intuitively, the further right a curve goes, the more difficult are the instances that we consider for computing the mean speedup. We measure “difficulty” in terms of the sequential baseline’s running time. For example, our approach at 3072 cores reaches a speedup of 315.1 for instances that took sequential Kissat at least 1 h to solve, which corresponds to a resource efficiency of $315.1/3072=10.3\%$. Under the same circumstances, the baseline configuration “K” achieves a speedup of 299.8 (resource efficiency 9.8%). The KCL portfolio (not shown³³3 The weak scaling as we compute it heavily depends on the sets of instances a certain approach is able to solve. The weak scaling curves of the KCL configuration are therefore difficult to compare to the other configurations due to the different kinds of instances solved (mostly by Lingeling/YalSAT). We do provide a weak scaling plot of the KCL configuration in the appendix (Fig. 14). ) results in the best weak scaling, with a speedup of 451.5 and an according resource efficiency of 14.7%. This discrepancy can be explained by the fact that KCL performs noticeably better than our new approach in the first 10–20 s of solving, for reasons discussed above (i.e., due to Lingeling and YalSAT). The corresponding short running times cause relatively high speedups. In terms of total speedups (Table 1), which emphasize longer running times, our approach consistently achieves the best results.

In the following, we provide a brief discussion of the obtained insights and results.

Our work results in a slimmed down and yet competitive solver system. Let us attempt to provide a coarse quantitative estimate of the achieved reduction by considering the involved lines of code. We counted roughly 25k effective lines of code (ELOC; disregarding blank lines and comments) in Lingeling’s main source file lglib.c, 30k ELOC in CaDiCaL’s source files (*.cpp) and also 30k ELOC in Kissat’s source files (*.c). We estimate that roughly 20k ELOC of the Mallob system are in use. Our changes to Mallob amount to few hundred lines of code. Going by these measures, our setup reduces the code to be considered from 105k ELOC to 50k ELOC. Moreover, the code executed by the parallel solver threads decreases by roughly 13k ELOC (when excluding Kissat’s source files related to pre–/inprocessing). While these measures are not fully reliable (as each solver backend already features some unused code), we believe it is safe to assume that our changes to MallobSat cut the lines of executed code roughly in half and drastically reduce the solver program executed in parallel.

Comparing our setup to MallobSat’s KCL portfolio, we noticed some remaining shortcomings of our somewhat radical approach, mostly due to foregoing dedicated Stochastic Local Search (SLS) threads and due to missing special techniques for certain hard inputs. This motivates us to (a) reintegrate SLS in our approach, which presents only a minor increase in complexity (especially in terms of information flow), and (b) to integrate advanced preprocessing techniques (as in ref. [61]) that are required to conquer the kinds of instances which our current setup still struggles to solve. Specifically, our new approach to preprocessing can be adapted well to preprocessors that exploit advanced proof systems, such as extended resolution (which our preprocessing already features via bounded variable addition) [29], symmetry breaking (e.g., BreakID [18, 23]), or propagation redundancy (e.g., PReLearn [46]). Following our evaluation, we have made first simple steps in this direction by adding Lingeling’s preprocessing and 5% YalSAT threads to our setup; we observed significantly improved performance at a shared-memory level (see appendix Fig. 15).

On a related note, transferring our findings to a CaDiCaL-only setup within MallobSat will allow to exploit MallobSat’s proof production and checking capabilities (which, as of now, rely on CaDiCaL’s LRUP proof output [45]). While it appears challenging to generalize distributed proof production [42] and real-time checking [52] to proof systems beyond resolution, our pragmatic approach to preprocessing allows to “outsource” advanced reasoning to a strict, sequential prefix of the distributed solver’s reasoning, which could greatly facilitate combining scalable proof technology with modern proof systems.

Lastly, and perhaps most significantly, the presence of a competitive “pure” clause-sharing solver may have notable consequences for future research in parallel and distributed SAT solving. Rather than assuming a gathering of diverse and opaque reasoners who periodically exchange insights [56], we may now rather accurately consider the central building block of modern parallel SAT solving to be a uniform parallel CDCL procedure, parallelized by clause sharing. This more precise and transparent algorithmic model lends itself for establishing new theory, heuristics, and algorithms surrounding parallel SAT solving.

In this work, we investigated modern distributed clause-sharing SAT solver design. In particular, we empirically confirm earlier suspicions [20] that such distributed solvers are being held back by performing non-scalable tasks fully redundantly, such as pre– and inprocessing techniques. We also show conclusively that LBD values have no measurable significance for MallobSat’s distributed clause sharing. At the same time, we show that sequential preprocessing employed next to search-only solving can still greatly benefit distributed solving. Our practical result is a clean distributed clause-sharing solver whose solver threads are “pure” CDCL solving engines with very lightweight and uniform diversification. This system is able to achieve competitive performance, even compared to a mixed portfolio consisting of many different search strategies and advanced reasoning techniques.

In terms of future work, we intend to explore scalable algorithms for selected pre– and/or inprocessing tasks, such as vivification, variable elimination, or SAT sweeping. Distributed computing may allow for much more powerful simplification procedures while the parallel search logic could remain separate, uniform, and fully scalable. Orthogonally, we intend to retrofit our new setup from this work to MallobSat’s CaDiCaL backend, which (as of yet) is MallobSat’s only modern engine for incremental SAT solving [53] and for proofs of unsatisfiability [42, 52]. Lastly, it may be promising to allow sharing (certain) clauses between an original task $j_o$ and a preprocessed task $j_p$, since this may allow to transfer made progress from $j_o$ to $j_p$ following preprocessing.