On Incremental Satis ability and Bounded Model Checking Siert Wieringa Aalto University , Finland 1954 1954

Introduction

Model checking is a formal veri cation technique Bounded Model Checking (BMC) is a symbolic revolving around proving temporal properties of model checking technique in which the existence systems modelled as nite state machines. A of a counterexample of a bounded length is rep- property holds for the model if it holds in all posresented by the satis ability of a propositional sible execution paths. If the property does not logic formula. Although solving a single instance hold this can be witnessed by a counterexample, of the satis ability problem (SAT) is su cient to which is a valid execution path for the model in decide on the existence of a counterexample for which the property does not hold. Because the any arbitrary bound typically one starts from model has a nite number of states any in nite bound zero and solves the sequence of formu- execution of the system includes a loop, and can las for all consecutive bounds until a satis able thus be represented by a nite sequence of exeformula is found. This is especially e cient in cution steps. Bounded Model Checking (BMC) the presence of incremental SAT-solvers, which [ 1 ] is a symbolic model checking technique in solve sequences of incrementally encoded formu- which the existence of a counterexample conlas. In this article we analyze empirical results sisting of a bounded number of execution steps that demonstrate the di erence in run time be- is represented by the satis ability of a proposihavior between incremental and non-incremental tional logic formula. It thus allows the use of SAT-solvers. We show a relation between the ob- decision procedures for the propositional satis served run time behavior and the way in which ability problem (SAT) for model checking. Dethe activity of variables inside the solver propa- spite the theoretical hardness of SAT [ 7 ] such degates across bounds. This observation has not cision procedures, called SAT-solvers [ 9, 14, 17 ], been previously presented and is particularly have become extremely e cient. BMC is popuseful for designing solving strategies for paral- ular as a technique for refuting properties, and lelized model checkers. although BMC based techniques can be used for proving properties we do not consider such techniques here.

Financially supported by the Academy of Finland A typical BMC encoding will have semantics project 139402 such that if there exists a counterexample of length k then there also exists a counterexam- ier to solve than the largest unsatis able ones. ple of any length greater than k. Thus in prin- A more opportunistic search strategy may reciple solving a single propositional logic formula duce the total time required to nd a satis able is su cient to decide on the existence of a coun- formula by skipping over hard instances. Such terexample for any arbitrary nite bound. How- strategies are natural for environments in which ever, one typically starts to solve the formula multiple computing nodes are available in paralcorresponding to bound zero and then solves se- lel, where one may de ne some nodes to use a quentially each consecutive bound until a coun- more opportunistic strategy than others. terexample is found. We will refer to this as the The observation on the empirical hardness of standard sequential search strategy. This strat- the smallest satis able formulas compared to the egy has the nice property that it always nds a largest unsatis able ones can also be made for counterexample of minimal length. As with ev- BMC. We attempted to implement opportunisery bound the representing formula grows larger tic strategies in our parallelized BMC framework it also avoids solving unnecessarily large formu- Tarmo [ 18 ]. This however turned out to be less las. Importantly, the performance of this strat- e cient then we would have expected, with peregy bene ts greatly from the availability of incre- formance degrading for many benchmarks. In mental SAT-solvers. Incremental SAT-solvers this article we evaluate the performance of the can solve sequences of formulas that share large incremental solver and compare it against that parts in common e ciently in a single solver pro- of solving each bound separately. The purpose cess, allowing reuse of information between for- of this study is not to illustrate that incremenmulas. tal solvers are more e ective for BMC than nonincremental ones, as that is well known, but to understand when and how opportunistic strate2 Motivation gies can be applied. This is done by comparing against non-incremental solver run times beAutomated SAT based planning is a problem cause solvers applying opportunistic strategies closely related to BMC. It deals with the same bene t less from the incremental interface of the sequences of parameterized formulas, except solver, as the problem is no longer introduced that the satis ability of a formula now corre- one bound at a time. sponds to the existence of a plan of a bounded length. In [15] evaluation strategies for planning were suggested that are more opportunis- 3 Preliminaries tic than the standard sequential search strategy.

