In the context of parallel SAT solving, eficient information sharing plays a pivotal role in improving the performance. Traditionally, this information comprises the clauses learned by the underlying sequential solvers of the parallel strategy. This paper investigates the integration of existing sharing strategies and proven heuristics into parkissat-rs, a parallel solver using the kissat sequential engine. The investigation focuses on evaluating the trade-ofs between dedicating a core to solving the formula and optimizing the sharing mechanism. We evaluate diferent configurations of parkissat-rs, using additional threads for sharing, a dynamic threshold for clauses filtering, a dedicated thread for strengthening shared clauses, and a mechanism to prevent the sharing of duplicate learned clauses. We also performed a scaling study on a subset of the parameters. These extensive experiments conducted on the SAT 2022 main track benchmark demonstrate the efectiveness of the derived solvers, especially on UNSAT instances.
[
Over the years, p-mcomsps’s sharing mechanism has undergone incremental improvements with multiple options. Some options involve simple decision heuristics, while others require dedicated execution units (threads). Since we intend to use a solver with diferent sequential algorithms and diversification mechanism, we need to evaluate the trade-ofs between dedicating a core to solving the formula versus optimizing sharing.
We evaluate various configurations of parkissat-rs with the following options: (i) employing additional threads to handle sharing, thereby increasing the bandwidth of learned clauses; (ii) utilizing a dynamic threshold for the Literal Block Distance measure; (iii) introducing a dedicated thread for strengthening the exchanged clauses; (iv) implementing a mechanism to prevent the sharing of duplicate learned clauses.
We show that option (i) alone is suficient to significantly improve performance on SAT instances. However, for better results on UNSAT instances, option (ii) must be activated and it combines well with options (iii) and (iv), albeit without spectacular improvements.
Furthermore, we present some insights into the results through a scaling experiment performed on machines with 32, 48, and 64 cores. We demonstrate that the solving times of SAT instances decrease as the number of cores increases, while the solving times of the UNSAT instance do not decrease beyond 48 cores.
The structure of the article is as follows: Section 2 describes the architecture and specificities of the parallel solver parkissat-rs. Section 3 outlines the framework and methodology employed in the study. The options integrated into the sharing policy are discussed in Section 4. Section 5 discusses some scaling results and Section 6 presents the concluding remarks of the paper.
In this section, we present parkissat-rs (see Figure 1), a state-of-the-art parallel (portfolio) solver that utilizes shared memory-based communication among the underlying sequential solvers. As the winner of the parallel SAT competition in 2022 by a significant margin, this customized portfolio of kissat solvers has proven to be highly efective. The diversification mechanism of parkissat-rs randomizes the branching order of variables for each solver in the portfolio, supplemented with the options provided by kissat, the underlying solver. PF
Additionally, several preprocessing and in-processing methods have been developed to guide the solver at the beginning or during the resolution process.
Furthermore, parkissat-rs implements a policy for sharing learned clauses. Initially, each solver places all the clauses it has learned with a Literal Block Distance (LBD) value less than or equal to 2 into an export bufer. Then, a dedicated sharing thread called Sharer retrieves the clauses from all export bufers and distributes them to the import bufers of all solvers. The sharing process is performed asynchronously, thereby avoiding contention on locks since each bufer is only accessed by two threads: the thread responsible for sharing the clauses and the Sharer thread. The sharing thread performs this operation every 0.5 seconds, and to control the bandwidth of shared data, it only shares 1500 literals per sharing round.
In Section 4, we will incrementally introduce various mechanisms to enhance the sharing policy of the aforementioned architecture. We will analyze the impact of these mechanisms on the performance of the platform.
Here, we present the methodology employed to evaluate the potential combinations of options, as well as provide a detailed overview of the experimental platform.
Hardware The experiments were conducted on a cluster consisting of Intel Xeon Silver 4216 processors, equipped with 32 cores and 384 GB of RAM. The solvers were executed with a timeout of 5000 seconds and a memory limit of 256 GB.
The benchmark We executed our solver on the main track of the SAT 2022 competition, which comprises a minimum of 171 SAT instances and 187 UNSAT instances, as per the competition results. Consequently, we divided the results into two separate tables: one for SAT instances and another for UNSAT instances. However, we excluded the 42 instances with UNKNOWN results, both as reported by the competition and observed in our experiments, from the tables. PF
SW ...
SW SW SW ...
SW SW
Kissat ... Performance evaluation Our objective is to compare the performance of each solver with the Virtual Best Solver (VBS), which is composed of the best results achieved by any solver for each instance. We assess the solvers based on their execution time and the number of instances solved. In each table, we present the performance of a solver alongside the number of cores dedicated to the CDCL algorithm.
Since we aim to utilize all available physical cores on our test machines and certain options require a dedicated thread, some configurations involve sacrificing a physical core used for CDCL (as in the original version, parkissat-rs) in favor of the specific option.
The tables include the following data: • The "CDCL" column indicates the number of CDCL cores utilized in the portfolio. • The "Total Runtime" represents the cumulative runtime of the solver.2 • The "Instances Solved" denotes the number of instances successfully solved.
In this section, we introduce various enhancements to the sharing mechanism of parkissat-rs and examine their performances. Each improvement is individually studied, as well as in combination with others, as they can have both quantitative and qualitative efects on clause sharing. Additionally, these mechanisms come with associated resource costs, making it crucial to investigate their potential side efects on each other.
To streamline the presentation of the results, we have opted to incrementally incorporate each studied mechanism. Towards the end of the section, we will present all the possible combinations. The resulting solver is named P-[options] for clarity and reference.
The first option we introduce to the sharing policy is the concept of multiple production groups. A production group comprises a set of solvers as producers, all solvers in the portfolio as consumers, and a dedicated Sharer thread running on a specific physical core.
The original implementation of parkissat-rs utilizes one production group (referred to as P-1G in the tables). To enhance the throughput of shared clauses, we incorporate a second production group: half of the solvers in the portfolio act as producers for one group, while the other half act as producers for the other group. This updated configuration is referred to as P-2G.
While the proposed mechanism is fully customizable and allows for additional groups, preliminary tests on our test machine have shown performance degradation when using more than 2 groups. The increase in the number of physical cores dedicated to diferent threads becomes too significant. Figure 2 shows the final architecture after incorporating all the options (P-2G-horde-str-dup).
Table 1 compares P-1G and P-2G. We observe that using two sharing groups yields improved performance on SAT instances, with three additional instances solved. However, there is no performance improvement for UNSAT instances. Although P-2G loses one instance, the runtime is nearly equivalent, indicating that P-1G is not significantly faster.
The second Sharer enables faster sharing of clauses, leading to a more rapid utilization of the shared clauses. However, since the strategy only shares clauses with an LBD value less than or equal to two, the impact of these shared clauses is limited.
The -horde option enables the Sharer to dynamically adjust the LBD threshold for individual
producers based on an estimation of whether they are sending too few or too many clauses.
This mechanism allows for better control over the sharing of clauses. It is worth noting that
this sharing strategy is an improvement of the one developed in [
Table 2 presents the performance results of using the -horde option with P-1G and P-2G. Although this option appears to slightly degrade the performance for SAT instances, specifically with P-1G-horde losing two instances compared to P-1G, a closer examination of the runtime indicates that P-1G-horde overall achieved faster execution.
On the other hand, the -horde option delivers significant performance gains for UNSAT instances, with both solvers benefiting from up to five additional solved instances.
The key insight from this experiment is that clauses with an LBD greater than two prove to be highly valuable for solving UNSAT instances. Notably, the -horde option performs on par with the VBS in solving UNSAT instances.
The -str option activates the reducer component, which implements an asynchronous clause strengthening algorithm. The purpose of this option is to enhance the unit propagation (UP) procedure by reducing the size of received learned clauses. The reducer operates within a production group and attempts to minimize the size of the clauses received from the solvers Solvers VBS P-2G P-2G-horde P-1G P-1G-horde
CDCL 28 30 31 30 28 30 31 30
TIME 42H39 45H13 45H14 45H42 46H03 48H43 53H07 54H42 54H46 within the group. Successfully reduced clauses are then sent back to the solvers. Since the reducer is computationally intensive, a dedicated core is allocated for its execution.
The theoretical basis of this strengthening technique is presented in [
A previous evaluation demonstrated that a similar architecture reduced the size of one third of
received clauses by a quarter [
Table 3 presents the performance results of the -str option. We can observe that the integration of this option yields consistent improvements for UNSAT instances across all the previously defined configurations, either in terms of running time or the number of solved instances. Notably, the P-2G-str configuration outperforms the P-2G configuration in terms of the number of solved instances.
However, for SAT instances, the impact of the -str option is generally negative, as three out of four configurations experience performance degradation. The P-1G-horde-str configuration appears to be an anomaly, which could be attributed to the inherent randomness afecting the solver’s behavior.
In summary, assigning a core that was originally dedicated to executing CDCL to the execution
of the reducer component proves to be highly beneficial for solving UNSAT instances but has an
adverse efect on SAT instances. These findings align with the results of experiments conducted
in [
In a parallel context, it is common to encounter many identical clauses that are learned by diferent CDCL solvers. Sharing these duplicates among solvers can be detrimental to the parallel solver’s performance.
To address this issue, it is beneficial to develop a mechanism that detects and rejects the sharing of duplicated clauses. However, such a mechanism comes with a cost that can potentially impact the sharer’s performance. Therefore, it is crucial to ensure that the number of duplicate clauses is significant enough to justify the trade-of.
The study depicted in Figure 3 examines the percentage of duplicates originating from CDCL solvers (Global duplicates) and from the reducer (after the strengthening phase). Each dot in the plot represents the percentage for a specific instance 3.
Solvers VBS P-2G P-2G-horde P-2G-horde-str-dup P-1G-horde-str P-2G-str P-1G P-1G-horde P-1G-str-dup P-1G-horde-dup P-1G-str P-1G-dup P-2G-horde-dup P-2G-horde-str P-2G-dup P-1G-horde-str-dup
The study reveals that CDCL solvers generate between 0% and 10% duplicates. On the other hand, the reducer produces a substantial number of duplicates across a larger number of benchmark instances. This analysis motivates the introduction of a duplicate removal mechanism.
Implementing such a mechanism requires tracking the already shared clauses. However,
storing all clauses perfectly would be memory-intensive. Therefore, we chose to implement a
space-eficient probabilistic approach using Bloom filters [ 8]. The sharer is enhanced with a
Bloom filter to prevent the sharing of duplicates within its production group. It is worth noting
that similar filters have been utilized in [
The results obtained using the -dup option are shown in Table 4. It can be observed that the outcomes are somewhat mitigated. Our intuition suggests that although a Bloom filter ofers eficiency, the process of verifying duplicate clauses in each round of sharing can still impede sharing. This trade-of does not appear to be worthwhile, especially in the context of this specific benchmark with the chosen solver.
Thus far, our research has focused on analyzing the impact of diferent mechanisms on a configuration consisting of 32 physical cores, which reflects the characteristics of machines used in SAT competitions over the past few years. However, the issue of scalability of these algorithms has emerged as a significant concern.
To address this concern, we conducted a new study using two additional architectures: one with 48 cores and another with 64 cores. Within this study, we concentrated on 32 cores
SAT instances 48 cores 64 cores UNSAT instances 32 cores 48 cores
64 cores 27500 25000 22500 20000 )s17500 ( iTem1125500000 10000 7500 5000 2500 0 2G-hordeStrategi2eGs-horde-str 1G-horde-dup 2G 2G-hordeStrategi2eGs-horde-str 1G-horde-dup the best-performing combinations identified in the 32-core study: namely, 2G, 2G-horde, 2G-horde-str, and 1G-horde-dup. To assess their performance, we employed a benchmark comprising 40 instances that were solved by at least one configuration utilizing the 32-core architecture, with each instance having a maximum allowed solving time. The results of this study are presented in Figure 4.
Overall, our findings indicate that the relative performance of the diferent combinations, with the exception of one case, remains consistent as the number of cores increases, regardless of whether the problem is SAT or UNSAT. However, we observed an intriguing phenomenon: beyond 48 cores, scalability notably diminishes for UNSAT problems, irrespective of the algorithm employed. This can be attributed to the limitations of the sharing mechanisms, as the additional threads do not efectively reduce the search space explored by other threads. Conversely, SAT problems exhibit diferent behavior, as increasing the number of threads enhances the probability of swiftly finding a solution.
Furthermore, alongside these general results that support prior research, it is worth highlighting the remarkable performance of 2G-horde-str. While it maintains its superiority for solving UNSAT problems, it emerges as the most eficient algorithm for SAT problems in the 64-core configuration. This achievement can be attributed to the substantial impact of strengthened clauses, which enable the early pruning of irrelevant branches in the decision tree, thereby accelerating convergence towards a solution.
In this paper, we have combined established techniques with new algorithms to enhance the sharing mechanism in the parallel solver, parkissat-rs.
Specifically, compared to the original implementation, we introduced production groups, the horde sharing strategy, strengthening, and duplicate removal mechanisms. The complete solver with all the options is depicted in Figure 2.
We conducted experiments and compared the performance of each implemented add-on on the benchmarks of the 2022 SAT competition. This allowed us to draw conclusions regarding the individual and combined efects of each technique. For SAT instances, the most efective implementation is P-2G. This implies that the original implementation is already eficient and requires minimal changes. The division of solvers within production groups significantly accelerates sharing.
For UNSAT instances, all implementations utilizing the horde sharing strategy are highly eficient. This mechanism complements strengthening and duplicate removal when used separately, but combining all three does not yield improved results.
These conclusions hold for multi-core machines with up to 100 cores. Further exploration of these strategies in many-core machines with more than 100 cores would be fascinating. In such scenarios, the cost of CPU-intensive mechanisms could be ofset by utilizing a larger number of solvers, achieving better resource utilization.
Furthermore, a possible heuristic avenue, not explored in this paper, is the diversification mechanism used by parallel SAT solvers to avoid redundant work between worker threads. We are interested in directly modifying the internal structure of the sequential engine by shufling the literal order of its clause database. This modification will impact the unit propagation of the solver and may yield diferent results. strengthening in parallel sat solving, in: R. Lee, S. Jha, A. Mavridou, D. Giannakopoulou (Eds.), NASA Formal Methods, Springer International Publishing, Cham, 2020, pp. 222–229. [8] B. H. Bloom, Space/time trade-ofs in hash coding with allowable errors, Communications of the ACM 13 (1970) 422–426. [9] D. Schreiber, P. Sanders, Scalable sat solving in the cloud, in: C.-M. Li, F. Manyà (Eds.), Theory and Applications of Satisfiability Testing – SAT 2021, Springer International Publishing, Cham, 2021, pp. 518–534.