=Paper=
{{Paper
|id=None
|storemode=property
|title=On Incremental Satisfiability and Bounded Model Checking
|pdfUrl=https://ceur-ws.org/Vol-832/paper_4.pdf
|volume=Vol-832
|dblpUrl=https://dblp.org/rec/conf/fmcad/Wieringa11
}}
==On Incremental Satisfiability and Bounded Model Checking==
https://ceur-ws.org/Vol-832/paper_4.pdf
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