Das Kapitel geht der entscheidenden Rolle von SAT-Formeln bei der Verschlüsselung komplexer Probleme in verschiedenen Bereichen wie Schaltkreisverifikation, Kryptographie, automatisierte Planung und Softwareverifikation nach. Es betont die Herausforderungen durch harte SAT-Instanzen und die Notwendigkeit paralleler und verteilter Rechnerumgebungen, um die Lösungszeiten zu reduzieren. Die Erweiterung des Rahmenwerks zur Aufnahme von SAT-Lösern für verteilte Klauseln ist ein wesentlicher Schwerpunkt, der die Einbeziehung diverser Klauselteilungsstrategien und Knotentopologien ermöglicht. Diese Erweiterung führt zu einem vielseitigen Framework, das die Entwicklung verteilter SAT-Solver vereinfacht und es zu einem unschätzbaren Werkzeug für Forscher macht. Das Kapitel bietet einen detaillierten Überblick über verwandte Arbeiten, einschließlich bahnbrechender Bemühungen zur Lösung verteilter SAT-Probleme und der Entwicklung von Strategien zum Austausch von Klauseln. Es präsentiert außerdem eine umfassende Bewertung der neuen Architektur, bewertet ihre Leistung anhand implementierter Sharing-Strategien und vergleicht sie mit modernen Lösungsansätzen. Das Kapitel schließt mit einer Diskussion über mögliche zukünftige Arbeiten, einschließlich der Entwicklung fehlertoleranter Algorithmen und der Optimierung bestehender Komponenten zur Steigerung der Gesamteffizienz. Die Erforschung der dezentralen Bereitstellung, der gemeinsamen Nutzung von Klauseln und der Architektur des Rahmenwerks bietet einen tiefen Einblick in die technischen Komplexitäten und innovativen Lösungen im Bereich der dezentralen SAT-Lösungen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
In the evolving landscape of SAT solving, leveraging parallel computation has become increasingly significant. The portfolio strategy, combined with clause sharing, has emerged as the leading approach for both local and distributed parallelization on CPUs. Frameworks such as Mallob exemplify the effectiveness of this strategy by providing a straightforward method to deploy portfolio parallel solvers across various computing environments. Similarly, the framework specializes in local parallelization, offering diverse strategies for task sharing and parallel execution. This enables the adoption of complex hybrid local parallelization techniques, including portfolio, divide-and-conquer, and cube-and-conquer methods.
This paper presents , a new extension of the framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden ’s functionality, enabling more effective and comprehensive distributed SAT solving methodologies.
1 Introduction
Currently, SAT formulas are essential for encoding complex problems across various fields such as circuit verification [25], cryptography [30], automated planning [35], and software verification [26]. The complexity of these encoded problems ranges from simple to extremely challenging. One effective method for solving hard instances is the use of parallelism.
According to the annual SAT competition [17], the Portfolio clause sharing parallelization strategy has been the gold standard for parallel SAT solving for several years. However, many SAT formulae remain too difficult to solver. As a result, exploiting distributed computing environments to reduce solving times has become a crucial research focus, inspiring the development of several software solutions and frameworks [5, 15, 23, 36]. To the best of our knowledge, existing competitive solutions lack the flexibility in distributed sharing and solving strategies that the
framework provides for (local) multi-core environments [28].
Anzeige
In this work, we extend the
framework to accommodate distributed clause sharing SAT solvers. This extension, namely
, allows the incorporation of various clause-sharing strategies and node topologies, resulting in a versatile framework that eases distributed SAT solvers development.
is designed as a simple, generic, and extensible platform for parallel and distributed SAT solvers. Its primary goal is to empower researchers to easily test and develop new sharing and parallelization strategies without needing to master the complexities of distributed programming for SAT solving. While it is not intended to outperform existing solvers,
serves as a research tool capable of replicating their performance, while providing a versatile environment for rapid prototyping and experimentation with innovative strategies.
This paper is organized as follows: Section 2 introduces preliminary concepts, followed by a review of related work in Section 3. Section 4 details the architecture of
and its new extension,
. In Section 5, we assess the new architecture with some implemented sharing strategies. Finally, we conclude with a discussion of potential future works in Section 6.
2 Sequential, Parallel and Distributed SAT solving
The Conflict-Driven Clause Learning (CDCL) [38] algorithm has emerged as the predominant method in SAT solving, consistently delivering superior performance across a wide spectrum of SAT challenges. This algorithm has benefited from various enhancements, encompassing sophisticated heuristics [33], advanced pre-processing and in-processing strategies [11], and efficient data structures [31].
Anzeige
Parallelizing CDCL poses significant challenges. State-of-the-art methods primarily involve running multiple instances of the algorithm concurrently. This is typically achieved by altering initial variable assignments [19, 24] or by diversifying the heuristics and configurations within a portfolio of sequential solvers [22]. The portfolio approach when combined with clause-sharing mechanisms [22], has proven to be the most effective for parallelizing CDCL solvers. Here, clauses learned by one solver are shared with others, reducing redundant mistakes and utilizing collective knowledge to speed up the solving process. According to the recent work [37], clause sharing is the primary factor in the success of distributed SAT solving, particularly when scaling to hundreds of solvers. While solver diversification remains beneficial, its impact becomes secondary compared to the collaborative learning achieved through clause sharing.
In distributed computing, we handle multiple computational units (or nodes) connected through a network. Implementing a distributed SAT solver based on the portfolio approach requires strategic diversification of CDCL solvers across nodes, ensuring effective clause sharing, both within nodes (intra-node) and between nodes (inter-node). It is crucial to mitigate communication latency and address the challenges posed by the asynchronous nature of efficient distributed systems, such as distinguishing between a node’s failure and its delayed response.
Challenges of Distributed SAT Solving: Scaling up a parallel SAT solver to distributed systems presents two main challenges:
Technical limitations that increase the difficulty of certain aspects of development, such as deployment, termination detection and fault management.
Adapting parallelization and clause sharing to efficiently utilize all available computing power.
Thus, developing distributed SAT solvers presents significant challenges that could be addressed through specialized tools abstracting away technical complexities. The key is creating a flexible, modular architecture that enables both simplicity and extensibility. This modularity allows users to easily locate and modify specific behaviors while containing feature logic within well-defined interfaces.
3 Related Works
SAT solving can be parallelized using the divide-and-conquer strategy [19]. One of the pioneering efforts in distributed SAT solving, PSATO [42] based on the sequential solver SATO [43], adopts this strategy with a master-slave model for communication and load-balancing. GridSAT [16] follows the same idea. In this solver, a node (referred to as a “client” in the original paper) alerts the master node to divide its search tree and assigns a portion to a new node when it encounters a problem that is too challenging or anticipates a memory overflow. This new node, initiated by the master, receives a subset of the problem directly from the initiating node, facilitating problem-solving in a distributed manner.
[23] advances this concept further by employing a Cube&Conquer [24] strategy for distributed SAT solving, along with an adaptable load-balancing mechanism. In Cube&Conquer, the problem is divided into thousands (or millions) of simpler sub-problems using look ahead [7, Chapter 5] techniques. Each sub-problem represents a portion of the original problem where some decisions have been pre-made, allowing CDCL solvers to focus on exploring specific parts of the search space efficiently.
At the same time, other solvers have explored the portfolio approach [22], a strategy also explored in other fields, such as in Software Verification [6]. For instance, the annual SAT competitions [17] highlight
[37] as a forefront solution in modern distributed SAT solving.
distinguishes itself through an adaptable scheduling mechanism. It can schedule different types of jobs, such as distributed portfolio instances of parallel SAT solvers. Thus, it is proficient in handling multiple SAT problems concurrently, adaptively redistributing resources based on the real-time difficulty assessment of each task.
employs a distributed clause sharing solver architecture, wherein each SAT problem (job) is tackled by a coordinated group of nodes specifically allocated for it. The clause sharing strategy is to gather the globally best clauses across all the solvers of a given job.
Introduced at the 2023 SAT Competition [4], the
framework [15] aims to simplify the construction of local parallel and distributed SAT solvers. It has demonstrated performance on par with the leading
system. The framework organizes computational nodes into distinct groups, each configured with a specific solver setup. For clause sharing, the version presented at the competition utilizes a circular ring architecture per group. Additionally, the framework can broadcast clauses from any given node to all others within its group using a tree-based structure.
The Parallel Instantiable SAT Solver, known as
[28], is a framework designed for the instantiation of parallel SAT solvers in multi-core environments. Over the years,
has successfully integrated a variety of sequential solvers, including
[10],
[9],
[8],
[29],
[2], and
[18]. It incorporates the two principal multi-threaded parallel strategies: Portfolio [22] and Divide and Conquer [19]. The adaptability and utility of
are attributed to its straightforward architecture (see Figure 1). This has enabled the implementation and execution of diverse parallel solving strategies, making
a significant tool in parallel SAT solving.
As depicted in Figure 1, the original architecture of
meticulously outlines the interactions among the various components within a parallel SAT solver, prioritizing simplicity, modularity, and flexibility. The behaviours related to parallelization are encapsulated by a tree of
implementations, with the
implementations at the leaves. These
instances interface with sequential solvers through the
. This interface provides all necessary interactions for the
to control the solving process, while the
facilitates clause sharing among its producers and consumers. The
represents the thread that executes the chosen
. For an in-depth explanation, please refer to [28].
Fig. 1.
The architecture of
The architecture of
showed its effectiveness in instantiating parallel SAT solvers via its results in the annual SAT Competitions [17]. The simplicity and extensibility it offers permitted the construction of multiple solvers such as those in works [39‐41]. However, the current architecture lacks sufficient abstractions and flexibility to permit efficient and straightforward instantiation of distributed solvers with diverse clause-sharing strategies.
In the
,
and
solvers, the logic for clause sharing is split between several entities in these solvers. For instance, filtering clauses based on size or LBD [1] value was done within the sequential solvers interaction interfaces’ export functions. To elevate this issue, we propose the new framework
that fixes the actual shortcomings of
and extend its functionalities to support distributed SAT solvers.
4 The Architecture of
is a new framework that enables the creation of distributed portfolios by instantiating and controlling sequential solvers across different nodes. This framework facilitates communication for clause exchange both via shared memory and message passing. In the following section, we will first discuss how the new software architecture mitigates the technical complexities of distributed systems. Then, we will explain how it simplifies the development of new sharing strategies.
4.1 Distributed Deployment In
In order to manage the multiple nodes and establish communication between them, we use the Message Passing Interface (
). It proved its effectiveness in state-of-the-art distributed SAT solvers such as
[37] and
[32]. A big part of the deployment of the distributed environment is managed by
, it mainly requires a hostfile identifying the different machines to be used. After the deployment, each node gets a unique identifier, the
.
In
, we updated the main function of
to manage the
initialization and finalization. This function is the one responsible for launching the corresponding
, waiting for its completion, and stopping it if the timeout is reached. In order to ensure flexibility, we also reduced the number of global variables, allowing the
implementations to manage the different instantiated components. Multiple working strategies can exist in parallel, each owning and managing its
working with its
. This design simplifies resource management and enhances efficiency.
Because nodes may not have local access to the SAT problem file, we implemented a formula-sharing mechanism within the mpiutils namespace. To handle large problem instances that can reach several gigabytes, we compress the numerical data using Zlib [21]. This mechanism is optional; the
implementation can choose to use or bypass these functions as needed.
Once the distributed solver finds a solution or a timeout is reached, all its nodes must be notified. And, in a distributed setting, termination is not that evident. Thus, to levitate this hurdle we have the new main function shown in Algorithm 1 and the termination detection algorithm described in Algorithm 2.
Algorithm 1 begins by parsing the arguments to define the desired solver to instantiate (line 2), followed by initializing essential variables for termination management (lines 3-6). The thread executing this main function sleeps with a timeout on the conditional variable condGlobalEnd (line 10) after launching a
. When a running thread finds the answer (SAT or UNSAT), it sets globalEnding and notifies the main via condGlobalEnd and updates the variables finalResult and finalModel. In case timeout is reached, the main wakes up and sets finalResult accordingly. The
finalization (line 15) occurs after the
concludes (line 14), ensuring no messages are left unprocessed. When main wakes up, it prints the model when required (lines 16-17) and exits by returning the finalResult’s value (SAT, UNSAT or TIMEOUT).
Algorithm 2 is a simple synchronization algorithm, that should be run periodically. The node with
\(=0\) acts as the master node and is notified by other nodes when they find a solution (line 7). This master node checks if it has found a solution (lines 10-11) and if a worker node sent a termination notification (line 13). Once the master knows whether a solution was found or not, it sends a message to all other nodes (line 15) indicating whether they should continue or stop. If the function returns true, the component executing this algorithm must wake up the node’s main function via (condGlobalEnd).
offers a rich and high-level API for the development of distributed applications. However, developing a portfolio distributed SAT solver remains complex, as it involves dealing with communication synchronization, data bufferization, and multiple threads. Our framework’s architecture hides this complexity by clearly separating the different needed behaviors in well-defined interfaces, guiding the developer in using network communication only where needed. The different aspects of the distributed solver can be changed independently. We present the interfaces of our framework in Section 4.2 with some implementation examples of sharing strategies in Section 5.1.
4.2 Clause Sharing in
Fig. 2.
The new architecture of Painless
Clause sharing in distributed SAT solvers can be managed in two main ways: using a single sharing strategy for both inter-node (global) and intra-node (local) sharing, or employing separate strategies for each scope. We want our framework to support both approaches, but the current architecture of
(Figure 1) does not accommodate the latter, limiting its flexibility. For example, to enable collaboration between global and local strategies, the global strategy must act as both a producer and a consumer within the local strategy, requiring it to implement the
interface from Figure 1. This highlights a deficiency in the current architecture’s ability to support more generic sharing strategies.
To address these limitations and support more flexible sharing mechanisms, we propose the new architecture depicted in Figure 2. This revised structure establishes a coherent hierarchy and interaction schema for both locally parallel and distributed SAT solvers, enabling more robust clause sharing mechanisms. A key advantage of this new architecture is its ability to mix inter-node and intra-node strategies without the need to implement entirely new strategies that handle both aspects. This modular approach allows for greater flexibility and efficiency, as developers can combine existing strategies in various ways without having to implement all possible combinations.
The proposed architecture introduces three new interfaces for sharing:
,
, and
. Additionally, we have updated the
worker and the
interface. Furthermore, the
has been made more abstract by adding specialized interfaces:
, and
.
Table 1.
Combined Abstract Interfaces for
and
. (+) Public method, (#) Protected method or member, (italics) Virtual method, (override) redefinition of virtual methods.
In the new architecture, clause importing and exporting functionalities have been transferred from
to the new
interface, which is inherited by both
and
. The primary methods of
, detailed in Table 1, offer flexibility for derived classes, easing the implementation of customized clause filtering and storage strategies.
The
maintains a dynamic list of clients (subscribers) to which it exports clauses. This list can be safely updated at any time using the
and
methods, ensuring thread-safe operations in concurrent environments. The export process is facilitated by two key methods:
for individual clauses and
for bulk exports. Both methods safely access the current client list, preventing race conditions during clause export.
These methods transmit clauses to each client using the
function, which primarily calls the client’s public
method. This adheres to a key design principle: the producer does not judge the usefulness of a clause; instead, this responsibility is left to the consumer. By invoking the client’s
method, we ensure that each client can implement its own sharing logic and clause filtering.
As illustrated in Figure 2, both
and
maintain dedicated
instances to store imported clauses. Each
implementation applies specific storage policies that may discard clauses based on memory constraints or other criteria, effectively adding a second filtering layer after
’s initial filter. The
additionally maintains a list of producers from which it obtains clauses. Two key methods manage producer interactions:
: Initializes the necessary data structures for a new producer.
: Adds the strategy as a client in the producer’s client list.
This two-step process ensures proper initialization order, mitigating potential concurrency issues.
In this revised architecture, the
invokes two essential methods defined by the
:
, which handles the periodic selection and export of clauses to the strategy’s clients, and
, which determines the wait time for the executor between two consecutive sharing operations. Additionally, the
can now manage multiple
instances, invoking their
methods in a round-robin fashion.
For inter-node sharing strategies, we introduced the specialized
interface, which adds distributed initialization and finalization through two additional methods:
and
. Its
method incorporates a termination-detection algorithm for the distributed solver, as detailed in Algorithm 2. While implementations can use this algorithm, they are free to develop custom approaches. Developers can also bypass the
interface entirely and directly implement the new
interface, enabling highly customized sharing strategies.
It is important to note that a sharing strategy may not always be necessary; in some cases, simply connecting different solvers via the client list is enough, eliminating the need for an additional thread to manage the sharing process.
These enhancements streamline the handling of challenging aspects in distributed environments, such as deployment and termination detection. The framework’s simplicity and extensibility facilitate rapid development of new distributed portfolio solvers, while its modular design enables researchers to conduct fair comparisons of different heuristics by maintaining consistency across other solver components.
5 Assessing The New Distributed
Framework
To demonstrate the scientific relevance of our framework, we present a study of various parallelization and sharing strategies inspired by state-of-the-art distributed SAT solvers, namely
[37] and
[32]. Additionally, we compare novel combinations of global and local sharing strategies that have not been previously explored.
5.1 Implementations of
We have developed three distributed sharing strategies for evaluating
:
,
and
. They all serialize the clauses to be shared along with their Literal Block Distance (LBD) values [1]1, enabling the receiving node’s consumer to assess the usefulness of the received clauses. However, the LBD value makes sense only locally to the solver that produced the clause, sharing it may help, but it has not that much importance [37, Section 5.1]. The size of the serializing buffer is configurable, which is crucial for controlling latency in inter-node communication.
implements a flexible approach to clause sharing among distributed SAT solver instances. It utilizes user-defined subscription and subscriber lists to establish communication patterns between nodes, allowing for customizable topologies including ring structures. The strategy employs non-blocking sends (MPI_Isend) to distribute clauses to subscribers and waits for incoming clauses by probing (MPI_Probe), using dynamic receive buffers to efficiently collect clauses from subscriptions. To optimize sharing, the implementation incorporates two Bloom filters [12]: one to prevent resending previously shared clauses, and another to avoid deserializing duplicate received clauses. We judged receiving duplicates of locally produced clauses from a subscription not harmful to the local solvers.
implements a straightforward strategy in which, during each round, every node broadcasts its clauses to all other nodes (as in [5]. The MPI_Allgather function serves as a synchronization point for all n participating nodes in the distributed system. To expedite the sharing process, we use a uniform static buffer size s across all nodes, padding with zeros if necessary, instead of pre-sending buffer sizes using MPI_Allgatherv. After collecting all buffers, we merge them into a single unified buffer, ensuring that each node ends the sharing round with an identical buffer of size \(n \times s\). A Bloom filter is employed to prevent redundant serialization and deserialization of clauses that have already been transmitted [5]. Upon deserialization, the clauses are immediately exported to the strategy’s clients.
Fig. 3.
The two phases of
strategy
strategy uses a binary tree topology for message passing, inspired by the sharing phase in
[37]. Each sharing round consists of two phases: clause merge and clause filtering. Communication is handled using MPI_Send, MPI_Probe, and MPI_Recv. The
method filters clauses based on their size and LBD values against predefined maxSize and maxLBD before storing them in the
.
In the first phase (see Figure 3a), nodes merge clause buffers received from their children with their own. Clauses are ordered by size, using LBD for tie-breaking, allowing an ordered merge to select the best clauses. The buffer size l(u) at each node is limited, except for clauses smaller than freeSize, which are not counted when serialized to the buffer [37]:
where \(\beta _{\infty }\) is the maximum buffer size, \(\beta _{0}\) is the minimum buffer size, and u is the number of merged buffers so far. Each node passes its value of u to its parent via the clause buffer.
The root node’s merged buffer contains the best clauses of the sharing round. This buffer is then broadcast to all nodes via the binary tree, with each node sending the buffer to its children.
In the second phase (see Figure 3b), each node generates a bit vector indicating which clauses were self-produced and shared in the previous z rounds. A custom distributed exact filter [37] detects duplicates, allowing clauses to be reshared after sufficient time. The bit vectors are combined via an OR operation up to the root and then broadcast to all nodes. Using the merged bit vector, nodes determine which clauses to export to their local clients.
Although the filter phase can lead to some wasted buffer space, a compensation mechanism dynamically adjusts the buffer size in future sharing rounds to mitigate this issue [37].
The first strategy developed was
, consisting of 192 lines of code (LoC) in its .cpp file. The
file contains 196 LoC, while
is larger at 728 LoC. Since initialization, serialization, and deserialization processes are consistent across all strategies, both
and
inherit approximately 80 LoC from
. The exact filter methods, adding another 83 LoC, are now integrated into the
class, as there is currently no separate filter interface.
5.2 Portfolio implementations of
To evaluate distributed portfolio solvers, we require implementations of:
to solve formulas,
to enforce the portfolio strategy, and
for clause management.
offers multiple
implementations, including
[9],
[10],
[34],
[13],
Class [8],
[29],
[18], and
[3]. For
, notable implementations include
, which respects a certain literal capacity and manages space for better clauses [37];
, designed to manage buffers for individual entities without requiring a lock mechanism; and
, which organizes clauses based on their size.
There is also an existing implementation of the intra-node sharing strategy
[5]. It filters produced clauses based on their LBD: it dynamically adjusts the solver’s LBD threshold to maintain optimal sharing if a solver shares too few or too many clauses.
We implement two portfolio strategies using the
interface:
and
. Both leverage the
variable to diversify solvers via unique globalIds. The
manages a general ID and type ID, enabling complete diversification.
offers a flexible, general-purpose implementation supporting both CDCL and local search solvers. It features local and global sharing mechanisms, a mallob mode replicating the sharing strategy from [37], and easy customization of solver types and strategies.
is a specialized portfolio based on
[32]. It executes pre-processing techniques such as Unit Propagation, Equivalent-literal Substitution, and Resolution Checking [14] in a leader node. Then, it divides all nodes into five groups: SAT, UNSAT, MAPLE, LGL, and DEFAULT. By following the implementation of [32], the group sizes are calculated based on the total number of nodes n, and are: \(\lfloor \frac{n}{8} \rfloor \), \(\lfloor \frac{n}{4} \rfloor \), \(\lfloor \frac{n}{8} \rfloor \), 1, \(n - 2\cdot \lfloor \frac{n}{8} \rfloor - \lfloor \frac{n}{4} \rfloor - 1\), respectively.
5.3 Evaluated Solvers
In Section 5.4 we evaluate different solvers, with different sharing strategies. The first two solvers emulate state-of-the-art solvers, while the two last explore new solvers implementing original sharing strategies.
: is an instantiation of
that emulates the setup of
[37]. The solvers set includes
(v3.1.1) and
(v1.9.1)2. For the sharing strategy, all solvers act as both producers and clients of the
strategy. It is configured in concordance to the one used by
in the 2024 International SAT Competition:
The freeSize parameter is set to 1 for unlimited unit clause sharing, the maximum clause size maxSize and LBD value maxLBD are both set to 60. Lastly, the clause database
is employed, as outlined in [37] with the maximum size set to maxSize and the capacity defined as \(10 * \beta _{0}\). \(\beta _{\infty }\) is set to 250000, while z is defined as 15 seconds, equivalent to 30 rounds. z represents the number of rounds during which a clause is remembered as being shared. If a clause is reshared after this period, it won’t be filtered as redundant. However, following
terminology, we used an option in seconds.
Fig. 4.
Ring topology of the DEFAULT group with 3 nodes in
: is an instantiation of
that emulates
[32]. The SAT and UNSAT groups use
(v1.0.3) solvers configured for their respective instance types. The MAPLE group uses
solvers, and the LGL group uses
(v1.0.0) solvers. Finally, the DEFAULT group uses
solvers with no specialization. For the sharing strategy,
requires sharing clauses from local solvers to the next neighbour, exporting received clauses from the previous neighbour to local solvers and to the next neighbour. Local solvers export clauses according to the hordeSat strategy [5]. To emulate this behaviour, we use a
instance having all solvers as clients and producers, and an instance of
configured for in-group ring sharing as a client (See Figure 4). To allow solvers receiving clauses from the previous neighbour, they subscribe to the
.
The
sends clauses obtained from the solvers via the
strategy to the next neighbour and exports received clauses from the previous neighbour to the solvers. To resend clauses received from the previous neighbour to the next neighbour, the
needs to import clauses that it exports to its clients; thus, it adds itself to its list of clients. Finally, following the implementation of
, the
strategy uses an unlimited buffer size and a single
instance executes both strategies.
: is an instantiation of
with
and
solvers, all connected to
. A
instance is used for inter-node sharing with the same parameters as
. It is solely connected to
, and both of them run on different threads.
: is an instantiation of
with
and
solvers, all connected to
. The
is used for inter-node sharing, solely connected to
. The
buffer size is set to \(1500\cdot \textit{solverCount}\) and each sharing strategy is executed by a separate
thread.
The initial LBD value in
is set to 2, with each producer having an upper limit of 1500 literals per sharing round.
uses
for concurrency management, while each solver uses
to store the imported clauses.
5.4 Evaluation
Table 2.
PAR2 and number of resolved instances on GRID5000. The winner and best values in each category are shown in bold font.
To assess the stability and performance of our new architecture, we used the 400 instances from the SAT’2024 competition, each with a timeout limit of 500 seconds. The tests were conducted on nodes in the “paravance” cluster of the Grid5000 infrastructure. Each node is equipped with two Intel Xeon E5-2630 v3 processors, featuring 8 physical cores each, and 128 GB of RAM, operating under a Non-Uniform Memory Access (NUMA) architecture with each CPU paired with 64 GB of RAM. All evaluations were done using 25 machines, thus having 50 CPUs, totaling 400 cores. All tested solvers use OpenMPI [20], and for each CPU an MPI process is instantiated.
To evaluate our emulations of
3 and
4, we ran the versions they submitted to the 2024 SAT Competition.
and
are configured as described earlier Section 5.3, please note that
was used in its mono mode, i.e. only one SAT problem is solved at a time. With 400 cores, the portfolios consist of multiple sequential solvers: 200
and 200
.
and
both follow a group distribution strategy (Section 5.2): 6 nodes with SAT-specialized
(48 cores), 12 nodes with UNSAT-specialized
(96 cores), 6 nodes with
(48 cores), 1 node with
(8 cores), and 25 nodes with general-purpose
(200 cores).
The version of
used to instantiate these solvers is available on GitHub5. The results of the evaluation are presented in Table 2, with the top row of the two first groups showing their relative Virtual Best Solver (VBS).
The solvers are compared using two metrics: the number of solved SAT problems and their PAR2 score. The PAR2 score penalizes unsolved instances by counting them as 2 times the timeout value. While traditionally PAR2 was calculated as a sum, in recent SAT competitions it is reported as an average on the number of benchmark instances. Additionally, to quantify how closely a solver’s S execution times \(S_{time}(i)\) approaches the ones of its relative VBS across the n tested instances, we use the Symmetric Mean Absolute Percentage Error (SMAPE) [27], defined as:
Table 2 tells us that the best overall solver is
, which solves the most instances. This is quite logical, since it uses three different state-of-the-art solvers:
,
, and
, each with different pre-processing and in-processing techniques, enabling it to solve different types of formulae. After it,
comes second. Even though it only uses
and
, it achieves excellent performance thanks to its clever clause sharing, showing the importance of efficient clause sharing in solving SAT problems.
comes very close to
, with a single instance difference in the overall score, but the UNSAT column shows us that it struggles to match the performance of
in UNSAT instances. The two solvers
and
perform worse than
, likely due to their more aggressive clause sharing. The
solver performs the worst; however, it was able to solve instances that were not solved by the best solver
, as shown by their relative VBS.
When comparing
with our emulation (
), the scatter plots in Figure 5b show that our emulation solves nearly the same UNSAT instances as
, with improved performance on SAT instances (Figure 5a). It is worth noting that even if
achieves better results than
, its resolution times are a little bit behind the best ones, as it is shown by the new metric
in Table 2. They are still close in performance, and thus we can say that we were able to emulate the
solver successfully with a more complex software architecture.
Fig. 6.
Execution times on UNSAT instances comparison with
When comparing
to our emulation (
), we observe that our solver is a bit less efficient on UNSAT instances (Figure 5d). However, as illustrated in Figure 5c, our solver resolves many SAT instances more efficiently. The
values in Table 2 confirms the current shortcomings, since the
solver is quite far from its relative VBS. These observations suggest that the current implementation may suffer from limited diversification or sub-optimal clause sharing.
In
and
, we implement more aggressive clause sharing, utilizing the
strategy for local sharing and the
or
strategy for global sharing. Although their PAR2 scores are higher than that of
, Figure 6b and Figure 6a show that these configurations are able to solve some UNSAT instances that
could not. The increased average solving time is likely a consequence of the aggressive clause sharing, which overloads the solvers with excessive clauses, thereby slowing down unit propagation. However,
with its more balanced global sharing via
allows to achieve better overall performance.
In summary, these experiments demonstrate that the solvers instantiated from the
framework can perform on par with state-of-the-art solvers. Our results show that
can successfully emulate existing solvers using different clause-sharing strategies with minimal performance loss. This highlights the framework’s ability to offer the flexibility, modularity, and generality for which it was designed. Ultimately,
simplifies the development of new distributed portfolio SAT solvers, making it easier to experiment with novel sharing strategies.
6 Conclusion
Taking advantage of massively parallel hardware is essential for addressing hard SAT problems. Current tools offer excellent performance and scalability on distributed systems for portfolio strategies but lack flexibility in their inter-node communication strategies. We propose a new extension for
, namely
, enabling clause sharing in a distributed system. This extension makes the framework capable of instantiating distributed portfolio solvers using various clause-sharing strategies.
An initial assessment shows that the new
architecture allows for the construction of distributed portfolios, offering performance close to that of state-of-the-art distributed SAT solvers. The modular and flexible nature of this new architecture simplifies experimenting with different sharing strategies.
The current architecture lacks a reliable mechanism to detect errors, making it vulnerable to node failures. Thus, to improve robustness, we aim to refine our strategies, introduce new ones like divide-and-conquer, and develop fault-tolerant algorithms that simplify the management of distributed workflows. In addition to this, we will work on optimizing the performance of the various existing components to further enhance the overall efficiency of the system.
Acknowledgements
The experiments presented in this paper were carried out using the Grid’5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and several Universities as well as other organizations (https://www.grid5000.fr).
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The integration of
wasn’t used due to a bug on our side when sharing clauses with other solvers (this has been fixed). However, it was used in
because
solvers shared clauses only among themselves.
framework specializes in local parallelization, offering diverse strategies for task sharing and parallel execution. This enables the adoption of complex hybrid local parallelization techniques, including portfolio, divide-and-conquer, and cube-and-conquer methods.
, a new extension of the 
framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden 
’s functionality, enabling more effective and comprehensive distributed SAT solving methodologies.
framework provides for (local) multi-core environments [28].
framework to accommodate distributed clause sharing SAT solvers. This extension, namely
, allows the incorporation of various clause-sharing strategies and node topologies, resulting in a versatile framework that eases distributed SAT solvers development.
is designed as a simple, generic, and extensible platform for parallel and distributed SAT solvers. Its primary goal is to empower researchers to easily test and develop new sharing and parallelization strategies without needing to master the complexities of distributed programming for SAT solving. While it is not intended to outperform existing solvers,
serves as a research tool capable of replicating their performance, while providing a versatile environment for rapid prototyping and experimentation with innovative strategies.
and its new extension,
. In Section 5, we assess the new architecture with some implemented sharing strategies. Finally, we conclude with a discussion of potential future works in Section 6.
[23] advances this concept further by employing a Cube&Conquer [24] strategy for distributed SAT solving, along with an adaptable load-balancing mechanism. In Cube&Conquer, the problem is divided into thousands (or millions) of simpler sub-problems using look ahead [7, Chapter 5] techniques. Each sub-problem represents a portion of the original problem where some decisions have been pre-made, allowing CDCL solvers to focus on exploring specific parts of the search space efficiently.
[37] as a forefront solution in modern distributed SAT solving.
distinguishes itself through an adaptable scheduling mechanism. It can schedule different types of jobs, such as distributed portfolio instances of parallel SAT solvers. Thus, it is proficient in handling multiple SAT problems concurrently, adaptively redistributing resources based on the real-time difficulty assessment of each task.
employs a distributed clause sharing solver architecture, wherein each SAT problem (job) is tackled by a coordinated group of nodes specifically allocated for it. The clause sharing strategy is to gather the globally best clauses across all the solvers of a given job.
framework [15] aims to simplify the construction of local parallel and distributed SAT solvers. It has demonstrated performance on par with the leading
system. The framework organizes computational nodes into distinct groups, each configured with a specific solver setup. For clause sharing, the version presented at the competition utilizes a circular ring architecture per group. Additionally, the framework can broadcast clauses from any given node to all others within its group using a tree-based structure.
[28], is a framework designed for the instantiation of parallel SAT solvers in multi-core environments. Over the years,
has successfully integrated a variety of sequential solvers, including
[10],
[9],
[8],
[29],
[2], and
[18]. It incorporates the two principal multi-threaded parallel strategies: Portfolio [22] and Divide and Conquer [19]. The adaptability and utility of
are attributed to its straightforward architecture (see Figure 1). This has enabled the implementation and execution of diverse parallel solving strategies, making
a significant tool in parallel SAT solving.
meticulously outlines the interactions among the various components within a parallel SAT solver, prioritizing simplicity, modularity, and flexibility. The behaviours related to parallelization are encapsulated by a tree of
implementations, with the
implementations at the leaves. These
instances interface with sequential solvers through the
. This interface provides all necessary interactions for the
to control the solving process, while the
facilitates clause sharing among its producers and consumers. The
represents the thread that executes the chosen
. For an in-depth explanation, please refer to [28].
showed its effectiveness in instantiating parallel SAT solvers via its results in the annual SAT Competitions [17]. The simplicity and extensibility it offers permitted the construction of multiple solvers such as those in works [39‐41]. However, the current architecture lacks sufficient abstractions and flexibility to permit efficient and straightforward instantiation of distributed solvers with diverse clause-sharing strategies.
,
and
solvers, the logic for clause sharing is split between several entities in these solvers. For instance, filtering clauses based on size or LBD [1] value was done within the sequential solvers interaction interfaces’ export functions. To elevate this issue, we propose the new framework
that fixes the actual shortcomings of
and extend its functionalities to support distributed SAT solvers.
is a new framework that enables the creation of distributed portfolios by instantiating and controlling sequential solvers across different nodes. This framework facilitates communication for clause exchange both via shared memory and message passing. In the following section, we will first discuss how the new software architecture mitigates the technical complexities of distributed systems. Then, we will explain how it simplifies the development of new sharing strategies.
). It proved its effectiveness in state-of-the-art distributed SAT solvers such as
[37] and
[32]. A big part of the deployment of the distributed environment is managed by
, it mainly requires a 
.
, we updated the main function of
to manage the
initialization and finalization. This function is the one responsible for launching the corresponding
, waiting for its completion, and stopping it if the timeout is reached. In order to ensure flexibility, we also reduced the number of global variables, allowing the
implementations to manage the different instantiated components. Multiple working strategies can exist in parallel, each owning and managing its
working with its
. This design simplifies resource management and enhances efficiency.
implementation can choose to use or bypass these functions as needed.
. When a running thread finds the answer (SAT or UNSAT), it sets globalEnding and notifies the main via condGlobalEnd and updates the variables finalResult and finalModel. In case timeout is reached, the main wakes up and sets finalResult accordingly. The
finalization (line 15) occurs after the
concludes (line 14), ensuring no messages are left unprocessed. When main wakes up, it prints the model when required (lines 16-17) and exits by returning the finalResult’s value (SAT, UNSAT or TIMEOUT).
\(=0\) acts as the master node and is notified by other nodes when they find a solution (line 7). This master node checks if it has found a solution (lines 10-11) and if a worker node sent a termination notification (line 13). Once the master knows whether a solution was found or not, it sends a message to all other nodes (line 15) indicating whether they should continue or stop. If the function returns 
offers a rich and high-level API for the development of distributed applications. However, developing a portfolio distributed SAT solver remains complex, as it involves dealing with communication synchronization, data bufferization, and multiple threads. Our framework’s architecture hides this complexity by clearly separating the different needed behaviors in well-defined interfaces, guiding the developer in using network communication only where needed. The different aspects of the distributed solver can be changed independently. We present the interfaces of our framework in Section 4.2 with some implementation examples of sharing strategies in Section 5.1.
(Figure 1) does not accommodate the latter, limiting its flexibility. For example, to enable collaboration between global and local strategies, the global strategy must act as both a producer and a consumer within the local strategy, requiring it to implement the
interface from Figure 1. This highlights a deficiency in the current architecture’s ability to support more generic sharing strategies.
,
, and
. Additionally, we have updated the
worker and the
interface. Furthermore, the
has been made more abstract by adding specialized interfaces:
, and
.
and
. (+) Public method, (#) Protected method or member, (italics) Virtual method, (override) redefinition of virtual methods.
to the new
interface, which is inherited by both
and
. The primary methods of
, detailed in Table 1, offer flexibility for derived classes, easing the implementation of customized clause filtering and storage strategies.
maintains a dynamic list of clients (subscribers) to which it exports clauses. This list can be safely updated at any time using the
and
methods, ensuring thread-safe operations in concurrent environments. The export process is facilitated by two key methods:
for individual clauses and
for bulk exports. Both methods safely access the current client list, preventing race conditions during clause export.
function, which primarily calls the client’s public
method. This adheres to a key design principle: the producer does not judge the usefulness of a clause; instead, this responsibility is left to the consumer. By invoking the client’s
method, we ensure that each client can implement its own sharing logic and clause filtering.
and
maintain dedicated
instances to store imported clauses. Each
implementation applies specific storage policies that may discard clauses based on memory constraints or other criteria, effectively adding a second filtering layer after
’s initial filter. The
additionally maintains a list of producers from which it obtains clauses. Two key methods manage producer interactions:
: Initializes the necessary data structures for a new producer.
: Adds the strategy as a client in the producer’s client list.
invokes two essential methods defined by the
:
, which handles the periodic selection and export of clauses to the strategy’s clients, and
, which determines the wait time for the executor between two consecutive sharing operations. Additionally, the
can now manage multiple
instances, invoking their
methods in a round-robin fashion.
interface, which adds distributed initialization and finalization through two additional methods:
and
. Its
method incorporates a termination-detection algorithm for the distributed solver, as detailed in Algorithm 2. While implementations can use this algorithm, they are free to develop custom approaches. Developers can also bypass the
interface entirely and directly implement the new
interface, enabling highly customized sharing strategies.
Framework
[37] and
[32]. Additionally, we compare novel combinations of global and local sharing strategies that have not been previously explored.
:
,
and
. They all serialize the clauses to be shared along with their Literal Block Distance (LBD) values [1]1, enabling the receiving node’s consumer to assess the usefulness of the received clauses. However, the LBD value makes sense only locally to the solver that produced the clause, sharing it may help, but it has not that much importance [37, Section 5.1]. The size of the serializing buffer is configurable, which is crucial for controlling latency in inter-node communication.
implements a flexible approach to clause sharing among distributed SAT solver instances. It utilizes user-defined subscription and subscriber lists to establish communication patterns between nodes, allowing for customizable topologies including ring structures. The strategy employs non-blocking sends (
implements a straightforward strategy in which, during each round, every node broadcasts its clauses to all other nodes (as in [5]. The 
strategy
strategy uses a binary tree topology for message passing, inspired by the sharing phase in
[37]. Each sharing round consists of two phases: clause merge and clause filtering. Communication is handled using 
method filters clauses based on their size and LBD values against predefined maxSize and maxLBD before storing them in the
.
, consisting of 192 lines of code (LoC) in its 
file contains 196 LoC, while
is larger at 728 LoC. Since initialization, serialization, and deserialization processes are consistent across all strategies, both
and
inherit approximately 80 LoC from
. The exact filter methods, adding another 83 LoC, are now integrated into the
class, as there is currently no separate filter interface.
to solve formulas,
to enforce the portfolio strategy, and
for clause management.
offers multiple
implementations, including
[9],
[10],
[34],
[13],
Class [8],
[29],
[18], and
[3]. For
, notable implementations include
, which respects a certain literal capacity and manages space for better clauses [37];
, designed to manage buffers for individual entities without requiring a lock mechanism; and
, which organizes clauses based on their size.
[5]. It filters produced clauses based on their LBD: it dynamically adjusts the solver’s LBD threshold to maintain optimal sharing if a solver shares too few or too many clauses.
interface:
and
. Both leverage the
variable to diversify solvers via unique 
manages a general ID and type ID, enabling complete diversification.
offers a flexible, general-purpose implementation supporting both CDCL and local search solvers. It features local and global sharing mechanisms, a 
is a specialized portfolio based on
[32]. It executes pre-processing techniques such as Unit Propagation, Equivalent-literal Substitution, and Resolution Checking [14] in a leader node. Then, it divides all nodes into five groups: SAT, UNSAT, MAPLE, LGL, and DEFAULT. By following the implementation of [32], the group sizes are calculated based on the total number of nodes n, and are: \(\lfloor \frac{n}{8} \rfloor \), \(\lfloor \frac{n}{4} \rfloor \), \(\lfloor \frac{n}{8} \rfloor \), 1, \(n - 2\cdot \lfloor \frac{n}{8} \rfloor - \lfloor \frac{n}{4} \rfloor - 1\), respectively.
: is an instantiation of
that emulates the setup of
[37]. The solvers set includes
(v3.1.1) and
(v1.9.1)2. For the sharing strategy, all solvers act as both producers and clients of the
strategy. It is configured in concordance to the one used by
in the 2024 International SAT Competition:
is employed, as outlined in [37] with the maximum size set to maxSize and the capacity defined as \(10 * \beta _{0}\). \(\beta _{\infty }\) is set to 250000, while z is defined as 15 seconds, equivalent to 30 rounds. z represents the number of rounds during which a clause is remembered as being shared. If a clause is reshared after this period, it won’t be filtered as redundant. However, following
terminology, we used an option in seconds.
: is an instantiation of
that emulates
[32]. The SAT and UNSAT groups use
(v1.0.3) solvers configured for their respective instance types. The MAPLE group uses
solvers, and the LGL group uses
(v1.0.0) solvers. Finally, the DEFAULT group uses
solvers with no specialization. For the sharing strategy,
requires sharing clauses from local solvers to the next neighbour, exporting received clauses from the previous neighbour to local solvers and to the next neighbour. Local solvers export clauses according to the hordeSat strategy [5]. To emulate this behaviour, we use a
instance having all solvers as clients and producers, and an instance of
configured for in-group ring sharing as a client (See Figure 4). To allow solvers receiving clauses from the previous neighbour, they subscribe to the
.
sends clauses obtained from the solvers via the
strategy to the next neighbour and exports received clauses from the previous neighbour to the solvers. To resend clauses received from the previous neighbour to the next neighbour, the
needs to import clauses that it exports to its clients; thus, it adds itself to its list of clients. Finally, following the implementation of
, the
strategy uses an unlimited buffer size and a single
instance executes both strategies.
: is an instantiation of
with
and
solvers, all connected to
. A
instance is used for inter-node sharing with the same parameters as
. It is solely connected to
, and both of them run on different threads.
: is an instantiation of
with
and
solvers, all connected to
. The
is used for inter-node sharing, solely connected to
. The
buffer size is set to \(1500\cdot \textit{solverCount}\) and each sharing strategy is executed by a separate
thread.
is set to 2, with each producer having an upper limit of 1500 literals per sharing round.
uses
for concurrency management, while each solver uses
to store the imported clauses.
3 and
4, we ran the versions they submitted to the 2024 SAT Competition.
and
are configured as described earlier Section 5.3, please note that
was used in its mono mode, i.e. only one SAT problem is solved at a time. With 400 cores, the portfolios consist of multiple sequential solvers: 200
and 200
.
and
both follow a group distribution strategy (Section 5.2): 6 nodes with SAT-specialized
(48 cores), 12 nodes with UNSAT-specialized
(96 cores), 6 nodes with
(48 cores), 1 node with
(8 cores), and 25 nodes with general-purpose
(200 cores).
used to instantiate these solvers is available on GitHub5. The results of the evaluation are presented in Table 2, with the top row of the two first groups showing their relative Virtual Best Solver (VBS).
, which solves the most instances. This is quite logical, since it uses three different state-of-the-art solvers:
,
, and
, each with different pre-processing and in-processing techniques, enabling it to solve different types of formulae. After it,
comes second. Even though it only uses
and
, it achieves excellent performance thanks to its clever clause sharing, showing the importance of efficient clause sharing in solving SAT problems.
comes very close to
, with a single instance difference in the overall score, but the UNSAT column shows us that it struggles to match the performance of
in UNSAT instances. The two solvers
and
perform worse than
, likely due to their more aggressive clause sharing. The
solver performs the worst; however, it was able to solve instances that were not solved by the best solver
, as shown by their relative VBS.
with our emulation (
), the scatter plots in Figure 5b show that our emulation solves nearly the same UNSAT instances as
, with improved performance on SAT instances (Figure 5a). It is worth noting that even if
achieves better results than
, its resolution times are a little bit behind the best ones, as it is shown by the new metric
in Table 2. They are still close in performance, and thus we can say that we were able to emulate the
solver successfully with a more complex software architecture.
to our emulation (
), we observe that our solver is a bit less efficient on UNSAT instances (Figure 5d). However, as illustrated in Figure 5c, our solver resolves many SAT instances more efficiently. The
values in Table 2 confirms the current shortcomings, since the
solver is quite far from its relative VBS. These observations suggest that the current implementation may suffer from limited diversification or sub-optimal clause sharing.
and
, we implement more aggressive clause sharing, utilizing the
strategy for local sharing and the
or
strategy for global sharing. Although their PAR2 scores are higher than that of
, Figure 6b and Figure 6a show that these configurations are able to solve some UNSAT instances that
could not. The increased average solving time is likely a consequence of the aggressive clause sharing, which overloads the solvers with excessive clauses, thereby slowing down unit propagation. However,
with its more balanced global sharing via
allows to achieve better overall performance.
framework can perform on par with state-of-the-art solvers. Our results show that
can successfully emulate existing solvers using different clause-sharing strategies with minimal performance loss. This highlights the framework’s ability to offer the flexibility, modularity, and generality for which it was designed. Ultimately,
simplifies the development of new distributed portfolio SAT solvers, making it easier to experiment with novel sharing strategies.
, namely
, enabling clause sharing in a distributed system. This extension makes the framework capable of instantiating distributed portfolio solvers using various clause-sharing strategies.
architecture allows for the construction of distributed portfolios, offering performance close to that of state-of-the-art distributed SAT solvers. The modular and flexible nature of this new architecture simplifies experimenting with different sharing strategies.
wasn’t used due to a bug on our side when sharing clauses with other solvers (this has been fixed). However, it was used in
because
solvers shared clauses only among themselves.
