Keywords

1 Introduction

Modern CDCL SAT solvers  [1, 12] have been successfully used to solve a wide variety of real-world problems, such as those issued from hardware and software verification  [4].

With the omnipresence of many-core machines, these solvers have been adapted to become parallel  [3]. In this context, a key feature in the efficiency is information sharing. This is usually implemented as sets of new (learnt) lemmas that are exchanged between the different participants of the parallelization solving strategy (i.e., the underling sequential solvers).

Besides, it is well admitted that the shorter the learnt lemmas the more powerful they are. This explained the proposal of different techniques based on resolution to shorten them  [7, 8, 15, 16]. A process known as strengthening. Potentially as difficult as the SAT problem itself, the strengthening of those learnt lemmas can benefit from parallelization  [17].

This paper presents the implementation and evaluation of a parallel strengthening algorithm inspired from [17]. Our implementation is integrated as a part of Painless  [9], a framework for building parallel SAT solvers.

Paper Structure. Section 2 introduces some background. Strengthening is presented in Sect. 3. Its implementation is described in Sect. 4. Some experimental results are depicted in Sect. 5. Section 6 concludes the paper.

2 Background

This section introduces useful background used in the remaining of this paper.

Boolean Satisfiability. A propositional variable is a variable that has two possible values: true or false. A literal is a propositional variable or its negation (NOT). A clause is a finite disjunction (OR) of literals. A clause with a unique literal is called unit clause. A conjunctive normal form (CNF) formula is a finite conjunction (AND) of clauses. In the rest of the paper clauses are represented by the set of their literals, and formulas by the set of their clauses. Let F be a formula, an assignment of variables of F is defined as a function \(\mathcal {A}: \mathcal {V}\rightarrow \{true, false\}\), where \(\mathcal {V}\) is the set of variables of F. A clause is satisfied when at least one of its literals is evaluated to true. A formula is satisfied if all its clauses are evaluated to true. A formula is said to be satif there is at least one assignment of its variables that makes it true; it is reported to be unsatotherwise. The Boolean satisfiability (SAT) problem consists in determining if a given formula is sator unsat.

CDCL Algorithm. Conflict-driven clause learning algorithm  [14, 18] is used in almost all (complete) modern SAT solvers. It enumerates assignments for the given formula. Variables’ values are forced using unit propagation  [5] (i.e.,fixing recursively the values of variables in unit clauses). If an empty clause is generated a conflict has been reached. The reasons are studied and a learnt clause is derived and stored. The search backtracks and starts over. If unit propagation does not generate a conflict, a guess is done (branching) to grow up the current assignment. The search ends if a satisfying assignment has been found or if all have been checked without finding solutions.

Let F be a formula, unit propagation can be iteratively applied for a given partial assignment \(\mathcal {A}\): iterativeUnitPropagation\((F,\mathcal {A})\) produces the set of assignments implied by this operation. \(F|_A\) returns the formula simplified by the iterative unit propagations of \(\mathcal {A}\) on F.

figure a

3 Strengthening Algorithm

The pseudo-code of the strengthening algorithm we implemented in our tool is presented in Algorithm 1. The theoretical basics of this technique are presented in [17]. This section only focuses on the technical details.

Algorithm 1 takes a clause \(C_{in}\) as input, and, potentially outputs a reduced size (strengthened) clause, w.r.t. \(C_{in}\), (lines 8 and 14). It considers an empty assignment \(\mathcal {A}\) (line 3), the knowledge of all the clauses of the problem F, and it manages its own set of learnt clauses \(L_R\) (line 4) empty at the beginning of the program.

To achieve its strengthening task, Algorithm 1 iteratively assigns a false value to each literal of the clause \(C_{in}\), until it reaches a conflict or it assigns successfully all literals of the input clause. Therefore, there are two possible outputs, respectively \(C_{new}\) and \(C_{out}\).

At each iteration, Algorithm 1 picks a literal whose complementary is not implied by the current assignment (\(\lnot l \notin \texttt {iterativeUnitPropagation}(F^{\prime },\mathcal {A})\)). This ensures the stripping of the input clause from all literals that are implied by the rest of the clause. Then, it executes a unit propagation (line 5). If no conflict is discovered, the literal is added to the output clause \(C_{out}\) and its negation is added to the set of assignment \(\mathcal {A}\) (line 10–11).