They suggest to spend some amount of the to- The majority of modern SAT-solvers are based tal solving e ort at attempting to solve formu- on the Davis Putnam Logemann Loveland las for bounds ahead of the currently smallest (DPLL) procedure [8]. The DPLL-procedure is unsolved one. It was inspired by the empirical a backtracking search procedure for SAT that observation that if a plan exists then amongst builds a partial assignment by iteratively decidthe smallest satis able formulas in the sequence ing on a branching variable to be assigned a there are typically formulas that are much eas- value in the partial assignment. When the partition of the search space de ned by the partial out the need for integrating them into one appliassignment is without solutions the algorithm cation. The input sequences used were the same backtracks. In addition to this modern SAT- as the benchmarks used for experimental results solvers typically employ con ict clause learning presented in [ 18 ]. These sequences were gener[ 17 ]. Such solvers record a new con ict clause ated with the current state-of-the-art encoding whenever they are forced to backtrack. They for model checking of linear time temporal logic then backtrack non-chronologically to a decision properties with past (PLTL) [ 2 ] as implemented point at which the con ict clause was still satis- in the model checker NuSMV 2.4.3 [ 6 ]. ed.

The performance of the DPLL-procedure depends heavily on its branching variable decisions. 4 Run time A commonly used decision heuristic for clause learning SAT-solvers is the Variable State Inde- In our experiments we have studied the behavpendent Decaying Sum (VSIDS) heuristic rst ior of SAT-solvers on problem sequences from presented in the solver Cha [14]. The idea of BMC regarding both the run time and variable the heuristic is to favor variables that are in- activity. A selection of the results is presented in cluded in recently derived con ict clauses. For the gures in this article. For each benchmark each variable an initially zero value called the ac- there are two sub gures, a run time graph lativity is maintained. Whenever a con ict clause beled (a) and a variable activity graph labeled is learnt the activity of all variables that occur in (b). In this section we will focus only on the run the clause is increased. Periodically the activity time graphs, which have bounds on the x-axis of all variables is divided by a constant. and time on the y-axis. For each bound a ver

All results presented in this article were ob- tical bar displays the time it took to solve the tained using the SAT-solver MiniSAT 2.2.0 [ 9 ]1. formula corresponding to that single bound usThe solver core was not modi ed but a num- ing the SAT-solver in non-incremental fashion. ber of small modi cations2 were made in aux- If the solver found unsatis able a solid red bar iliary routines such as the le parser in order is drawn, if the solver found satis able only the to read incremental SAT sequences from disk. outline of the bar is drawn in green. When employing BMC typically the SAT-solver The incremental solver solves using the stanwill not read the formula sequence from disk but dard sequential strategy and whenever it comit will rather be integrated into a BMC engine pletes a bound it reports the run time up to that is generating formulas for new bounds on that point. The points in the graphs marked the y. We use sequences stored on disk as this with crosses (x) and connected by the thick line is convenient for testing the performance of the represent these run times.

SAT-solver independently. As our sequences are The thin dotted line connecting the plusses streamable one can also use them as an interface (+) is representing the cumulative run time of between a BMC engine and a SAT-solver with- the non-incremental solver, i.e. for each bound k the value displayed is the sum of all run times 1Available from http://www.minisat.se of the non-incremental solver tests from bound 2Available from http://users.ics.tkk.fi/swiering 0 to k. This demonstrates the time required ) s ( 1000 500 (a)

80 bound 20 40 60 100 120 140 0 0 20 40 60 (b)

80 bound 100 120 140 for the standard sequential strategy using a non- a way that is easy to update when the bound on incremental solver. This line is intentionally not the length of the execution paths is extended. in uencing the range of the y-axis, as it typically The solver can be thought of as having tuned itgrows so large that it would make the other re- self towards verifying the property holds in the sults hard to see. exact same way over and over.

