An Empirical Evaluation of SAT Solvers on Bit-vector Problems

Abstract

Bit blasting is the main method for solving SMT problems in the theory of xed size bit vectors. It converts bit-vector problems to equisatis able Boolean satis ability problems that are then solved by SAT solvers. We present an empirical evaluation of state-of-the-art SAT solvers on problems produced by bit blasting with the Yices SMT solver. The results are quite di erent from common SAT solver evaluations such as the SAT races and SAT competitions, which argues for extending these evaluations to include benchmarks derived from SMT problems.

Introduction

Our evaluation is based on 15447 CNF problems that we generated from non-incremental benchmarks in the logic QF BV (quanti er-free, xed size bit vectors). These benchmarks are available on the SMT-LIB repository.3 We started from the 41696 benchmarks available in this repository as of July 2019.

Solver

MapleCOMSPS MapleCOMSPS LRB MapleLCMDiscChronoBT-DL-v3 MapleLCMDistChronoBT MapleLCMDistChronoBT-DL-v1 MapleLCMDistChronoBT-DL-v2.1 MapleLCMdistCBTcoreFirst Maple LCM Dist PSIDS MapleCMDistChronoBT cadical-1.2.1 cadical-satrace19 cryptominisat5 expMaple CM GCBumpOnlyLRB glucose-4.2.1 minisat-2.2.0-simp smallsat

Reason for inclusion

Winner SAT Competition 2016 Accident 1st in UNSAT Track, 1st in SAT+UNSAT at SatRace 2019 Winner SAT Competition 2018 2nd in SAT Track at SatRace 2019 2nd in SAT Track at SatRace 2019 3rd SAT+UNSAT Track at SatRace 2019 Winner SAT Competition 2017 3rd in UNSAT Track at SatRace 2019 latest CaDiCaL release 1st in SAT Track, 2nd in SAT+UNSAT at SatRace 2019 historic 2nd in UNSAT Track at SatRace 2019 historic historic 3rd in SAT Track at SatRace 2019

We processed all these benchmarks with the Yices 2 SMT solver [ 5 ] to convert them to the DIMACS CNF format used by SAT solvers. Out of the initial 41696 benchmarks, Yices 2 can solve 18940 problems without conversion to CNFs (i.e., by rewriting and other simpli cation at the bit-vector level). We obtained then 22756 CNF formulas in total. We then removed trivial formulas and duplicates. There were 325 empty CNFs (trivially SAT), 2685 formulas that contained the empty clause (trivially UNSAT), and 4286 duplicates. This leaves 15450 formulas. Out of them, we decided to remove three extremely large CNF formulas (of more than 5 GB each) and keep the remaining 15457 formulas for our evaluation.

By a duplicate, we mean a CNF le that is syntactically identical to another benchmark; it contains the exact same variables and clauses in the same order. We did not attempt to identify formulas that are identical modulo variable or clause reordering. It may be somewhat surprising that problems in SMT-LIB that are syntactically distinct result in the exact same CNF after bit blasting. We have not investigated this issue very much and we do not know whether this happens with other SMT solvers than Yices 2. But this may suggest removing possibly redundant problems from SMT-LIB.

The formulas resulting from this bit blasting vary widely in size. The smallest formula has two variables and two clauses. The largest formula has more than 9 million variables and 41 million clauses. Such very large examples are present but they are not common. The median number of variables is 9115 and the median number of clauses is 29307. All these CNF benchmarks are available at https://www.csl.sri.com/~bruno/bit-blasting.html. 3

Solvers

by GRASP [ 13 ] and Cha [ 14 ]. Except for CaDiCaL and CryptoMiniSAT, all the solvers are derived from MiniSAT [ 7 ] via Glucose [ 1 ] and COMiniSATPS [ 16, 17 ] and still share a lot of code with MiniSAT 2.2.0. They employ techniques introduced by MiniSAT and its successors: learned clause minimization [ 7 ], preprocessing with variable and clause elimination [ 6 ], glue-based estimates of learned clause quality [ 2 ]. In addition to these common bases, recent solvers employ techniques such as vivi cation of learned clauses [ 12 ], chronological backtracking [ 15 ], and new branching heuristics [ 11 ]. Additional details on each solver and the particular techniques they implement can be found in the SatRace proceedings [ 10 ].