When a conflict is reached (line 6), function \(\texttt {analyze}()\) is then called (line 7): it executes a sequence of backtracking, unit propagation, and conflict analysis until getting out of the conflict or emptying the set \(\mathcal {A}\). During this phase, the algorithm learns new clauses (that are added to \(L_R\)). When \(\texttt {analyze}()\) reaches a zone without conflict (while assuming \(\mathcal {A}\)), it generates the clause \(C_{new}\) that is returned (line 8). This last is composed of the set of literals: \(\{l | \lnot {l} \in \mathcal {A}\} \cup \{k\}\), k being some literal of \(C_{out} \notin \mathcal {A}\).

If all the literal of \(C_{in}\) are assigned successfully, then the clause \(C_{out}\) is added to \(L_R\) and then returned (lines 13–14).

4 Implementation

Our implementation is based on Painless  [9] which is a framework allowing the implementation of parallel SAT solvers for many-core environments. The main components of Painless are: working organization, clause sharing, and sequential engines. For this work, we focused on the third component and implemented a reducer solver that can be included in all Painless’ configurations.Footnote 1

About the Painless Framework. The main idea of the framework is to separate the technical components (e.g.,dedicated to concurrent programming aspects) from those implementing heuristics and optimizations embedded in a parallel SAT solver. Three main components arise when treating parallel SAT solvers: Sequential Engines, Parallelisation, and Sharing. These form the global architecture of Painless. They can be instantiated independently to produce new complete solvers.

The core element considered here is a sequential SAT solver. This can be any CDCL-like solver. Technically, these engines are operated through a generic SolverInterface providing basics of sequential solvers: solve, add clauses, etc.

To build a parallel solver using the aforementioned engines, one needs a parallelisation strategy (e.g.,s portfolio, divide-and-conquer). In Painless, a strategy is represented by a tree-structure of arbitrary depth. The internal nodes of the tree (WorkingStrategy) represent parallelisation strategies, and leaves are core engines operated by a thread (SequentialWorker).

In Painless, solvers can export (import) clauses to (from) the others during the resolution process. The sharing of these learnt clauses is dedicated to particular components called Sharers. Each Sharer is in charge of sets of producers and consumers and its behaviour reduces to a loop of sleeping and exchange phases w.r.t.to a given SharingStrategy.

Implementing Strengthening. This section presents the implementation of strengthening we included into the Painless framework. The development of such a component has been designed to be easily used in combination with all other mechanisms provided by Painless.

The Reducer engine of Fig. 1 implements Algorithm 1. As it can be easily observed, the main component of this algorithm are iterative unit propagation and analysis (based on assumptions) procedures. These are also the usual components provided by any CDCL-like SAT solver.

Therefore, we implemented the strengthening operation as a decorator of SolverInterface. This decorator is a SolverInterface itself that uses, by delegation, another SolverInterface to apply the strengthening (see Fig. 1).

Fig. 1.
figure 1

Parallel strengthening architecture

Full size image

The CDCL solver needs to be able to solve a formula with a set of assumptions. Assumptions are literals with a predefined value that the solver must accept as immutable. This is how we implemented the loop in Algorithm 1. We give the negation of the learnt clause as assumptions to the solver, which stops the resolution when a conflict is reached or when the solver has branched on all the assumptions. The solver must also be able to express a conflict only in terms of assumptions, i.e. the set of literals returned by the analysis contains only literals present in the initial set of assumptions.

The Reducer is always at the root of a portfolio. For example, if one wants to implement a divide-and-conquer solver complemented by a Reducer, they must create a portfolio with a Reducer and a divide-and-conquer as workers. This is extremely easy to do thanks to the composite nature of Painless’ Parallelisation engine. The Reducer is both a consumer and a producer of the Sharer. It receives clauses, strengthened them and shares them back after.

5 Empirical Study

To assess the performances of the developed component and study its impact in different parallel solvers, we integrated our Reducer in several parallelisation strategies. We then conducted a set of experiments to compare the results.