From Fig. 1(a) it can be seen that the shortest lfttsssscbSbbeuhhapmmocAeonrteaui5uTraatgiot7nsenhlltrb-slltdhdeuseoeesarosssnnfreb5attlers1av3hlttxvote0hei.hesiearsr4emaefsdTmaoto.aacepidrhlppfnsblam2reeplodlroaneaeuaogfrmter1ubrleflgfat0tosbynlohuetF5rorcetntmsiuaahuibgfhimnnnrosuen.eoetdrolnsewhi2mancarsrc(os1eut-huawo0liitsnman)silfht6esatcrte,vtasiaarthmvheretibteebrkamhcmeullteouegynbceehirishoefsenrlraoonasesttvfnrsrs-hatfoimeigop.ooluenbdserforna.cems.unlrnod[tltsAe1delechhIevm65airhtneane]moe,tlrgtiemifnshttaaifwtitaa.asrotnoaelnnykyooer-f.l tttttssoqbFiiioheopuoiaomalgeApeulnvtr.enhoneu,cnsc3rrhetdnoab.etr(tsnucaeatthaodohetn)hFteeusfaiiaroaitgssnvstfetrpywotiidopatecriabwhsrrbmahyseearieettxnnulettrirhaacalntoaeaebyhmtrt.tsrlueylmeoeyopBrgwoafaaulityiekiereltsshdkshifoaiint.focssenftooglrgeirlfwctseoacohtitninerrhuhethmlggehreyeartlueihpspsttnlsdtfoahru1aoutiolirh5nlvlcsbteh0reodfclopr,ookreaturrmrpiitrineoeghdnetssndhehpedpsfenooloteeorathnqrsnofSreceduvgAdrartiieesiunTnnhnpisennygget---opportunistic strategy could possibly be bene cial. An incremental solver can be started from

Note that all results presented in this arti- any arbitrary bound, and it is possible to procle demonstrate that the use of the incremental ceed by increasing the bound by more than one solver is crucial when performing the standard every time a formula is solved. Using bound sequential strategy. Fig. 3(a) presents run time increments larger than one is one of the simbehavior for the benchmark eijk.S1238.S which ple strategies we have tried in our experiments. is the encoding of model checking a property that This strategy should still be considered opporholds on all execution paths of the model. This tunistic because of the \missing information" it implies that the formulas are unsatis able for all causes for the solver, leading it further away from bounds. Here, the crucial role that incremen- the e ciency of incremental solving, and further tal SAT solving often plays in solving BMC is towards non-incremental behavior. Given the even clearer. Whereas a non-incremental solver small margin of error available for opportuniswould take about 100 seconds to nd that bound tic approaches for satis able benchmarks, and 150 alone is unsatis able, the incremental solver no chance of any performance improvement for nds this result for all bounds from 0 to 150 se- many unsatis able benchmarks, we need to be quentially in half that time. This is typical be- careful when applying these approaches. They havior for many benchmarks corresponding to are however amongst the most natural ways of model checking a property that holds. It seems diversifying search strategies amongst nodes in that in these cases the solver learns that the an environment with parallel computation reproperty holds for all short execution paths in sources.

Parallel SAT solving

seems that the interrupted solver is missing more information than just con ict clauses. This was There are two common architectures for parallel one of the reasons to look at the way the activSAT-solvers [ 11 ]. The rst is the classic divide- ity of variables propagates across bounds on the and-conquer approach in which the formula is incremental SAT-solver runs. split into multiple disjoint subformulas each of which are then solved on a di erent computing node [ 4, 19 ]. The second approach is the 6 Variable activity so called portfolio approach [ 10 ]. The basic idea is that every computing node is running a SAT- To obtain data on the activity of variables the solver that is attempting to solve the same for- SAT-solver was modi ed to print the activity of mula. As modern SAT-solvers make some deci- all variables after each bound it completed. For sions randomly their run time varies greatly be- each bound we are interested in which variables tween runs. This makes the portfolio approach are the most active, and especially in whether surprisingly e cient as it is able to decide the this activity remains high across several bounds. satis ability of the formula as soon as the fastest We consider a variable hyperactive if its activity solver nishes. Further diversi cation may be is within the highest 2% of variables with nonachieved by using di erent parameters on di er- zero activity. ent computation nodes. Obviously opportunistic The graphs labeled (b) in this article visualsearch strategies provide means for diversi ca- ize the hyperactive variables. All variables that tion when we are considering solving incremen- are hyperactive for at least one bound are reptally encoded SAT formulas in a parallel envi- resented by an integer value on the y-axis of the ronment. graph. The variables are sorted on the y-axis