CryptoMiniSAT [ 20 ] also derives from MiniSAT but it is now very di erent. Unlike other MiniSAT-derived solvers, CryptoMiniSAT implements the in-processing strategy, and includes many more simpli cation techniques. CaDiCaL does not borrow code from MiniSAT and it also uses in-processing. All other solvers in our list work in two phases. They rst simplify the input formula using variable and clause elimination algorithms. After this preprocessing, they switch to pure CDCL search and perform only limited clause simpli cation during search. The in-processing strategy uses simpli cation procedures more aggressively. Rather than just performing one round of initial simpli cation, in-processing solvers apply these simpli cation procedures periodically, They alternate between search and simpli cation. This strategy is used by both CaDiCaL and CryptoMiniSAT. Both solvers also implement many more simpli cation techniques than the others. 4

Experiment

We ran the solvers listed in Table 1 on the 15447 benchmarks produced by Yices 2. For the experiment, we used a set of ten Linux-based servers running Ubuntu 18.04. All servers have 64 GB RAM and have two four-core x86-64 Intel processors (Xeon Gold 5122 Processors, 16.5M Cache, 3.60 GHz). We used a timeout of 20 minutes CPU time per benchmark and did not set a memory limit.

On these servers, solver runtime may be a ected by hard-to-predict OS and hardware characteristics. We purposely limited the number of jobs on each server (two jobs per server) to reduce variability. By running the same binary multiple times, we observed variation in runtime of about 4% between the fastest and slowest run. This variability must be taken into account when comparing solver runtimes. Ideally, we should run the same solvers multiple times to get averages but we did not have enough time for this. Our primary performance metrics is the number of solved benchmarks, which is less sensitive to small runtime variability.

We ran all the solvers in Table 1 once on all the benchmarks. All solvers were run with default con gurations (i.e., no command-line options), but we disabled generation of DRAT proofs. To perform the experiments, we had to address a few software issues: We xed a division-by-zero bug in the smallsat solver.

A more signi cant problem is that many, if not all, of the MiniSAT-derived solvers do not respect the SIGXCPU signal which we used for timeout. We set a runtime limit with the shell ulimit command. When the limit is reached, the OS sends the solver the SIGXCPU signal, which by default should terminate the process. Solvers intercept this signal and implement a signal handler that is intended to print statistics when the solver is interrupted. This mechanism seems to have been inherited from MiniSAT where it was working properly but the quality of implementation has not kept up. Many solvers just catch the signal and keep going. They cannot be interrupted by our timeout mechanism

(or by ctrl-C for that matters). We xed this issue by removing the faulty signal-handling code from all solvers.

We removed an incorrect warning produced by the DIMACS parser used by most MiniSATderived SAT solvers.

For the solvers that did not provide it, we added an option to disable printing of satisfying assignments on their standard output. This helped reduce the volume of data produced by solvers from gigabytes to more manageable sizes.

We note that many of the MiniSAT-derived solvers do not build very cleanly. Compilation generates a very large number of warnings. Despite this, all the solvers appear to be reliable. We did not notice incorrect results from any solver. There was no disagreement between solvers on any benchmark that was solved by more than one of them. 5

Results

The results of our evaluation are shown in Tables 2 and 3. The rst table shows the number of solved instances by each solver. It also includes results for the virtual best solver.4 The second table shows runtime distributions.

A clear result is that both versions of CaDiCaL are signi cantly better on our benchmarks than the other solvers. MapleCOMSPS LRB is in third place and solves 68 fewer problems than CaDiCaL-1.2.1. The winner of last year's SAT race is fourth and solves close to 100 fewer problems than CaDiCaL-1.2.1. Other solvers that did well in this SAT race are further behind.