Solvers Description. All parallel solvers we constructed, but one, are based on P-MCOMSPS  [11]. It implements a portfolio strategy   [6] (PF) and uses MapleCOMSPS  [13] as sequential engine. The solvers differ however by their sharing strategies.

One of the main heuristics used in sharing strategies is the so-called Literal Block Distance (LBD) measure: the LBD of a clause is the number of decision levels represented in that clause. It is fairly admitted that the lower the LBD, the better the clause [1]. In a parallel context, it is useful to share these low LBD clauses.

We therefore derived the following strategies: AI, only learnt clauses with an LBD value less or equal than a threshold are shared. This threshold is additively increased if not enough clauses are exchanged  [2]; \(\mathbf{L} {i}\) shares only learnt clauses with an LBD value \(\le i\). Hence, we ended up by developing the solver P-MCOMSPS-AIFootnote 2, the solver P-MCOMSPS-L2Footnote 3 and the solver P-MCOMSPS-L4 (L4 is a new untested yet strategy).

To complete the picture, we also developed a divide-and-conquer (DC) solver that uses L4 sharing strategy. We call this solver DC-MCOMSPS-L4  [10].

For each of these solvers, we created its counterpart including the Reducer component. We called them by extending their names by -REDUCE (e.g., P-MCOMSPS-L4-REDUCE). It is important to note that the we do not use a additional core for the Reducer, e.g., if we use 12 cores for P-MCOMSPS-L4, we also use 12 cores for P-MCOMSPS-L4-REDUCE, one thread performs the strengthening instead of the CDCL algorithm.

Table 1. Results of the different solvers on the SAT benchmark 2018
Full size table

Experimental Results. For the evaluation we use the main benchmark of the SAT competition 2018Footnote 4 which contains 400 instances. All jobs were run on an Intel Xeon CPUs @ 2.40 GHz and 1.48 TB of RAM. Solvers have been launched with 12 threads, a 150 GB memory limit, and a 5000 s timeout (the timeout is the same as for the SAT competitions).

The performance of our solvers is evaluated using the following success metrics: penalized average runtime (PAR-2) sums the execution time of a solver and penalizes the executions that exceed the timeout with a factor 2; solution-count ranking (SCR) counts the number of problems solved by a solver; cumulative time of the intersection (CTI) sums the execution time of a solver on the problems solved by all the solvers.

Table 1 presents the results of our experiments, where each solver is compared to its counterpart (with a Reducer component). The shaded cells indicate which one of the two solvers has the best results. We observe that in all metrics, but two cases, the versions with a Reducer are better: more instances are solved and better PAR-2 values are obtained in all cases. Only CTI of the DC version is not as good as the other values. Also, the gains in the number of instances solved appears to be greater in the unsatcategory, but the number of satinstances also improves.

To go further in our evaluation, we measured the minimisation capabilities of the Reducer on instances that each solver could actually solve, while discarding those where the Reducer did not receive any clause (problem solved too quickly): (1) P-MCOMSPS-L4-REDUCE (255 instances), 44.21% of the clauses treated by the Reducer are actually shortened. The mean size of these clauses after strengthening is 25.45% less than the mean of their original size; (2) P-MCOMSPS-L2-REDUCE (257 instances), treated 32.59% of the clauses and it lower their size by 23.67%; (3) P-MCOMSPS-AI-REDUCE (258 instances) treated 34.79% clauses and reduced by 27.75%; (4) DC-MCOMSPS-L4-REDUCE (245 instances) reduced 28.80% clauses by 18.86%. In conclusion, the Reducer succeeded to reduce 1/3 of the clauses it receives by 1/4 of their size.

6 Conclusion

This paper presents an implementation of clause strengthening  [17] which has been integrated into Painless  [9]. Thanks to the modularity of Painless, we were able to test the efficiency of strengthening within different configurations of parallel SAT solvers.

In this study, we used several sharing strategies and different parallelisation paradigms (i.e.,portfolio and divide-and-conquer). Our experiments show that having a core dedicated to strengthening improves the performance of our parallel solvers whatever the configuration is (including the winner configuration from the SAT competition 2018).