The Con ict-Driven Clause Learning algorithms for solving the Boolean satis ability problem comprise the major part of the methods used to solve various instances of the problems that arise in industry and science. In recent years there have been proposed several major heuristics for these algorithms which are assumed to be de facto good for the solvers' performance over diverse sets of benchmarks. The goal of this paper is to evaluate the contribution of each separate heuristic to the performance of a state-of-the-art solver, see the extent to which they are bene cial, and gure out if the heuristics have any particular features that need to be taken into account.
The Boolean satis ability problem (SAT) [
Since SAT is NP-complete, modern implementations of CDCL employ a lot of heuristics. Some of them can be considered baseline, such as the Variable State Independent Decaying Sum (VSIDS) [3], restarts [4], or Literal Block Distance [5]. Others are either situational or were proposed only recently. The latter include Learnt Clause Minimization [6], Distance heuristic [7], Chronological Backtracking [8], Duplicate Learnts heuristic [9], and the use of Stochastic Local Search component [10]. The interesting observation is that the majority of applications, such as cryptography or bioinformatics, tend to use the older solvers developed prior to 2013, such as MiniSAT [11] or glucose [5]. The new CDCL heuristics proposed in recent years have yet to earn such acclaim.
In the present paper, the goal is to evaluate the contribution of the state-of-the-art CDCL heuristics proposed recently to the solvers' e ectiveness and compare them with each other. The main studied question is whether the new heuristics do improve the solvers' e ectiveness over a wide range of benchmarks or not. An additional goal is to understand the strengths and weaknesses of these heuristics.
A brief outline of the paper is as follows. The next section presents some background on CDCL SAT solvers and the considered heuristics. The third section contains the methodology of experiments, including the description of several variants of the Relaxed LCMDCBDL newTech SAT solver that took 2nd place in the SAT Competition 2020. These variants di er only in the enabled heuristics. They are compared in the fourth section which is devoted to the computational experiments and their discussion. It is followed by the conclusion and acknowledgments.
As was mentioned above, the modern CDCL SAT solvers are programmatic implementations of the algorithms for solving the Boolean satis ability problem. Essentially, they are the tools to be used in practice for tackling hard problems, that can not be easily be solved using existing e ective approaches. The progress in CDCL SAT solvers is mainly realized via annual SAT Competitions1. These competitions use benchmark sets comprised of instances from diverse application domains to test new heuristics and implementations of the CDCL algorithm. They are popular with the developers of SAT solvers and related technologies. The emergence of the MiniSAT solver in 2004 [11] marked an important stepping stone in the CDCL solvers development thanks to the high quality of its programmatic implementation. To this day, the majority of modern algorithms for solving SAT are either directly based on MiniSAT or employ many of the implementation techniques it popularized. It would not be far o to say, that MiniSAT can be viewed as one of the main progenitors of almost all modern SAT solvers. On the heuristics side, MiniSAT implemented VSIDS and the frequent restarts. Later, the state of the art in CDCL was extended by the concept of Literal Block Distance (LBD) [5]. However, since then the progress in the area somewhat stagnated. Despite many new heuristics being introduced, many SAT applications still employ MiniSAT and glucose solvers proposed more than ten years ago.
Nevertheless, the SAT competitions continue, and naturally, the heuristics which appear in the winners of competitions are viewed with great interest. In the context of this paper, several promising heuristics proposed in recent years will be considered. The brief outline and description of the analyzed heuristics follow.
LCM: Learnt Clause Minimization { the heuristic proposed in [6], which is aimed at improving the quality of learnt clauses by applying to them a special procedure that makes it possible to remove the redundant literals from a clause.
DISTANCE: the distance heuristic was rst introduced in [7]. Its goal is to initialize the values of the branching heuristic by directing the search at the beginning. It is relatively expensive, so in most implementations the heuristic works for at most 100 000 con icts. CB: Chronological Backtracking { this method described in [8] implements an attempt to make a partial return to the roots of SAT solving, in particular, to the Davis{Putnam{Logemann{Loveland (DPLL) algorithm. It allows the solver in certain conditions to ignore the nonchronological backtracking, which became one of the trademarks of CDCL solvers, in favor of a chronological one.
DL: Duplicate learnts heuristic [9] attempts to use simple data mining methods to discover the learnt clauses that are repeatedly derived during the search and store them permanently. SLS: the Stochastic Local Search component augmented with Rephasing technique has been appearing in the growing number of solvers. While the idea of combining CDCL and SLS is far from novel, the implementation of the SLS component in Relaxed LCMDCBDL newTech [10] has several speci c features that have not been used before.
The implementation of each heuristic usually contributes major changes to some of the core SAT solver components. Nevertheless, it is often possible to isolate the heuristic from the 1 http://www.satcompetition.org/ rest of the algorithm. Since the goal of the present paper is to evaluate the heuristics and compare their e ectiveness, it was decided to perform the computational experiments using the SAT solver which already implements all of the listed ones. In particular, there was used the Relaxed LCMDCBDL newTech solver that took the second place at SAT Competition 2020. Below it is referred to as RLNT. What makes it interesting compared to SAT Competition 2020 winner, the kissat solver, is that the lineage of RLNT can be easily followed back to Minisat [11]. Indeed, RLNT is based on MapleLCMDistChronoBT-DL-v3 { the winner of SAT Race 2019, which is based on MapleLCMDistChronoBT { the winner of SAT Competition 2018, based on MapleLCMDist { the winner of SAT Competition 2017, based on MapleCOMSPS { the winner of SAT Competition 2016, based on CominisatPS [12], based on Minisat and glucose. Informally, it can be said that MapleLCMDist = MapleCOMSPS + LCM + DIST, MapleLCMDistChronoBT = MapleLCMDist + CB, MapleLCMDistChronoBT-DL-v3=MapleLCMDistChronoBT+ DL. Finally, RLNT = MapleLCMDistChronoBT-DL-v3 + SLS. The reality is more complex in the latter two cases, since the di erence between the corresponding solvers involves changes to some of the parameters of existing heuristics.
To evaluate the contribution of heuristics in equal conditions, there was developed the implementation of RLNT, in which each of the heuristics listed in the previous section can be enabled or disabled independently via the use of #ifdef mechanism. It means that by manipulating the de ned constants it is possible to change only the header of a single source le, recompile the program and obtain, e.g. RLNT-noCB solver, which has the Chronological Backtracking disabled. The general idea that is employed to compare the heuristics is to switch them o separately. The greater the decrease in the solver's performance from disabling a heuristic, the greater is its bene t for the solver.
For the experiments there have been prepared the following solvers that are the variants of RLNT: RLNT itself, RLNT-noSLS, RLNT-noDL, RLNT-noCB, RLNT-noDIST, RLNT-noLCM, RLNT-noDL-noDIST. Here, RLNT followed by no* refers to the version of RLNT in which the heuristics corresponding to the solver name are disabled. The latter variant, RLNT-noDL-noDIST was evaluated because in the preliminary testing it showed good performance. In addition to that, in order to evaluate the progress in CDCL solvers from a slightly di erent perspective, the winners of SAT Competitions 2017-2019 were also included: MapleLCMDist, MapleLCMDistChronoBT, MapleLCMDistChronoBT-DL-v3. To o set them the versions of RLNT were prepared that coincide with the respective SAT competition winners in the enabled heuristics, e.g. RLNT-noSLS-noDL corresponds to MapleLCMDistChronoBT, RLNT-noSLS-noDL-noCB corresponds to MapleLCMDist. Finally, the version RLNT-noSLS-noDL-noCB-noDIST-noLCM is the variant in which all heuristics are disabled.
To accurately assess the performance of CDCL SAT solvers it is necessary to use a diverse set of benchmarks that come from di erent applications. The benchmark sets used in SAT Competitions appear to satisfy this criterion, thus in this paper, they were used in the experiments. In particular, the test instances from the main tracks of SAT Competitions 20162 and 20203, and also SAT Race 20194 were used. They are freely available from the corresponding 2 https://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=downloads 3 https://satcompetition.github.io/2020/downloads.html 4 http://sat-race-2019.ciirc.cvut.cz/index.php?cat=downloads websites. In total there were 1300 instances.
Remind, that when a SAT solver is launched with a xed time limit on some SAT instance, there are three possible outcomes. First, it can nd a satisfying assignment, meaning that a SAT instance is satis able. Second, it can prove that there are no satisfying assignments and thus the input formula is unsatis able. If the solver terminates due to the time limit, then the status of the instance is unknown. Overall, taking into account the fact that a formula can have many satisfying assignments, it may seem that satis able instances are signi cantly easier to tackle for a SAT solver, compared to unsatis able instances, for which it is required to construct a speci c proof. Empirical observations show that it is indeed true but to a limited extent. Both hard and simple cases of satis able and unsatis able instances are often encountered in practice.
In the experiments, each considered solver was launched once on each instance from the benchmark set. The outcome of the launch, together with the runtime of a solver was recorded. The statistics presented below include the count of solved instances, divided into counts for solved satis able and unsatis able ones. Similar to the SAT competitions, these numbers are accompanied by the PAR-2 score (Penalized Average Runtime with factor 2) which is computed as follows. First, a sum of terms is computed, where for each instance from the benchmark set the term is formed as a runtime of a solver if it solved this instance, or as 2 times the time limit if the solver did not. Then this sum is divided by the number of terms. Given the two solvers that solved the equal number of instances, the one with the lower value of PAR-2 is faster on average.
Following the standard SAT Competition procedure, all solvers were launched with a time limit of 5000 seconds. As a computing platform the PCs with 16-core AMD Ryzen 3950x CPUs and 32Gb RAM were used, operating under Ubuntu 20.10. The solvers were launched in 16 simultaneous threads without restrictions on memory usage.
The results of the experiments are summarized in Table 1. The so-called cactus plots, that present the performance of the solvers on satis able instances and unsatis able instances, are showed in Figures 1 and 2. The plotline for each solver displays the runtimes of this solver over all benchmarks, ordered in ascending order. It means that on the cactus plot, the further the plotline is to the right { the larger number of instances were successfully tackled by the corresponding solver within the time limit, and the closer the line is to the bottom { the smaller is the average runtime of a solver over all benchmarks.
The analysis of the results in Table 1, together with that presented in cactus plots at Figure 1 and 2 allows one to make several observations. First, it is quite clear that, at least on the employed benchmark set, the heuristics do not yield equal gain. The rst three rows of the Table clearly show, that dropping some of the heuristics increases the solver's performance. In particular, it appears that disabling DL or DIST allow RLNT to solve several more satis abile and unsatis able instances. Disabling them together yields even greater bene t. Therefore, it is necessary to reevaluate the combination of heuristics for each particular solver if the goal is to achieve the best possible performance. It means that when incorporating new heuristics into a solver, it is best to study how it ts into the general picture. However, this makes it much harder to perform straightforward fair comparisons. Another interesting observation that can be drawn from Figure 1 is the following: it is clear that the SLS heuristic appears to give the solver the ability to cope with at least 50 more satis able test instances from the considered set of benchmarks than the competition, which is quite surprising. It is the SLS heuristic that is responsible for the large gap between two groups of plot lines at Figure 1. On the other 3000 ) s d n o c e s ( e m i T2000 1000 0 0
MapleLCMDist MapleLCMDistChronoBT MapleLCMDistChrBt-DL-v3 RLNT-noSLS-noDL RLNT-noSLS-noDL-noCB RLNT-noSLS RLNT-noSLS-noDL-noCB-noDIST-noLCM RLNT-noDL-noDIST RLNT-noDIST RLNT-noCB RLNT-noDL RLNT RLNT-noLCM 50 100 150 200 250 300
350
Instances hand, from Table 1 it can be seen that dropping SLS results in a signi cant gain (about 30) in the number of unsatis able instances solved, which is, however, overshadowed by the decrease in the number of solved satis able tests. Apart from SLS, the next best heuristic appears to be LCM which mostly targets the unsatis able instances. The CB heuristic which helps the solver a lot with satis able instances takes third place. Another observation is that the overall architecture of SAT solvers indeed progressed slightly in recent years, since, for example, RLNT-noSLS-noDL shows better performance compared to MapleLCMDistChronoBT which uses the same set of heuristics.
Comparing the cactus plots at Figures 1 and 2 one can conclude that since 2017, the solvers started to switch focus to satis able instances, often at the cost of unsatis able ones. In particular, the MapleLCMDist solver from 2017 managed to solve the largest number of unsatis able instances and the smallest number of satis able ones out of all tested solvers. The switch in focus, however, is accompanied by overall progress that results in decreasing the average solver runtimes.
Now, let us look at the detailed statistics on satis able and unsatis able instances solved by each solver in three benchmark sets, corresponding to SAT Competition 2016 (SC2016), SAT Race 2019 (SR2019), and SAT Competition 2020 (SC2020). It is presented in Table 2. The horizontal line after the sixth row separates the solvers with SLS and the solvers without this heuristic. Observe, that for both SC2016 and SR2019 the enabling of SLS leads to the increase of the number of satis able instances solved by a moderate amount, from 3 to 12. On the other hand, for SC2020 the di erence induced by SLS is at least 25 instances. It means that the benchmark set for SC2020 is (hopefully, inadvertently) biased towards the SLS heuristic. As it was mentioned above, enabling SLS in all cases results in the decrease of unsatis able instances solved, but by a relatively small amount. From the analysis of other results, it can be conjectured, that the benchmark set from SC2016 is biased towards LCM, but to a signi cantly smaller degree. Observe that disabling LCM results in 10 less unsatis able instances solved in all cases. As for the SR2019 benchmark series, it appears to be more or less balanced and does not appear to be biased towards any speci c heuristic. However, it should be taken into account that the proportion of satis able instances solvable under a time limit to that of unsatis able instances. From Table 2 it is clear that SC2016 favors heuristics targeting unsatis able instances, while SR2019 and SC2020 benchmark sets are better for solvers with heuristics that work well on satis able instances.
RLNT-noDL-noDIST RLNT-noDIST RLNT-noDL RLNT RLNT-noCB RLNT-noLCM RLNT-noSLS-noDL MapleLCMDistChronoBT-DL-v3 RLNT-noSLS-noDL-noCB RLNT-noSLS RLNT-noSLS-noDL-noCB-noDIST-noLCM MapleLCMDistChronoBT MapleLCMDist
Taking into account all of the above, it is quite clear, that from the point of view of application domains, where the majority of SAT instances to solve are unsatis able, the modern CDCL heuristics are not very enticing. On the other hand, the domains which work mainly with satis able instances are likely to bene t from using the cutting-edge SAT competition winners. Overall, the more heuristics exist { the better, because since SAT is the NP-complete problem, it means that in advance, no one can predict whether some heuristic will work on the particular class of instances or not. That is why the choice makes the area richer with possibilities for improvement.
The results of the computational experiments indicate that in the CDCL SAT solvers that employ many separate heuristics it is important to sometimes spend time on reviewing their performance and tuning the existing con gurations because sometimes disabling a heuristic can result in the performance gain comparable to that from adding a brand new one. The predispositions of some heuristics towards satis able or unsatis able instances should also be factored into the choice of whether to employ them in each particular practical case.
The research was supported by the RFBR grant No.19-07-00746. [3] Moskewicz M W, Madigan C F, Zhao Y, Zhang L and Malik S 2001 Cha : Engineering an e cient SAT solver Proceedings of the 38th Annual Design Automation Conference DAC '01 pp 530{535 [4] Luby M, Sinclair A and Zuckerman D 1993 Inf. Process. Lett. 47 173{180 [5] Audemard G and Simon L 2009 Predicting learnt clauses quality in modern SAT solvers IJCAI pp 399{404 [6] Luo M, Li C, Xiao F, Manya F and Lu Z 2017 An e ective learnt clause minimization approach for CDCL
SAT solvers IJCAI pp 703{711 [7] Xiao F, Luo M, Li C M, Manya F and Lu Z 2017 MapleLRB LCM, Maple LCM, Maple LCM Dist, MapleLRB LCMoccRestart and glucose-3.0+width in SAT competition 2017 Proc. of SAT Competition 2017 vol B-2017-1 pp 22{23 [8] Nadel A and Ryvchin V 2018 Chronological backtracking SAT (LNCS vol 10929) pp 111{121 [9] Kochemazov S, Zaikin O, Semenov A A and Kondratiev V 2020 Speeding up CDCL inference with duplicate learnt clauses ECAI 2020 (FAIA vol 325) pp 339{346 [10] Zhang X and Cai S 2020 Relaxed backtracking with rephasing Proc. of SAT Competition 2020 vol B-2020-1 pp 15{16 [11] Een N and Sorensson N 2004 An extensible sat-solver SAT 2004 (LNCS vol 2919) pp 502{518 [12] Oh C 2015 Between SAT and UNSAT: The fundamental di erence in CDCL SAT SAT (LNCS vol 9340) pp 307{323