4The virtual best solver is obtained by selecting the fastest solver on each problem.

Solver cadical-1.2.1 cadical-satrace19

MapleCOMSPS LRB MapleLCMDiscChronoBT-DL-v3 expMaple CM GCBumpOnlyLRB

cryptominisat5

Maple LCM Dist

MapleLCMDistChronoBT

MapleLCMdistCBTcoreFirst

MapleLCMDistChronoBT-DL-v1 MapleLCMDistChronoBT-DL-v2.1

smallsat

MapleCOMSPS PSIDS MapleCMDistChronoBT

glucose-4.2.1 minisat-2.2.0-simp virtual best

1 s 11850 11872 10732 7753 10006 11253 7717 7733 7715 7775 7768 10815 10671 7686 12188 11713 13233

Apart from MapleLCMDiscChronoBT-DL-v3, solvers from 2019 do not seem particularly better than winners of past SAT competitions. It is also notable that two variants of MapleLCMDiscChronoBD-DL-v3 do much worse. In fact, the best solver after CaDiCaL is MapleCOMSPS LRB, which nished in 7th position in the 2016 SAT Competition. Interestingly, the winner that year was a variant of MapleCOMPSPS LRD which does not do well on our benchmarks. Also, MapleCOSMPS LRB does much better than more recent solvers that implement techniques such as chronological backtracking [ 15 ] and learned-clause vivi cation [ 12 ]. These new techniques seem to be useful on SAT-Competition benchmarks but their value is less clear here.

One can see that all solvers are signi cant improvements over MiniSAT. MiniSAT 2.2.0 is last in our table. It times out on 811 problems, which is close to 300 more timeouts than any other solver. It is actually handicapped by its poor results on a speci c family of benchmarks due to Bruttomesso and Sharygina [ 4 ]. All other solvers work ne on these benchmarks and we know that the benchmarks in question are unsatis able and have short resolution proofs. In fact, they can be solved by bounded variable elimination alone. Although MiniSAT implements bounded variable elimination, it puts limits on the procedure that prevents it form solving these benchmarks. In particular, MiniSAT uses a limit on the size of clauses created during variable elimination. This limit is 20 literals by default. When this limit is increased to 400 literals (using command-line option --cl-lim=400), MiniSAT solves 185 more problems in total.

Table 3 shows that most of our benchmarks are very easy for all solvers. A very large majority of the problems (75%) are solved in less than 10 s by all solvers. We still see di erences between solvers on these easy benchmarks, in particular in the number of instances solved within 1 s. On the other hand, more than 200 problems were not solved at all. We have built a smaller subset of \interesting" benchmarks that removes problems on which all solvers behave similarly. This list includes all problems that are solved by some but not all solvers. We also included e m i t 1200 1000 800 600 400 200 0 0

cadical-1.2.1 cadical-satrace19

MapleCOMSPS-LRB MapleLCMDiscChronoBT-DL-v3 expMaple-CM-GCBumpOnlyLRB cryptominisat5

Maple-LCM-Dist

MapleLCMDistChronoBT

MapleLCMdistCBTcoreFirst

MapleLCMDistChronoBT-DL-v1 MapleLCMDistChronoBT-DL-v2.1

smallsat

MapleCOMSPS PSIDS-MapleCMDistChronoBT

glucose-4.2.1 minisat-2.2.0-simp 200 400 600 800 1000 1200 1400 problems solved by all solvers when the di erence between fastest and slowest solvers was large (i.e., more than 100 s). This list of interesting problems contains 1354 instances. Figure 1 shows the traditional cactus plot for our solvers on these interesting problems. This plot visually shows what we described previously. Both versions of CaDiCaL are our best solvers, followed by MapleCOMSPS LRB and MapleLCMDistcChronoBT-DL-v3 then a group of ten solvers that are close to each other. Glucose-4.2.1 is then behind this group and MiniSAT is further to the left. 6

