Benchmarking SAT Solvers for Bounded Model Checking

Description

Benchmarking SAT Solvers for Bounded
Model Checking
Emmanuel Zarpas
IBM Haifa Research Laboratory,
[e-mail]
Abstract. Modern SAT solvers are highly dependent on heuristics.
Therefore, benchmarking is of prime importance in evaluating the per-
formances of different solvers. However, relevant benchmarking is not
necessarily straightforward. We present our experiments using the IBM
CNF Benchmark on several SAT solvers. Using the results, we attempt
to define guidelines for a relevant benchmarking methodology, using SAT
solvers for real life BMC applications.
1 Introduction
Over the past decade, formal verification via model checking has evolved from a
theoretical concept to a production-level technique. It is being actively used in
chip design projects across the industry, where formal verification engineers can
now tackle the verification of large industrial hardware designs. Bounded Model
Checking (BMC) [1] has recently enabled the verification of problems that used
to be beyond the reach of formal verification. However, BMC performance relies
heavily on the performance of the underlying SAT solver.
We conducted several experiments using the IBM CNF benchmark [12, 11]
to evaluate SAT tools. Often, we found discrepancies between our results and
the experimental results found in the literature. For example, our results are not
necessarily in line with the results of the SAT03 contest [4]. The main goal of this
paper is to outline a methodology for benchmarking SAT ...

Sujets

• Siège de Nicée
• Centre national de formation et d'études de la protection judiciaire de la jeunesse
• Clauses du contrat de travail en France
• Équipe cycliste BMC Racing
• Accélération (parallélisme)
• Contrôle d'accès à base de règles

Informations

• Publié par: Thean
• Nombre de lectures: 42
• Langue: English

Extrait

BenchmarkingSATSolversforBounded ModelChecking EmmanuelZarpas IBMHaifaResearchLaboratory, azprsai@.lbi.mocm Abstract. ModernSATsolversarehighlydependentonheuristics. Therefore,benchmarkingisofprimeimportanceinevaluatingtheper- formancesofdifferentsolvers.However,relevantbenchmarkingisnot necessarilystraightforward.WepresentourexperimentsusingtheIBM CNFBenchmarkonseveralSATsolvers.Usingtheresults,weattempt todefineguidelinesforarelevantbenchmarkingmethodology,usingSAT solversforreallifeBMCapplications. 1Introduction Overthepastdecade,formalverificationviamodelcheckinghasevolvedfroma theoreticalconcepttoaproduction-leveltechnique.Itisbeingactivelyusedin chipdesignprojectsacrosstheindustry,whereformalverificationengineerscan nowtackletheverificationoflargeindustrialhardwaredesigns.BoundedModel Checking(BMC)[1]hasrecentlyenabledtheverificationofproblemsthatused tobebeyondthereachofformalverification.However,BMCperformancerelies heavilyontheperformanceoftheunderlyingSATsolver. WeconductedseveralexperimentsusingtheIBMCNFbenchmark[12,11] toevaluateSATtools.Often,wefounddiscrepanciesbetweenourresultsand theexperimentalresultsfoundintheliterature.Forexample,ourresultsarenot necessarilyinlinewiththeresultsoftheSAT03contest[4].Themaingoalofthis paperistooutlineamethodologyforbenchmarkingSATsolversonBounded ModelCheckingproblems. Thepaperisorganizedasfollows:InSection2,wepresentexperimental resultsforsomefamousSATsolvers.Section3presentsanewversionofthe IBMBenchmarkanddiscussescorrelationoftheCNFcharacteristicsandsolvers performance.Section4containsadiscussiononSATbenchmarkingforBMC, wherewetrytolearnfromourexperimentalresultsinlightofotherexperiments suchastheSATcontests.Section5concludesthepaper. 2ExperimentswithIBM2002Benchmark:SATSolver Comparison [ O 7] u , r z e C x h p a er ff i I m I e ( n z t C s h c a o ff m 2 p 0 a 0 re 4. d 5. f 1 o 3 u ) r [ f 3 a ], m B o e u r s k S M A i T n5 s 6 o 1 lv [ e 2 r ] s a : n z d Ch Si a e ff ge I( v 2 4 00 [8 1 ] . . 2. W 17 e v u e s r e s d io t n h ) e F.BacchusandT.Walsh(Eds.):SAT2005,LNCS3569,pp.340–354,2005.
cSpringer-VerlagBerlinHeidelberg2005