The current implementation of our paral- by their index such that if we de ne y(v) as the lelized BMC framework Tarmo can be seen as integer on the y-axis corresponding to the varia parallelized incremental SAT-solver using the able with index v then for any v0 > v we have portfolio approach. Each computing node is run- y(v0) > y(v). ning an incremental SAT-solver in the conven- Just like in the run time graphs the values on tional sequential fashion. The novelty of Tarmo the x-axis of the graph represent bounds. If a is that it allows sharing of con ict clauses be- variable was hyperactive starting from bound k tween SAT-solvers even if they are working on up to but not including bound k0 > k then a hordi erent bounds. The solvers operate otherwise izontal line was drawn in the graph from bound independently, i.e. if one solver solves a formula k to k0 at the y position corresponding to that this does not stop the other solvers from at- variable. In other words for all variables v and all tempting to solve that same formula. This choice bound intervals [k; k0) on which v is hyperactive was made after observing that interrupting a a line was drawn from (k; y(v)) to (k0; y(v)). solver to make it \catch-up" with another breaks One may observe that generally variables with its ability to bene t from incremental SAT to the larger indices become active later. This is befull extent. As we made this observation in an cause in the solver each newly introduced varienvironment where clause sharing takes place it able is given a larger index than all existing vari20

40 60 (a)bound80 60 (b) bound80 20 40 100 120 140 100 120 140 ables, and for each bound a set of new variables is bound local. created. For each bound a subset of the new vari- We have generated graphs like the ones preables becomes hyperactive quickly, as the solver sented in this paper for a large set of benchruns into con icts on the newly added clauses. marks3. We observe that on benchmarks with

The hyperactive variables in the satis able a bound global variable activity the run time of benchmarks irst.dme6 and bc57sensors.p2neg the non-incremental SAT-solver for the largest are displayed in Fig. 1(b) and Fig. 2(b). Note bound solved is smaller than the time spent for that although for each bound some of the new the incremental solver to get to the same bound variables become hyperactive all these vari- and solve it. For benchmarks with a bound loables tend to remain hyperactive throughout the cal variable activity this is never the case and whole process. This means that whenever a thus a opportunistic heuristic will not improve bound is added the solver still runs into new con- performance.

icts regarding variables that represent the state Although we expect all hard satis able benchat smaller timepoints. We say that the activity marks to have a bound global variable activity it of variables is bound global. is not the case that all unsatis able benchmarks have a bound local variable activity. The bench

For the benchmark eijk.S1238.S the activity mark abp4.ptimoneg represented in Fig. 6 is an graph looks very di erent. For each bound the example of an unsatis able benchmark with a solver creates con ict clauses including the new bound global variable activity. Apparently the variables, thus creating a new set of hyperactive correctness of the property is not implied within variables, but there are only very few variables a short number of execution steps here, and the for which hyperactivity is maintained. This is in incremental solver needs to evaluate large porline with observation on the run time behavior of tions of the search space for every bound. Note this benchmark which also indicate that hardly also that for this benchmark an opportunistic apany work has to be performed to nd unsatis ability. We say that the activity of variables is 3Available from http://users.ics.tkk.fi/swiering 7

 Conclusions

proach may help to nd unsatis able formulas at to the solver. Tolerance to bad choices for such larger bounds faster. an incremental encoding could be achieved by doing this in a parallel environment with some opportunistic nodes.

In this article we have shown a relation between the run time of the standard sequential strategy for bounded model checking and the activity of decision variables in solvers employing this strategy. We can use this observation in a SATsolver to predict during the search whether a more opportunistic strategy could be bene cial for the search. This is especially useful for parallel solvers in which di erent threads may be executing di erent strategies.

It is also easy to envision how these techniques could be useful for model checkers that use a combination of truly di erent model checking techniques such as PdTrav [ 5 ]. One could easily engineer a system which would do BMC for some amount of time, after which the variable activity could play a role in the decision on how to continue. If the variable activity appears to be bound local then the property is likely to hold for the model and thus we may want to start doing a complete model checking technique based on for example k-induction [16], Craig interpolation [ 13 ] or BDDs [12] to prove this.