Playing with CaDiCaL

CaDiCaL [ 3 ] is one of the many SAT solvers developed by Armin Biere over the years. It is written in C++ and its code is available on GitHub.5 It started participating in the SAT competitions in 2017. In our study, we used the release 1.2.1 of CaDiCaL which was the latest release available at the time.

As we mentioned previously, CaDiCaL uses in-processing and implements a large number of di erent simpli cations and other specialized procedures. We experimentally investigate which of these features matter most on our benchmarks. For this purpose, we just turn o several options or features that are enabled by default in CaDiCaL then measure performance of the modi ed CaDiCaL. compacting:

chrono: decompose: eagersubsume:

elim: elimgates:

lucky: probing: rephase: scan-index :

stabilize: subsumption: ternary: vivify: walk : compacting internal variables support for chronological backtracking elimination of equivalent literals apply subsumption to recently learned clauses bounded-variable elimination recognize clauses that encode and, xor, and if-then-else try prede ned satisfying assignments failed-literal probing periodically switch preferred variable polarity optimized watched literal search switch between two heuristic modes clause subsumption hyper ternary resolution clause vivi cation random walks Among the many features implemented in CaDiCaL, we selected the subset shown in Figure 2. All of these are enabled by default and activate various simpli cation and search procedures available in CaDiCaL. Some of these are standard simpli cations such as variable elimination and subsumptions [ 6 ], and failed-literal probing. Chronological backtracking is based on [ 15 ]. Vivi cation was introduced by Piette et al. [ 18 ] and it is used in Luo et al.'s procedure for minimizing learned clauses [ 12 ]. It was also proposed by Han and Somenzi under the name distillation [ 9 ].

Compacting is a data-structure optimization procedure that makes internal tables more compact by removing empty slots and renumbering variables. Decomposition computes strongly connected components in the problem's binary implication graph to eliminate variables. It searches for implication cycles of the form: l0 ) l1 ) : : : ) ln ) l0; from which one can deduce that l1; : : : ; ln can all be replaced by l0. Eager subsumption keeps track of n most recently learned clauses and when a new clause C is learned, it checks whether C subsumes any of them. Under the name elimgates we refer to three options of CaDiCaL that enable code to recognize clausal encodings of common Boolean gates. These clauses can be treated specially during bounded variable elimination [ 6 ]. Lucky and walk refer to two procedures that attempt to quickly nd a satisfying assignment before executing the CDCL search procedure. Walk is a local search procedure. Lucky tries several assignments (e.g., set all variables to false or to true) to check whether they satisfy all the clauses. Rephase is a heuristic that periodically updates the preferred polarity used when assigning decision variables. Other solvers typically use the caching scheme due to Pipatsrisawat and Darwiche [ 19 ]. Rephasing introduces more diversity in this scheme. Stabilize enables CaDiCaL to essentially work in two modes in which di erent heuristics are used for selecting branching variables and controlling restarts. It is related to the distinction between SAT and UNSAT problems observed by Oh [ 16 ]. Ternary is a form of resolution limited to three (and two) literal clauses.

The scan-index feature is di erent from the others. It is not enabled or disabled by Disabled Feature

elim stabilize rephase scan-index

probing compacting

vivify subsumption

ternary decompose eagersubsume

lucky chrono

walk elimgates command-line options. Unique among all solvers in our list, CaDiCaL implements an optimal procedure for scanning a clause to search for a new watched literal [ 8 ]. This requires storing a scan index with the clause and searching from this scan index whenever a current watched literal becomes false. Other solvers use the simpler method of MiniSAT that does not require a scan index. They always scan a clause from the start. We wanted to evaluate the impact of this scan-index procedure. To disable it, we modi ed the CaDiCaL code to force scanning to start at the beginning of a clause.