BenchmarkingSATSolversforBoundedModelChecking341 2002versionoftheIBMCNFBenchmark[12],whoseCNFsaregeneratedthrough BMCfromtheIBMFormalVerificationBenchmarkLibrary[11].Thislibraryisa collectionofmodelsfromreal-lifeindustrialhardwareverificationprojects. Foreachmodel,weusedtheCNFformulas(SATdat.k.cnf)forboundwith k=1,10,15,20,25,30,35,40,45,50.Thetime-outwassetat10,000seconds onaworkstationwith867841XIntel(R)Xeon(TM)CPU2.40GHz,with512KB firstlevelcacheand2.5GBphysicalmemory.Weusedthedefaultconfiguration foreachengine. 2.1zChaffIvs.BerkMin561 WeranzChaffI(2001.2 1 .17version)andBerkMin561onthe2002versionofthe IBMCNFBenchmark.Table1isasummaryoftheresultsobtained.More Table1. Theresultsaredisplayedinsecondsandincludethetimeout10,000seconds zChaffBerkMin561 Totaltime(10000sectime-out)344765414094 First(#ofCNFwheretheengineisthefastest)298131 #ofunsolvedproblems(timeoutreached)2530 +(#ofCNFwheretheengineisthefastest bymorethanaminuteand20%)6732 Firstbymodel(#ofmodelwheretheengineisthefastest)2818 completeexperimentalresultsarepresentedinTable8,whereforeachmodelin thetable,wepresentthesumoftheresultsofSATdat.k.cnfwithk=1,10,15, 20,25,30,35,40,45,50(i.e.,theBMCtranslationofeachmodelforthedifferent k).Formoredetails,seethecompleteresultsin[13].BecauseSATsolversdo notalwaysbehaveinhomogeneousmanner(Cf.detailedresultsin[13]ortable 2),thecompleteresultsanalysisshouldnotbedisregarded. TheresultsshowthatzChaffandBerkMin561achievedcloseresults.On someCNFs,zChaffrunsfaster,andonothers,BerkMin561runsfaster.Inmost cases,thedifferencesintheirperformanceisnotverysignificant,thehighest speedisnotfasterbymorethanoneminuteor20%.However,whilezChaff seemstoperformslightlybetteroverall,BerkMin561getsbetterresultsthan zChaffontheUNSATCNFs.Fromtheseresults,itisnotpossibletoconclude thatBerkMin561performsbetterthanzChaff.Thisisnotconsistentwithwhat canbereadintheliteratureorwiththefinalresultsoftheSAT03contest(Cf. section2.4). Thisisnotaverysatisfyingconclusionandthepreviousmetricsdonottell usinasimplewayhowmuchfasterzChaffisthanBerkmin561 2 .Weneedsome 1 2 BerkMin561wassecondintheSAT03contestindustrialbenchmarkscategoryinthe SAT03contest;thewinnerForkliftisnotpubliclyavailable. Itisveryimportanttobeabletogiveclearandconcisevaluesforresultsdissemi- nation.

342E.Zarpas Table2. TheresultsaredisplayedinsecondsfortheCNFsfrom18rulemodel.The time-outwassetto10000seconds.zChaffperformstheworstfork=15,20,35;Berk- Min561performstheworstfork=30,40,50;Siegev4hasthebestperformance,except fork=15,25 18ruleCNFResultzChaffBerkMinSiege SATdat.k1.cnfunsat000 SATdat.k10.cnfunsat110 SATdat.k15.cnfunsat1345 SATdat.k20.cnfunsat654741 SATdat.k25.cnfunsat951109251 SATdat.k30.cnfsat700755557 SATdat.k35.cnfsattime-out22301730 SATdat.k40.cnfsat55108060247 SATdat.k45.cnfsattime-outtime-out959 SATdat.k50.cnfsat5010time-out1370 additionalmetricsinordertocomparetheseSATsolvers.Thearithmeticmean ofthespeedupseemsirrelevant.Let’ssaywewanttocomparetheperformances ofsolversAandB.IfthespeedupofAvs.Bis10ontest1and0.0001on test2,thearithmeticmeanofthespeedup(Avs.B)wouldbe5andthemean ofthespeedup(Bvs.A)wouldbe5000.Thisisclearlynotrelevant.Theglobal speedup(TotaltimeA/TotalTimeB)isgoodtohavebutthe“longruns” havefarmoreweightthantheshortones.Themedianismuchmoreinteresting. howeveritdoesnottakeintoaccounttheextremevalues(e.g,ifontest1the speedupisequaltomedian+10ortomedian+0.1,itdoesnotchangethe medianvalue).Ontheotherhand,themedianinsensivitytoextremevalues makesitlessdependentonthetime-outs.Thegeometricalmeanseemstobe agoodsolution.Itdefinitelytakesintoaccounttheweightofthe“negative speedup”(i.e.,aspeedupoflessthan1) 3 . Wefeltthesevaluesshouldbecomputedthesevaluesonlyonarelevant subsetofthebenchmark.Forexample,wediscardedallthecaseswherethe fourSATsolverstime-out.Inaddition,wediscardedcasesforwhichthefour solvers(zChaffI,Berkmin561,Siegev4,zChaffII)runinlessthanfiveseconds. Therationalisthatitisdifficulttoaccuratelycompareverysmallruntimesand thattheseverysmallruntimesarearguablynotrelevant.Theresultsdisplayed inTable3(b)showthatBerkmin561isnearlytwotimesslowerthanzChaffI, butthatBerkminbehavessomehowbetterinthe“long”cases. 2.2Siegev4 Siegewashors-concoursfortheSAT03contest,thereforeitdidnotparticipate inthesecondstage.Nevertheless,theSiegeresultswereprettygoodforthe 3 Notethatthelogarithmofthegeometricalmeanisequaltothearithmeticalmean ofthelogarithms.

BenchmarkingSATSolversforBoundedModelChecking343 Table3. Witha10000sec.time-out TotalTime#time-outs (inseconds) zChaffI344,76425 berkmin561414,03530 Siegev419723914 zChaffII389,30431 (a) Speedup z B C er h k a m ff in IzC Si h e a g f e fI z z C C h h a a f f f f I I I g m e e o d m ia e n an0 0 . . 4 55 1 2 2 . . 9 8 0 7 1 1 . . 2 2 3 9 global0.753.580.75 (b) firststageandSiegehasareputationforbeingoneofthebestSATsolvers available.WeranSiegev4[8]onthebenchmarkusing123456789asaseed.Table 3displaystheoverallconclusions.FormoredetailsseeTable8and[13].Siegev4 isthefastestin298cases(CNFs)outof498.Inmanydifficultcases,Siegev4 isfastestbyanorderofmagnitude,ormore.Insomecases,Siegev4performed significantlyworsethanzChafforBerkMin561.Forexample,for26rule,Siegev4 isslowerthanzChaffbyanorderofmagnitudeandslowerthanBerkMinbytwo ordersofmagnitude.Inaddition,withinthetime-out,severalCNFscanbesolved onlybySiegev4 4 .Inconclusion,weseethatSiegev4performssignificantly better(roughlyspeaking2.5timesfaster)thanzChaffI,Berkmin561andzChaff IIontheIBMCNF2002benchmark. 2.3zChaffII TheindustrialcategoryoftheSAT04competition[6]waswonbyzChaffII (zChaff2004.5.13).However“black-box”solverssuchasForklift(the2003edi- tionwinner)were“hors-concours”andassuchnotallowedtoenterthesecond stageofthecompetition.WefocushereontheperformanceofzChaffIIvs zChaffI.zChaffIIisfasterthan:zChafffor229CNFs(outof442),Berkmin561 for208CNFs(outof442),Siegev4for82CNFs(outof442).Inaddition,zChaff IIreachedtime-outmoreoftenthanzChaffI(forsixmorecases).Table3dis- playsasyntheticviewoftheresults.ThezChaffIIcodewasleftunchanged,so itusedrandomseeds.Siegev4isroughlythreetimefasterthanzChaffI.Figure 1givesusagraphicviewoftheperformanceofzChaffIIvs.zChaffI.Theover- allperformancedifferencebetweenzChaffIandzChaffIIonourbenchmarkis small 5 ,eventhoughthetwosolverscanbehaveverydifferentlyinspecificcases. 4 5 Siegeisarandomizedsolver,therefore,itcouldbearguedthatthecomparisonis notfairsincethezChaffandBerkMin561,versionsweusedwerenotrandomized. Nevertheless,evenadeterministicsolvercanbeluckyandprovidingSiegewitha seedofSiegemakesitdeterministic. ItshouldbenotethatzChaffIIisrandomized,sotheresultscouldbedifferentfor otherruns.Itwouldbeinterestingtohaveastatisticaldescriptionoftherangeof zChaffIIperformances.

344E.Zarpas 00001 0001 001 01 1 0.1110100100010000 1.0 10.0 zchaff I runtime 08 07 06 05 04 03 02 10 0 niB (a)(b) Fig.1. Histogram(b)givesthedistributionofthedecimallogarithmof zChaffI/zChaffIIspeedupwith10000sectime-out 2.4ComparisonwithSATContestResults Inordertounderstandwhetherornotourresultsareconsistentwiththoseof theSAT03contest 6 (fordetailsresultssee[5]),wehadalookattheresultsof thefirstandsecondstagesofthecompetition. Firststage.Lookingattheresults 7 fortheindustrialcategory[5],wenotethe following: –Series13rule 8 isover-represented(Cf.Table4).Besides,sinceallsolvers time-outonmostoftheCNFsfromthisseries,itisnotverymeaningful. –Exceptforseries13ruleand11rule,theseriesfromtheIBMCNFbench- markareeasyforzChaff,BerkMin561,andSiegev1. –Resultsforrule07arenotconsistentwithourownexperiences.Thisdis- crepancyisprobablycausedbythe“Lisasyndrome”[4]:CNFswereshuffled forSAT03andsolverperformancecandifferdramaticallybetweenashuffled CNFandtheoriginal. TheSAT03contestresultsforBerkMin561,Forklift,Siegev1,andzChaffon (shuffled)seriesfromtheIBMCNFBenchmarkaresummarizedinTable4.If resultsfromseries07ruleand13rulearediscarded,zChaffshowsbetterresults thanBerkMin561. 6 7 8 InthefirststageoftheSAT04competition,zChaffIandzChaffIIhaveveryclose resultsandthesolversthatoutperformedthem(Forklift,Oepir)arenotavailable forexperimentation. TheSiegeversionusedfortheSAT03contestisSiegev1. ThenamesoftheSAT03seriesappearsinitalicsinordertodifferentiatethemfrom theseriesweusedinourexperiments.FortheexactcompositionoftheSAT03series, see[5].

BenchmarkingSATSolversforBoundedModelChecking345 Table4. PartialresultsfromfirststageSAT03contest BerkMin561forkliftSiege1zChaff Total#ofSolvedBenchmarks112112112101 TotalCPUtimeneeded(sec)105000103000103000114000 without13rule(sec)15105184084160 without13ruleand07rule(sec)1410424268553 WebelievethatthedifferencesinresultsforthefirststageofSAT03contest resultsforIBMthebenchmarkandourexperimentsareduetoclauseshuffling inSAT03andtothefactthattheSAT03experimentusedasmallertest-bedof CNFsfromtheIBMbenchmark. Secondstage.Duringthesecondstageofthecompetition,solverswereranked accordingtothenumberofCNFstheycouldsolvefromarestrictedbenchmark. Forkliftwasrankedfirst,Berkmin561second,andzChaffIsixthontheindustrial benchmark 9 . Clearly,therespectivezChaffIandBerkMin561rankingdonotcorrespondto ourexperimentalresults(seeTable3).However,inthesecondstage,allsolvers “timed-out”ontheIBMbenchmarksselected.Inotherwords,therankingof thesolversselectedforthesecondstageofthecompetitiondidnottakeinto accountperformanceontheIBMbenchmarks.Thisprobablyexplainswhyour evaluationofzChaffandBerkMin561ontheIBMCNFBenchmarkgivesresults thatarenotinlinewiththesecondstageresults(onindustrialbenchmarks)of theSAT03contest. 3ExperimentswithIBM2004Benchmark:Searchfor Correlation 3.1DescriptionoftheIBM2004Benchmark BoundedModelCheckingtranslationtechnologyiscontinuouslyevolving.There- fore,were-generatedtheIBMCNFBenchmarkfromtheIBMModelBenchmark usinganalternativeBMCtool.Weranthenewtranslationforthefollowing boundsk=0..10,k=11..15,k=16..20,k=21..25,...,k=95..100.The2004 CNFsareavailableon-line.Inthispaper,werefertothe2002and2004versions astheoldandthenewbenchmarks,respectively. Table5and6presentstatisticaldescriptionsoftheoldandthenewbench- marks.Inthesetwotables,averageisthearithmeticalmean,STDEVisthe standarddeviation, cla v u a s r es istheratiobetweenthenumberofclausesandthe numberofvariables,%unitisthepercentofunit(i.e.,oflengthone)clausesina CNF,%binisthepercentofclausesoflengthtwo,%teristhepercentofclauses 9 Siegewashors-concours,thereforenotselectedforthesecondstage.

436E.Zarpas Table5. Old(2002)benchmark varclauses cla v u ar ses %unit%bin%ter%l=4% l> 4 average80,167343,8264.120.375.514.23.56.5 median54,857220,1804.080.277.012.23.56.6 STDEV81,924388,1560.520.36.47.71.01.3 max636,0893,172,1075.421.684.555.35.29.1 min3,64514,6812.48040.84.30.10.1 Table6. New(2004)Benchmark varclauses cla v u ar ses %unit%bin%ter%l=4% l> 4 average73,414305,3013.990.674.515.03.66.3 median50,897195,6123.980.476.113.13.66.6 STDEV75,553349,2480.450.66.17.30.91.2 max565,8892,760,5025.484.684.551.64.99.1 min3,60614,1042.55046.54.40.10.1 oflengththree,%l=4isthepercentofclausesoflength4and%l>4isthe percentofclauseslongerthan4. ThesetwotablestellusthatthenewbenchmarkCNFsareroughly10% smallerthantheoldbenchmarkCNFs.However,theyencompassroughlythe sameproportionoflengthtwo,three,andfourclauses.Thehigherproportion ofunitclausesinthenewbenchmarkisduetospecificoptimizations.Wealso seethattheratio cla v u ar ses isslightlylowerinthenewbenchmark(seethenext subsectionforadiscussionontherelevanceofthisratio).Figure2displaysthe histogramof%bin,wheretwomodels(07and131)havea“nonstandard” percentofbinaryclausesandareinthe45%-55%andnotinthe70%-85%. WelookedatsomestatisticsforthestructureoftheCNFsofthenewbench- mark.Wefoundthatforanymodelofthebenchmark,therearefourrealnum- bersa,b,c,dsuchthatforalltheCNFsofthemodel,#(variables) ≈ ak+b and#(clauses) ≈ ck+d,withkbeingtheboundusedtogeneratetheCNFs. Inamoregeneralway,foranymodelandforanyintegernstrictlygreaterthan 0,therearetworealnumberseandfsuchthatforallCNFsofthemodel #(clausesoflengthn) ≈ ek+f(ofcourseeandfcanbenull,forexamplein mostmodels,thenumberofunitclausesisaconstant).Thecorrelations(for adiscussionaboutstatistictechniquesforNP-completeproblemssee[10])be- tweentheseriesfromthebenchmarkandtheseriespredictedwiththeprevious equationsareabout0.99.ThisisnotsurprisingsincetheCNFsaregenerated fromthemodelinawayessentiallylineartothebound.Inaddition,wefound outthat,inourbenchmark,thelengthofthelongestclauseisthesameforall CNFsgeneratedfromthesamemodel.Figure2(b)displaysthehistogramof thelongestclausesinthenewbenchmark.Notethattwomodels,07and131, whichhavethegreaterlongestclauses,arealsotheoneswitha“nonstandard” percentofbinaryclauses.