Another observation we made is that for deciding the satis ability of the last formula in an incrementally encoded sequence of formulas it can sometimes be faster to solve all formulas in the sequence. This raises the question whether other applications of SAT solving that currently rely on solving a single SAT formula could bene t from the use of incremental problem encodings. Such encodings allow enforcing a search direction on the SAT-solver that is natural to the application and therefore possibly bene cial

Symbolic model

 [1] Armin Biere , Alessandro Cimatti, Edmund M. Clarke , and Yunshan Zhu . Symbolic model checking without BDDs . In Rance Cleaveland, editor, TACAS , volume 1579 of Lecture Notes in Computer Science, pages 193 { 207 . Springer, 1999 . [2] Armin Biere , Keijo Heljanko, Tommi A. Junttila , Timo Latvala, and Viktor Schuppan . Linear encodings of bounded LTL model checking . Logical Methods in Computer Science , 2 ( 5 ), 2006 . [3] Armin Biere and Toni Jussila . Hardware model checking competition 2007 (HWMCC07). Organized as a satellite event to CAV 2007 , Berlin, Germany, July 3- 7 , 2007 . [4] Max Bohm and Ewald Speckenmeyer . A fast parallel SAT-solver - e cient workload balancing . Ann. Math. Artif. Intell., 17 ( 3- 4 ): 381 { 400 , 1996 . [5] Gianpiero Cabodi , Paolo Camurati, Luz Garcia, Marco Murciano, Sergio Nocco, and Stefano Quer . Trading-o SAT search and variable quanti cations for e ective unbounded model checking . In Alessandro Cimatti and Robert B . Jones, editors, FMCAD , pages 1{8 . IEEE, 2008 . [6] Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Se- in Computer Science , pages 1 { 12. Springer, bastiani, and Armando Tacchella. NuSMV 2005 . 2: An opensource tool for symbolic model checking . In Ed Brinksma and Kim Guld- [14] Matthew W. Moskewicz , Conor F. Madistrand Larsen, editors, CAV , volume 2404 of gan, Ying Zhao, Lintao Zhang, and Sharad Lecture Notes in Computer Science , pages Malik. Cha : Engineering an e cient SAT 359{364 . Springer, 2002 . solver. In DAC , pages 530 { 535 . ACM, 2001 . [7] Stephen A. Cook. theorem -proving procedures . pages 151{158. ACM , 1971 . The complexity of [15] Jussi Rintanen , Keijo Heljanko, and Ilkka In STOC, Niemela. Planning as satis ability: parallel plans and algorithms for plan search . Artif. Intell., 170 ( 12 -13): 1031 { 1080 , 2006 . [9] Niklas Een and Niklas Sorensson. An extensible SAT-solver . In Enrico Giunchiglia and Armando Tacchella , editors, SAT , volume 2919 of Lecture Notes in Computer Science, pages 502 { 518 . Springer, 2003 . [13] Kenneth L. McMillan . Applications of Craig interpolants in model checking . In Nicolas Halbwachs and Lenore D. Zuck, editors, TACAS , volume 3440 of Lecture Notes [10] Youssef Hamadi , Sad Jabbour, and Lakhdar Sais. ManySAT: A parallel SAT solver . JSAT , 6 ( 4 ): 245 { 262 , 2009 . [11] Antti Eero Johannes Hyvarinen, Tommi A. Junttila, and Ilkka Niemela. Partitioning search spaces of a randomized search . In Roberto Serra and Rita Cucchiara , editors, AI*IA , volume 5883 of Lecture Notes in Computer Science, pages 243 { 252 . Springer, [ 19 ] Hantao Zhang , 2009 . [17] Jo ~ao P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satis ability . IEEE Trans. Computers , 48 ( 5 ): 506 { 521 , 1999 . [18] Siert Wieringa , Matti Niemenmaa, and Keijo Heljanko . Tarmo: A framework for parallelized bounded model checking . In Lubos Brim and Jaco van de Pol, editors, PDMC , volume 14 of EPTCS , pages 62 { 76 , 2009 . Maria Paola Bonacina, and Jieh Hsiang. PSATO: A distributed propositional prover and its application to quasigroup problems . J. Symb. Comput. , 21 ( 4 ): 543 { 560 , 1996 .