Although some of the procedures listed in Figure 2 are also implemented by CryptoMiniSAT and other solvers, implementation details matter. CaDiCaL uses various optimizations that may not be implemented in other solvers. Checking the code is a good idea for full details. 6.2

Results of solved benchmarks should be taken with precaution since CaDiCaL is a randomized solver. We have tested CaDiCaL on our benchmarks with 18 di erent random seeds. In this test, the number of solved instances varied from 15156 to 15176, with an average of 15167.33 and a standard deviation of 4.59.

Table 4 gives us an initial picture of features of a state-of-the-art SAT solver like CaDiCaL that matter most for our bit-vector benchmarks. This study is far from complete, as CaDiCaL includes many more parameters and options than the ones we tested. We limited our experiments to Boolean features that can be turned on or o . Other aspects that are unique to CaDiCaL (such as the use of the move-to-front heuristic) are more di cult to investigate since they require signi cant code modi cation. 7

Conclusion

E cient SAT solvers are key to solving SMT problems in the theory of xed size bit vectors. Progress in SAT solving is hard to quantify. It is measured empirically on benchmarks used in regular SAT competitions. Unfortunately, it is not clear whether good performance in these SAT competitions correlate with good performance on SMT benchmarks. Our empirical evaluation shows that CaDiCaL is currently the best SAT solver on CNF problems produced with Yices 2, by a signi cant margin. Other solvers that are close to or better than CaDiCaL on SATcompetition benchmarks are not close in our evaluation. This implies that SAT-competition benchmarks are di erent and not representative of the SAT problems we produce by bit blasting.

Our initial investigation identi ed several features and procedures of CaDiCaL that seem to be most bene cial on our benchmarks. Some of these are not di cult to implement and could be easily added to other solvers. Other procedures such as chronological backtracking that have proved e ective in SAT competitions do not seem to help on our benchmarks.

Benchmarking is of course a di cult problem and our evaluation is still limited. We have heard that other SMT solvers than Yices work best with CaDiCaL too,6 but a larger experimental evaluation involving several solvers would be useful. We have not mentioned various potential issues with the SMT-LIB benchmarks (e.g., many hard problems are crafted or do not come from real application domains, there may be too many similar problems), and we have not thoroughly examined SAT solver performance on di erent benchmark families.

Acknowledgments

This material is based upon work supported in part by NSF grant 1816936, and by the Defense Advanced Research Project Agency (DARPA) and Space and Naval Warfare Systems Center, Paci c (SSC Paci c) under Contract No. N66001-18-C-4011. Any opinions, ndings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily re ect the views of NSF, DARPA, or SSC Paci c.

References

