On Incremental Satisfiability and Bounded Model Checking Siert Wieringa∗ Aalto University, Finland siert.wieringa@aalto.fi Abstract 1 Introduction Model checking is a formal verification technique Bounded Model Checking (BMC) is a symbolic revolving around proving temporal properties of model checking technique in which the existence systems modelled as finite state machines. A of a counterexample of a bounded length is rep- property holds for the model if it holds in all pos- resented by the satisfiability 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 satisfiability problem (SAT) is sufficient 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 finite number of states any infinite bound zero and solves the sequence of formu- execution of the system includes a loop, and can las for all consecutive bounds until a satisfiable thus be represented by a finite sequence of exe- formula is found. This is especially efficient 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 con- las. In this article we analyze empirical results sisting of a bounded number of execution steps that demonstrate the difference in run time be- is represented by the satisfiability of a proposi- havior 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 satisfi- served run time behavior and the way in which ability problem (SAT) for model checking. De- the activity of variables inside the solver propa- spite the theoretical hardness of SAT [7] such de- gates across bounds. This observation has not cision procedures, called SAT-solvers [9, 14, 17], been previously presented and is particularly have become extremely efficient. BMC is pop- useful 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 tech- niques 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 unsatisfiable ones. ple of any length greater than k. Thus in prin- A more opportunistic search strategy may re- ciple solving a single propositional logic formula duce the total time required to find a satisfiable is sufficient to decide on the existence of a coun- formula by skipping over hard instances. Such terexample for any arbitrary finite bound. How- strategies are natural for environments in which ever, one typically starts to solve the formula multiple computing nodes are available in paral- corresponding to bound zero and then solves se- lel, where one may define 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 satisfiable formulas compared to the egy has the nice property that it always finds a largest unsatisfiable ones can also be made for counterexample of minimal length. As with ev- BMC. We attempted to implement opportunis- ery 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- efficient then we would have expected, with per- egy benefits 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 efficiently 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 incremen- mulas. tal solvers are more effective for BMC than non- incremental ones, as that is well known, but to understand when and how opportunistic strate- 2 Motivation gies can be applied. This is done by compar- ing against non-incremental solver run times be- Automated SAT based planning is a problem cause solvers applying opportunistic strategies closely related to BMC. It deals with the same benefit less from the incremental interface of the sequences of parameterized formulas, except solver, as the problem is no longer introduced that the satisfiability 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 plan- ning 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 effort 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 decid- the smallest satisfiable 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 par- tition of the search space defined by the partial out the need for integrating them into one appli- assignment 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 conflict clause learning presented in [18]. These sequences were gener- [17]. Such solvers record a new conflict 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 conflict clause was still satis- in the model checker NuSMV 2.4.3 [6]. fied. The performance of the DPLL-procedure de- pends 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 behav- pendent Decaying Sum (VSIDS) heuristic first ior of SAT-solvers on problem sequences from presented in the solver Chaff [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 conflict clauses. For the figures in this article. For each benchmark each variable an initially zero value called the ac-there are two subfigures, a run time graph la- tivity is maintained. Whenever a conflict clause beled (a) and a variable activity graph labeled (b). In this section we will focus only on the run is learnt the activity of all variables that occur in 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 us- The solver core was not modified but a num- ing the SAT-solver in non-incremental fashion. ber of small modifications2 were made in aux- If the solver found unsatisfiable a solid red bar iliary routines such as the file parser in order is drawn, if the solver found satisfiable 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 stan- will not read the formula sequence from disk but dard sequential strategy and whenever it com- it 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 fly. 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 1 Available from http://www.minisat.se of the non-incremental solver tests from bound 2 Available from http://users.ics.tkk.fi/swiering 0 to k. This demonstrates the time required 80 1600 70 1400 60 1200 hyperactive variables 50 1000 time (s) 40 800 30 600 20 400 10 200 0 0 0 10 20 30 40 50 60 0 10 20 30 40 50 60 bound bound (a) (b) Figure 1: Benchmark irst.dme6 from [3] 60 10000 9000 50 8000 7000 40 hyperactive variables 6000 time (s) 30 5000 4000 20 3000 2000 10 1000 0 0 0 20 40 60 80 100 0 20 40 60 80 100 bound bound (a) (b) Figure 2: Benchmark bc57sensors.p2neg from [3] 100 3500 3000 80 2500 hyperactive variables 60 2000 time (s) 1500 40 1000 20 500 0 0 0 20 40 60 80 100 120 140 0 20 40 60 80 100 120 140 bound bound (a) (b) Figure 3: Benchmark eijk.S1238.S from [3] 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. influencing the range of the y-axis, as it typically The solver can be thought of as having tuned it- grows 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 counterexample for benchmark irst.dme6 is of Another way to look at the result presented in length 53. The run times of the non-incremental Fig. 3(a) is that by using the standard sequen- SAT-solver clearly show the behavior that in- tial strategy we are aiding the solver in proving spired the opportunistic strategies of [15], i.e. the unsatisfiability of the formula corresponding the run time of the non-incremental solver for to the counterexample of length 150, the largest small satisfiable formulas is much smaller than bound tested here. By forcing it through the se- that of the largest unsatisfiable ones. It may quence of formulas we force a direction on the be observed from Fig. 2(a) that for benchmark search that is natural to our problem descrip- bc57sensors.p2neg the run times for the two tion, and apparently this is helpful for the SAT- smallest satisfiable formulas corresponding to solver. For benchmarks with this kind of run bounds 104 and 105 are relatively large. An easy time behavior there is clearly no hope for any satisfiable formula can however be found a little opportunistic strategies. further ahead at bound 106, thus the use of an opportunistic strategy could possibly be benefi- cial. An incremental solver can be started from Note that all results presented in this arti- any arbitrary bound, and it is possible to pro- cle 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 sim- behavior 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 oppor- holds on all execution paths of the model. This tunistic because of the “missing information” it implies that the formulas are unsatisfiable for all causes for the solver, leading it further away from bounds. Here, the crucial role that incremen- the efficiency 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 opportunis- would take about 100 seconds to find that bound tic approaches for satisfiable benchmarks, and 150 alone is unsatisfiable, the incremental solver no chance of any performance improvement for finds this result for all bounds from 0 to 150 se- many unsatisfiable 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 re- property holds for all short execution paths in sources. 5 Parallel SAT solving seems that the interrupted solver is missing more information than just conflict clauses. This was There are two common architectures for parallel one of the reasons to look at the way the activ- SAT-solvers [11]. The first 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 different comput- ing 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 modified 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 efficient as it is able to decide the this activity remains high across several bounds. satisfiability of the formula as soon as the fastest We consider a variable hyperactive if its activity solver finishes. Further diversification may be is within the highest 2% of variables with non- achieved by using different parameters on differ- zero activity. ent computation nodes. Obviously opportunistic The graphs labeled (b) in this article visual- search strategies provide means for diversifica- ize the hyperactive variables. All variables that tion when we are considering solving incremen- are hyperactive for at least one bound are rep- tally 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 define y(v) as the lelized BMC framework Tarmo can be seen as integer on the y-axis corresponding to the vari- 0 a parallelized incremental SAT-solver using the able with index v then for any v > v we have 0 portfolio approach. Each computing node is run- y(v ) > 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 conflict clauses be- variable was hyperactive starting from bound k tween SAT-solvers even if they are working on up to but not including bound k 0 > k then a hor- different 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 k 0 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, k 0 ) on which v is hyperactive was made after observing that interrupting a a line was drawn from (k, y(v)) to (k 0 , y(v)). solver to make it “catch-up” with another breaks One may observe that generally variables with its ability to benefit from incremental SAT to the larger indices become active later. This is be- full extent. As we made this observation in an cause in the solver each newly introduced vari- environment where clause sharing takes place it able is given a larger index than all existing vari- 20 2500 2000 15 hyperactive variables 1500 time (s) 10 1000 5 500 0 0 0 20 40 60 80 100 120 140 0 20 40 60 80 100 120 140 bound bound (a) (b) Figure 4: Benchmark abp4.ptimoneg from [2] 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 pre- ables becomes hyperactive quickly, as the solver sented in this paper for a large set of bench- runs into conflicts on the newly added clauses. marks3 . We observe that on benchmarks with The hyperactive variables in the satisfiable 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 lo- ables 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. flicts regarding variables that represent the state Although we expect all hard satisfiable bench- at 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 unsatisfiable 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 different. For each bound the example of an unsatisfiable benchmark with a solver creates conflict 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 por- line 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 ap- any work has to be performed to find unsatisfi- 3 ability. We say that the activity of variables is Available from http://users.ics.tkk.fi/swiering proach may help to find unsatisfiable 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. 7 Conclusions In this article we have shown a relation between References the run time of the standard sequential strat- [1] Armin Biere, Alessandro Cimatti, Ed- egy for bounded model checking and the activ- mund M. Clarke, and Yunshan Zhu. Sym- ity of decision variables in solvers employing this bolic model checking without BDDs. In strategy. We can use this observation in a SAT- Rance Cleaveland, editor, TACAS, volume solver to predict during the search whether a 1579 of Lecture Notes in Computer Science, more opportunistic strategy could be beneficial pages 193–207. Springer, 1999. for the search. This is especially useful for par- allel solvers in which different threads may be [2] Armin Biere, Keijo Heljanko, Tommi A. executing different strategies. Junttila, Timo Latvala, and Viktor Schup- It is also easy to envision how these techniques pan. Linear encodings of bounded LTL could be useful for model checkers that use a model checking. Logical Methods in Com- combination of truly different model checking puter Science, 2(5), 2006. techniques such as PdTrav [5]. One could eas- ily engineer a system which would do BMC for [3] Armin Biere and Toni Jussila. Hard- some amount of time, after which the variable ware model checking competition 2007 activity could play a role in the decision on how (HWMCC07). Organized as a satellite event to continue. If the variable activity appears to to CAV 2007, Berlin, Germany, July 3-7, be bound local then the property is likely to hold 2007. for the model and thus we may want to start do- ing a complete model checking technique based [4] Max Böhm and Ewald Speckenmeyer. A on for example k-induction [16], Craig interpola- fast parallel SAT-solver - efficient workload tion [13] or BDDs [12] to prove this. balancing. Ann. Math. Artif. Intell., 17(3- 4):381–400, 1996. Another observation we made is that for de- ciding the satisfiability of the last formula in an [5] Gianpiero Cabodi, Paolo Camurati, Luz incrementally encoded sequence of formulas it Garcia, Marco Murciano, Sergio Nocco, can sometimes be faster to solve all formulas in and Stefano Quer. Trading-off SAT search the sequence. This raises the question whether and variable quantifications for effective un- other applications of SAT solving that currently bounded model checking. In Alessandro rely on solving a single SAT formula could ben- Cimatti and Robert B. Jones, editors, FM- efit from the use of incremental problem encod- CAD, pages 1–8. IEEE, 2008. ings. Such encodings allow enforcing a search direction on the SAT-solver that is natural to [6] Alessandro Cimatti, Edmund M. Clarke, the application and therefore possibly beneficial 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. Madi- strand Larsen, editors, CAV, volume 2404 of gan, Ying Zhao, Lintao Zhang, and Sharad Lecture Notes in Computer Science, pages Malik. Chaff: Engineering an efficient SAT 359–364. Springer, 2002. solver. In DAC, pages 530–535. ACM, 2001. [7] Stephen A. Cook. The complexity of [15] Jussi Rintanen, Keijo Heljanko, and Ilkka theorem-proving procedures. In STOC, Niemelä. Planning as satisfiability: parallel pages 151–158. ACM, 1971. plans and algorithms for plan search. Artif. Intell., 170(12-13):1031–1080, 2006. [8] Martin Davis, George Logemann, and Don- [16] Mary Sheeran, Satnam Singh, and Gunnar ald Loveland. A machine program for Stålmarck. Checking safety properties us- theorem-proving. Commun. ACM, 5:394– ing induction and a SAT-solver. In Warren 397, July 1962. A. Hunt Jr. and Steven D. Johnson, editors, [9] Niklas Eén and Niklas Sörensson. An exten- FMCAD, volume 1954 of Lecture Notes in sible SAT-solver. In Enrico Giunchiglia and Computer Science, pages 108–125. Springer, Armando Tacchella, editors, SAT, volume 2000. 2919 of Lecture Notes in Computer Science, [17] João P. Marques Silva and Karem A. pages 502–518. Springer, 2003. Sakallah. GRASP: A search algorithm for [10] Youssef Hamadi, Saı̈d Jabbour, and propositional satisfiability. IEEE Trans. Lakhdar Sais. ManySAT: A parallel SAT Computers, 48(5):506–521, 1999. solver. JSAT, 6(4):245–262, 2009. [18] Siert Wieringa, Matti Niemenmaa, and [11] Antti Eero Johannes Hyvärinen, Tommi A. Keijo Heljanko. Tarmo: A framework for Junttila, and Ilkka Niemelä. Partitioning parallelized bounded model checking. In search spaces of a randomized search. In Lubos Brim and Jaco van de Pol, editors, Roberto Serra and Rita Cucchiara, editors, PDMC, volume 14 of EPTCS, pages 62–76, AI*IA, volume 5883 of Lecture Notes in 2009. Computer Science, pages 243–252. Springer, [19] Hantao Zhang, Maria Paola Bonacina, 2009. and Jieh Hsiang. PSATO: A distributed [12] Kenneth L. McMillan. Symbolic model propositional prover and its application to checking. Kluwer, 1993. quasigroup problems. J. Symb. Comput., 21(4):543–560, 1996. [13] Kenneth L. McMillan. Applications of Craig interpolants in model checking. In Nico- las Halbwachs and Lenore D. Zuck, edi- tors, TACAS, volume 3440 of Lecture Notes