[1] Gilles Audemard and Laurent Simon . GLUCOSE: a solver that predicts learnt clauses quality . In SAT 2009 Competitive Events Booklet , pages 7 {9 , 2009 .

[2] Gilles Audemard and Laurent Simon . Predicting learnt clauses quality in modern SAT solvers . In Twenty-First International Joint Conference on Arti cial Intelligence (IJCAI'2009) , pages 399 { 404 , 2009 .

[3] Armin Biere . CaDiCaL at the SAT race 2019 . In Proceedings of SAT Race 2019: Solver and Benchmark Descriptions , pages 8 {9 , 2019 .

[4] Roberto Bruttomesso and Natasha Sharygina . A scalable decision procedure for xed-width bitvectors . In Proceedings of the 2009 International Conference on Computer-Aided Design (ICCAD'09) , pages 13 { 20 , 2009 .

[5] Bruno Dutertre . Yices 2.2 . In Armin Biere and Roderick Bloem, editors, Computer-Aided Veri - cation (CAV' 2014 ), volume 8559 of Lecture Notes in Computer Science, pages 737 { 744 . Springer, July 2014 .

[6] Niklas Een and Armin Biere . E ective preprocessing in SAT through variable and clause elimination . In Fahiem Bacchus and Toby Walsh , editors, Theory and Practice of Satis ability Testing (SAT 2005 ), volume 3569 of Lecture Notes in Computer Science, pages 61 { 75 . Springer, 2005 .

[7] Niklas Een and Niklas Sorensen. An extensible SAT-solver . In Enrico Giunchiglia and Armando Tacchella , editors, Theory and Applications of Satis ability Testing (SAT 2003 ), volume 2919 of Lecture Notes in Computer Science, pages 502 { 518 . Springer, 2003 .

[8] Ian P. Gent . Optimal implementation of watched literals and more general techniques . Journal of Arti cial Intelligence Research , 48 : 231 { 252 , 2013 .

[9] Hyojung Han and Fabio Somenzi . Alembic: An e cient algorithm for CNF preprocessing . In Proceedings of the 44th Annual Design Automation Conference (DAC'07) , pages 582 { 587 , 2007 .

[10] Marijn J.H. Heule , Matti Jarvisalo, and Martin Suda, editors. Proceedings of SAT Race 2019 : Solver and Benchmark Descriptions . Department of Computer Science, University of Helsinki, 2019 . http://hdl.handle.net/10138/306988.

[11] Jia Hui Liang , Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki . Learning rate based branching heuristic for SAT solvers . In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satis ability Testing (SAT 2016 ), volume 9710 of Lecture Notes in Computer Science, pages 123 { 140 . Sprnger , 2016 .

[12] Mao Luo , Chu-Min Li , Fan Xio , Felip Manya, and Zhipeng Lu. An e ective learnt clause minimization approach for CDCL SAT solvers . In Proceedings of the 26th International Joint Conference on Arti cial Intelligence , pages 703 { 711 , 2017 .

[13] Joa ~o P. Marques-Silva and Karem A. Sakallah. GRASP - a search algorithm for propositional satis ability . IEEE Transactions on Computers , 48 ( 5 ): 506 { 521 , May 1999 .

[14] Matthew W. Moskewicz , Conor F. Madigan, Ying Zhao , Lintao Zhang , and Sharad Malik . Cha : Engineering an e cient SAT solver . In Proceedings of the 38th annual Design Automation Conference (DAC'01) , pages 530 { 535 , June 2001 .

[15] Alexander Nadel and Vadim Ryvchin . Chronological backtracking . In Olaf Beyersdor and Christoph M. Wintersteiger, editors, Theory and Applications of Satis ability Testing (SAT 2018 ), volume 10929 of Lecture Notes in Computer Science, pages 111 { 121 . Springer, 2018 .

[16] Chanseok Oh . Between SAT and UNSAT: The fundamental di erence in CDCL SAT . In Marijn Heule and Sean Weaver, editors, Theory and Applications of Satis ability Testing (SAT 2015 ), volume 9340 of Lecture Notes in Computer Science, pages 307 { 323 . Springer, 2015 .

[17] Chanseok Oh . Patching MiniSat to deliver performance of modern SAT solver . In SAT Race Solver Description , 2015 .

[18] Cedric Piette , Youssef Hamadi, and Lakhdar Sas. Vivifying propositional clausal formulas . In 18th European Conference on Arti cial Intelligence (ECAI 2008 ), Frontiers in Arti cal Intelligence and Applications , pages 525 { 529 . IOS Press, 2008 .

[19] Knot Pipatsrisawat and Adnan Darwiche . A lightweight component caching scheme for satis ability solvers . In Joa~o Marques-Silva and Karem A . Sakallah, editors, Theory and Applications of Satis ability Testing (SAT 2007 ), volume 4501 of Lecture Notes in Computer Science, pages 294 { 299 . Springer, 2007 .

[20] Mate Soos , Karsten Nohl, and Claude Castelluccia . Extending SAT solvers to cryptographic problems . In Oliver Kullmann, editor, Theory and Applications of Satis ability Testing (SAT 2009 ), volume 5584 of Lecture Notes in Computer Science, pages 244 { 257 . Springer, 2009 .