An Experimental Evaluation of Ground Decision Procedures

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

Publié par

Omme

Nombre de lectures

Langue

English

An Experimental Evaluation of
?Ground Decision Procedures
(Submitted for Publication, January 25, 2003)
Leonardo de Moura and Harald Rueß
SRI International
Computer Science Laboratory
333 Ravenswood Avenue
Menlo Park, CA 94025, USA
{demoura, ruess}@csl.sri.com
phone +1 650 859-6136, fax +1 650 859-2844
Abstract. There is a large variety of algorithms for ground decision
procedures, but their diﬀerences, in particular in terms of experimen-
tal performance, are not well studied. We develop maps of the behavior
of ground decision procedures by comparing the performance of a va-
riety of technologies on benchmark suites with diﬀering characteristics.
Based on these experimental results, we discuss relative strengths and
shortcomings of diﬀerent systems.
1 Introduction
Decision procedures are an enabling technology for a growing number of appli-
cations of automated deduction in hardware and software veriﬁcation, planning,
bounded model checking, and other search problems. In solving these problems,
decision procedures are used to decide the validity of propositional constraints
such as
z = f(x−y)∧x= z+y→−y =−(x−f(f(z))) .
This formula is in the combination of linear arithmetic and an uninterpreted
functionsymbol f.Sinceallvariablesareconsideredtobeuniversallyquantiﬁed,
they can be treated as (Skolem) constants, and hence we say that the formula
is ground.
Solving propositional formulas with thousands of variables and hundreds of
thousandsofliterals ...

Voir

Publié par

Omme

Nombre de lectures

Langue

English

AnExperimentalEvaluationofGroundDecisionProcedures?(SubmittedforPublication,January25,2003)LeonardodeMouraandHaraldRueßSRIInternationalComputerScienceLaboratory333RavenswoodAvenueMenloPark,CA94025,USA{demoura,ruess}@csl.sri.comphone+1650859-6136,fax+1650859-2844Abstract.Thereisalargevarietyofalgorithmsforgrounddecisionprocedures,buttheirdiﬀerences,inparticularintermsofexperimen-talperformance,arenotwellstudied.Wedevelopmapsofthebehaviorofgrounddecisionproceduresbycomparingtheperformanceofava-rietyoftechnologiesonbenchmarksuiteswithdiﬀeringcharacteristics.Basedontheseexperimentalresults,wediscussrelativestrengthsandshortcomingsofdiﬀerentsystems.1IntroductionDecisionproceduresareanenablingtechnologyforagrowingnumberofappli-cationsofautomateddeductioninhardwareandsoftwareveriﬁcation,planning,boundedmodelchecking,andothersearchproblems.Insolvingtheseproblems,decisionproceduresareusedtodecidethevalidityofpropositionalconstraintssuchasz=f(x−y)∧x=z+y→−y=−(x−f(f(z))).Thisformulaisinthecombinationoflineararithmeticandanuninterpretedfunctionsymbolf.Sinceallvariablesareconsideredtobeuniversallyquantiﬁed,theycanbetreatedas(Skolem)constants,andhencewesaythattheformulaisground.Solvingpropositionalformulaswiththousandsofvariablesandhundredsofthousandsofliterals,asrequiredbymanyapplications,isachallengingproblem.Overthelastcoupleofyears,manydiﬀerentalgorithms,heuristics,andtoolshavebeendevelopedinaddressingthischallenge.Mostoftheseapproacheseitheruseextensionsofbinarydecisiondiagrams[1],oranequisatisﬁablereductionofpropositionalconstraintformulastopropositionallogic,whichissolvedusing?FundedbySRIInternational,byNSFGrantsCCR-0082560,EIA-0224465,andCCR-0326540,DARPA/AFRL-WPAFBContractF33615-01-C-1908,andNASAContractB0906005.

2aDavis-Putnam[2]searchprocedure.Theirdiﬀerences,especiallyintermsofexperimentalperformance,arenotwellstudied.Ultimately,itisourgoaltodevelopcomprehensivemapsofthebehaviorofgrounddecisionproceduresbycomparingtheperformanceofavarietyoftech-nologiesonbenchmarksuiteswithdiﬀeringcharacteristics,andthestudyinthispaperisanessentialﬁrststeptowardsthisgoalofcomprehensivebench-markmarking.WehavebeencollectinganumberofexistingbenchmarksforgrounddecisionproceduresandappliedthemtotheCVC/CVCLite[3],ICS[4],UCLID[5],MathSAT[6],Simplify[7],andSVC[8]systems.Thisrequireddevel-opingtranslatorsfromthevariousbenchmarkformatstotheinputlanguagesofthesystemsunderconsideration.Forthediversityofthealgorithmsunderlyinggrounddecisionprocedures,weonlymeasureruntimes.Weanalyzethecompu-tationalcharacteristicsofeachsystemoneachofthebenchmarks,andexposespeciﬁcstrengthsandweaknessesofthesystemsunderconsideration.Sincesuchanendeavorshouldultimatelydevelopintoacooperativeongoingactivityacrosstheﬁeld,ourmainemphasisinconductingtheseexperimentsisnotonlyonreproducibilitybutalsoonreusabilityandextendibilityofourex-perimentalsetup.Inparticular,allbenchmarksandalltranslatorswedevelopedforconvertinginputformats,andallexperimentalresultsarepubliclyavailableathttp://www.csl.sri.com/users/demoura/gdb-benchmarks.html.Thispaperisstructuredasfollows.InSection2weincludeabriefoverviewonthelandscapeofdiﬀerentmethodsforgrounddecisionprocedures,andinSection3wedescribethedecisionprocedures,benchmarks,andourexperimentalsetup.Section4containsourexperimentalresultsbypairwisecomparingthebehaviorofdecisionproceduresoneachbenchmarkset,andinSection5and6wesummarizesomegeneralobservationsfromtheseexperimentsandprovideﬁnalconclusions.2GroundDecisionProceduresWeconsidergrounddecisionprocedures(GDP)fordecidingpropositionalsat-isﬁabilityforformulaswithliteralsdrawnfromagivenconstrainttheoryT.GDPsareusuallyobtainedasextensionsofdecisionproceduresforthesatisﬁ-abilityproblemofconjunctionsofconstraintsinT.Forexample,satisﬁabilityforaconjunctionofequationsanddisequationsovertermsinUisdecidableinO(nlog(n))usingcongruenceclosure[9].Conjunctionsofconstraintsinrationallineararithmeticaresolvableinpolynomialtime,althoughmanyalgorithmssuchasSimplexhaveexponentialworst-casebehavior.InthetheoryDofdiﬀerencelogic,arithmeticconstraintsarerestrictedtoconstraintsoftheformx−y≤cwithcaconstant.AnO(n3)algorithmfortheconjunctionofsuchconstraintsisobtainedbysearching,usingtheBellman-Fordalgorithm,fornegative-weightcyclesinthegraphwithvariablesasnodesandanedgeofweightcfromxtoyforeachsuchconstraints.ForindividualtheoriesTiwithdecidablesatisﬁabilityproblems,theunionofallTi’sisoftendecidedusingaNelson-Oppen[10]oraShostak-like[11,12]combinationalgorithm.

ICSulimit-s30000;icsproblem-name.icsUCLIDuclidproblem-name.uclsat0zchaffCVCcvc+sat<problem-name.cvcCVCLitecvcl+satfast<problem-name.cvcSVCsvcproblem-name.svcSimplifySimplifyproblem-name.smpMath-SATmathsatlinuxproblem-name.ms-bjmath-heuristicSatzHeurTable1.CommandlineoptionsusedtoexecuteGDPs.3GivenaprocedurefordecidingsatisﬁabilityofconjunctionsofconstraintsinTitisstraightforwardtodecidepropositionalcombinationsofconstraintsinTbytransformingtheformulaintodisjunctivenormalform,butthisisoftenpro-hibitivelyexpensive.Betteralternativesaretoextendbinarydecisiondiagramstoincludeconstraintsinsteadofvariables(e.g.diﬀerencedecisiondiagrams),ortoreducethepropositionalconstraintproblemtoapurelypropositionalproblembyencodingthesemanticsofconstraintsintermsofaddedpropositionalcon-straints(see,forexample,Theorem1in[13]).Algorithmsbasedonthislatterapproacharecharacterizedbytheeagernessorlazinesswithwhichconstraintsareadded.IneagerapproachestoconstructingaGDPfromadecisionprocedureforT,propositionalconstraintsformulasaretransformedintoequisatisﬁableproposi-tionalformulas.Inthisway,Ackermann[14]obtainsaGDPforthetheoryUbyaddingallpossibleinstancesofthecongruenceaxiomandrenamingunin-terpretedsubtermswithfreshvariables.Intheworstcase,thenumberofsuchaxiomsisproportionaltothesquareofthelengthofthegivenformula.Otherthe-oriessuchasS-expressionsorarrayscanbeencodedusingthereductionsgivenbyNelsonandOppen[10].VariationsofAckermann’strickhavebeenused,forexample,byShostak[15]forarithmeticreasoninginthepresenceofuninter-pretedfunctionsymbols,andvariousreductionsofthesatisﬁabilityproblemofBooleanformulasoverthetheoryofequalitywithuninterpretedfunctionsym-bolstopropositionalSATproblemshaverecentlybeendescribed[16],[17],[18].Inasimilarvein,aneagerreductiontopropositionallogicworksforconstraintsindiﬀerencelogic[19].Incontrast,lazyapproachesintroducepartofthesemanticsofconstraintsondemand[13],[20],[6],[21].Letφbetheformulawhosesatisﬁabilityisbeingchecked,andletLbeaninjectivemapfromfreshpropositionalvariablestotheatomicsubformulasofφsuchthatL−1[φ]isapropositionalformula.WecanuseapropositionalSATsolvertocheckthatL−1[φ]issatisﬁable,buttheresultingtruthassignment,sayl1∧...∧ln,mightbespurious,thatisL[l1∧...∧ln]mightnotbeground-satisﬁable.Ifthatisthecase,wecanrepeatthesearchwiththeaddedlemmaclause(¬l1∨...∨¬ln)andinvoketheSATsolveron(¬l1∨...∨¬ln)∧L−1[φ].Thisensuresthatthenextsatisfyingassignmentreturnedisdiﬀerentfromthepreviousassignmentthatwasfoundtobeground-unsatisﬁable.Insuchanoﬄineintegration,aSATsolverandaconstraintsolvercanbeusedasblackboxes.Incontrast,inanonlineintegrationthesearchforsatisfying

4(a)Math-SATsuite(c)SALsuite(b)UCLIDsuite(d)SEPsuiteFig.1.Numberofboolean(darkgray)andnon-boolean(lightgray)variablesineachproblem.assignmentsoftheSATsolverissynchronizedwithconstructingacorrespondinglogicalcontextofthetheory-speciﬁcconstraintsolver.Inthisway,inconsistenciesdetectedbytheconstraintsolvermaytriggerbacktrackinginthesearchforsatisfyingpropositionalassignments.Aneﬀectiveonlineintegrationcannotbeobtainedwithablack-boxdecisionproceduresbutrequirestheconstraintsolvertoprocessconstraintsincrementallyandtobebacktrackableinthatnotonlytheacurrentlogicalcontextismaintainedbutalsocontextscorrespondingtobacktrackingpointsinthesearchforsatisfyingassignments.Thebasicreﬁnementloopinthelazyintegrationisusuallyacceleratedbyconsideringnegationsofminimalinconsistentsetsofconstraintsor“good”over-approximationsthereof.Theseso-calledexplanationsareeitherobtainedfromanexplicitlygeneratedproofobjectorbytrackingdependenciesoffactsgeneratedduringconstraintsolverruns.3ExperimentalSetupWedescribethesetupofourexperimentsincludingtheparticipatingsystems,thebenchmarksandtheirmaincharacteristics,andtheorganizationoftheex-perimentsitself.Thissetuphasbeenchosenbeforeconductinganyexperiments.3.1Systems.ThesystemsparticipatinginthisstudyimplementawiderangeofdiﬀerentsatisﬁabilitytechniquesasdescribedinSection2.AlltheseGDPsarefreelyavailableanddistributed,andineachcasewehavebeenusingthelatestversion(asofJanuary10,2004).Weprovideshortdescriptionsinalphabeticalorder.

5TheCooperatingValidityChecker(CVC1.0a)[3]isaGDPforthecombinationoftheoriesincludinglinearrealarithmeticA,uninterpretedfunctionsymbolsU,functionalarrays,andinductivedatatypes.Propositionalreasoningisobtainedbymeansofalazy,onlineintegrationofthezChaﬀSATsolverandaconstraintsolverbasedonaShostak-like[11]combination,andexplanationsareobtainedasaxiomsofprooftrees.WealsoconsiderthesuccessorsystemCVCLite(version1.0.1),whosearchitectureissimilartotheoneofCVC,butitusesahome-grownSATsolverforrealizinigatighterintegrationbetweenSATandconstraintsolving.TheIntegratedCanonizerandSolver(ICS2.0)[4]isaGDPforthecombinationoftheoriesincludinglinearrealarithmeticA,uninterpretedfunctionsymbolsU,functionalarrays,S-expressions,productsandcoproducts,andbitvectors.Itrealizesalazy,onlineintegrationofanon-clausalSATsolverwithanincre-mental,backtrackableconstraintenginebasedonaShostak[11]combination.Explanationsaregeneratedandmaintainedusingasimpletrackingmechanism.UCLID(version1.0)isaGDPforthecombinationofdiﬀerencelogicandun-interpretedfunctionsymbols.ItusesaneagertransformationtoSATproblems,whicharesolvedusingzChaﬀ[5].Theuseofothertheoriessuchaslambdaex-pressionsandarraysisrestrictedinordertoeliminatetheminpreprocessingsteps.Math-SAT[6]isaGDPforlineararithmeticbasedonablack-boxconstraintsolver,whichisusedtodetectinconsistenciesinconstraintscorrespondingtopartialBooleanassignmentsinanoﬄinemanner.TheconstraintengineusesaBellman-FordalgorithmfordiﬀerencelogicconstraintsandaSimplexalgorithmformoregeneralconstraints.Simplify[7]isaGDPforlineararithmeticA,uninterpretedfunctionsU,andarraysbasedontheNelson-Oppencombination.Simplifyuseshome-grownSATsolvingtechniques,whichdonotincorporatemanyeﬃciencyimprovementsfoundinmodernSATsolvers.However,Simplifygoesbeyondtheothersystemsconsideredhereinthatitincludesheuristicextensionsforquantiﬁerreasoning,butthisfeatureisnottestedhere.StanfordValidityChecker(SVC1.1)[8]decidespropositionalformulaswithun-interpretedfunctionsymbolsU,rationallineararithmeticA,arrays,andbitvec-tors.ThecombinationofconstraintsisdecidedusingaShostak-likecombinationextendedwithbinarydecisiondiagrams.3.2BenchmarksuitesWehaveincludedintothisstudyfreelydistributedbenchmarksuitesforGDPswithconstraintsinAandUandcombinationsthereof.Theseproblemsrange

6fromstandardtimedautomataexamplestoequivalencecheckingformicropro-cessorsandthestudyoffault-tolerantalgorithms.Forthetimebeingwedonotseparatesatisﬁableandunsatisﬁableinstances.Sincesomeofthebenchmarksaredistributedinclausalandotherinnon-clausalform,itisdiﬃculttoprovidemeasuresonthediﬃcultyoftheseproblems,butFigure1containsthenum-berofvariablesforeachbenchmarkproblem.Thedarkgraybarsrepresentsthenumberofbooleanandthelightgraybarsthenumberofnon-booleanvariables.TheMath-SATbenchmarksuite(http://dit.unitn.it/~rseba/Mathsat.html)iscomposedoftimedautomataveriﬁcationproblems.Theproblemsaredistributedonlyinclausalnormalformandarithmeticisrestrictedtocoeﬃcientsin{−1,0,1}.Thisbenchmarkformatalsoincludesextra-logicalsearchhintsfortheMath-SATsystem.Thissuitecomprises280problems,159ofwhichareinthediﬀerencelogicfragment.ThesizeoftheASCIIrepresentationoftheseproblemsrangesfrom4Kbto26Mb.AscanbeseeninFigure1(a)mostofthevariablesareboolean.1BenchmarksuiteSatUnsatUnsolvedMath-Sat3722419UCLID0362SAL2116729SEP980Table2.Classiﬁcation.TheUCLIDbenchmarksuite(http://www-2.cs.cmu.edu/~uclid)isderivedfromprocessorandcachecoherenceprotocolveriﬁcations.Thissuiteisdis-tributedintheSVCinputformat.Inparticular,propositionalstructuresarenon-clausalandconstraintsincludeuninterpretedfunctionsUanddiﬀerenceconstraintsD.Altogetherthereare38problems,thesizeoftheASCIIrepre-sentationrangesfrom4Kbto450Kb,andthemajorityoftheliteralsarenon-boolean(Figure1(b)).TheSALbenchmarksuite(http://www.csl.sri.com/users/demoura/gdb-benchmarks.html)isderivedfromboundedmodelcheckingoftimedau-tomataandlinearhybridsystems,andfromtest-casegenerationforembeddedcontrollers.Theproblemsarerepresentedinnon-clausalform,andconstraintsareinfulllineararithmetic.Thissuitecontains217problems,110ofwhichareinthediﬀerencelogicfragment,thesizeoftheASCIIrepresentationoftheseproblemsrangesfrom1Kbto300Kb.Mostofthebooleanvariablesareusedtoencodecontrolﬂow(Figure1(c)).1WesuspectthatmanybooleanvariableshavebeenintroducedthroughconversiontoCNF.

ICSUCLIDCVCCVCLiteSVCSimplifyMath-SATMath-SATtimeout03019509152suiteaborts222158613900UCLIDtimeout4209524n/asuiteaborts4014900n/aSALtimeout13611158799n/asuiteaborts29464744n/aSEPtimeout000110n/asuiteaborts011100n/aTable3.Numberoftimeoutsandabortsforeachsystem.(a)(d)(b)(e)(c)(f)Fig.2.Runtimes(inseconds)onMath-SATbenchmarks.7TheSEPbenchmarksuite(http://iew3.technion.ac.il/~ofers/smtlib-local/index.html)isderivedfromsymbolicsimulationofhard-waredesigns,timedautomatasystems,andschedulingproblems.Theproblemsarerepresentedinnon-clausalform,andconstraintsindiﬀerencelogic.Thissuiteincludesonly17problems,thesizeoftheASCIIrepresentationoftheseproblemsrangesfrom1.5Kbto450Kb.Wedevelopedvarioustranslatorsfromtheinputformatusedineachbench-marksuitetotheinputformatacceptedbyeachGDPdescribedontheprevioussection,butMath-SAT.WedidnotimplementatranslatortotheMath-SATformatbecauseitonlyacceptsformulasintheCNFformat,andatranslationtoCNFwoulddestroythestructuralinformationcontainedintheoriginalfor-mulas.Inaddition,nospeciﬁcsareprovidedforgeneratinghintsforMath-SAT.Indevelopingthesetranslators,wehavebeencarefultopreservethestructuralinformation,andweusedalltheinformationavailabletouseavailablelanguage

8(a)(c)(b)(d)Fig.3.Runtimes(inseconds)ontheMath-SATbenchmarks(cont.)featuresusefulfortheunderlyingsearchmechanisms.2TheMath-SATsearchhints,however,areignoredinthetranslation,sincethisextra-logicalinforma-tionismeaninglessforalltheothertools.3.3SetupAllexperimentswereperformedonmachineswith1GHzPentiumIIIprocessor256Kbofcacheand512MbofRAM,runningRedHatLinux7.3.Althoughthesemachinesarenowoutdated,wewereabletosetaside4machineswithidenticalconﬁgurationforourexperiments,therebyavoidingerror-proneadjustmentofperformancenumbers.WeconsideredaninstanceofaGDPtotimeoutifittookmorethan3600secs.EachGDPwasconstrainedto450MbofRAMforthedataarea,and40MbofRAMforthestackarea.WesayaGDPabortswhenitrunsoutofmemoryorcrashesforotherreasons.Withthesetimingandmemoryconstraintsrunningallbenchmarkssuitesrequiresmorethan30CPUdays.ForthediversityoftheinputlanguagesandthealgorithmsunderlyingtheGDPs,wedonotincludeanymachine-independentandimplementation-independentmeasures.Instead,werestrictourselvestoreportingtheusertimeofeachprocessasreportedbyUnix.Inthisway,wearemeasuringonlythesystemsasimplemented,andobservationsfromtheseexperimentsabouttheunderlyingalgorithmscanonlybemaderatherindirectly.2Wehavealsobeencontemplatingamaliciousapproachforproducingworst-possibletranslations,butdecidedagainstitinsuchanearlystageofbenchmarking.

(a)(d)(b)(e)(c)(f)Fig.4.Runtimes(inseconds)ontheUCLIDbenchmarks.9WiththenotableexceptionofCVCLite,allGDPsunderconsiderationwereobtainedinbinaryformatfromtheirrespectivewebsites.TheCVCLitebi-narywasobtainedusingg++3.2.1andconﬁguredinoptimizedmode.Table1containsthecommandlineoptionsusedtoexecuteeachGDP.34ExperimentalResultsTable2showsthenumberofsatisﬁableandunsatisﬁableproblems4foreachbenchmark,andaproblemhasbeenclassiﬁed“Unsolved”whennoneoftheGDPscouldsolveitwithinthetimeandmemoryrequirements.Thescattergraphsin–Figures2and3includetheresultsofrunningCVC,ICS,UCLID,MathSAT,andSVContheMath-SATbenchmarks,–Figure4containstheruntimesofCVC,ICS,SVC,UCLIDontheUCLIDbenchmarks,and–Figure5)reportsonourresultsofrunningCVC,ICS,SVC,andUCLIDontheSALbenchmarks3In[20]thedepthﬁrstsearchheuristic(option-dfs)isreportedtoproducethebestoverallresultsforCVC,butwedidnotuseitbecausethisﬂagcausesCVCtoproducemanyincorrectresults.4Forvaliditycheckers,satisﬁableandunsatisﬁableshouldbereadasinvalidandvalidinstancesrespectively.

10(a)(d)(b)(e)(c)(f)Fig.5.Runtimes(inseconds)ontheSALbenchmarks.usingtheexperimentalsetupasdescribedinSection3.Pointsabove(below)thediagonalcorrespondtoexampleswherethesystemonthex(y)axisisfasterthantheother;pointsonedivisionaboveareanorderofmagnitudefaster;ascatterthatisshallower(steeper)thanthediagonalindicatestheperformanceofthesystemonthex(y)axisdeterioratesrelativetotheotherasproblemsizeincreases;pointsontheright(top)edgeindicatethex(y)axissystemtimedoutoraborted.MultiplicitiesofdotsfortimeoutsandabortsareresolvedinTable3.Forlackofspace,theplotsforSimplifyandCVCLitearenotincludedhere.SimplifyperformedpoorlyinallbenchmarksexceptSEP,anddoesnotseemtobecompetitivewithnewerGDPimplementations.InthecaseofCVCLite,itspredecessorsystemCVCdemonstratedover-allsuperiorbehavior.Also,theSEPsuitedidnotprovetodistinguishwellbetweenvarioussystems,asallbutoneproblemcouldbesolvedbyallsystemsinafractionofasecond.Alltheseomittedplotsareavailableathttp://www.csl.sri.com/users/demoura/gdb-benchmarks.html.Figures2and3compareICS,UCLID,CVC,SVCandMath-SATontheMath-SATsuite.TheplotscomparingUCLIDcontainonlytheproblemsinthediﬀerencelogicfragmentsupportedbyUCLID.TheresultsshowthattheoverallperformanceofICSisbetterthanthoseofUCLID,CVCandSVConmostproblemsofthissuite.WiththeexceptionofMath-SAT(whichwasappliedonlytoitsownbench-markset),everyothersystemfailedonatleastseveralproblems—mainlyduetoexhaustionofthememorylimit.Also,theMath-SATproblemsprovedtobeanon-trivialtestonparsersasSVC’sparsercrashedonseveralbiggerproblems

11(seeTable1).TheperformanceofSVCisaﬀectedbythesizeoftheproblemsandtheCNFformatused(Figure3(d))onthissuite,sinceitssearchheuris-ticsareheavilydependentonthepropositionalstructureoftheformula.Ontheotherhand,theperformanceofthenon-clausalSATsolverofICSisnotquiteasheavilyimpactedbythisspecialformat.Infact,ICSistheonlyGDPwhichsolvesallproblemssolvedbyMath-SAT(Figure2(d)),anditalsosolvedsev-eralproblemsnotsolvedbyMath-SAT,eventhoughsearchhintswereusedbyMath-SAT.UCLIDperformsbetterthanCVCandSVConmostofthebiggerproblems(Figures2(e)and2(f)).Figure4comparesICS,UCLID,CVC,andSVContheUCLIDbenchmarks.WhatissurprisinghereisthatSVCiscompetitivewithUCLIDonUCLID’sownbenchmarks(Figure4(e)).Also,theoverallperformanceofSVCissuperiortoitspredecessorCVCsystem(Figure4(f)).ICSdoesnotperformparticularlywellonthisbenchmarksetinthatitexhauststhegivenmemorylimitformanyofthelargerexamples.Figure5comparesICS,UCLID,CVC,andSVContheSALbenchmarks.ICSperformsbetterthanUCLIDonallexamples(Figure5(a)),anditsoverallperformanceisbetterthanCVC(Figure5(b)).ICS,UCLIDandCVCfailonseveralproblemsduelackofmemory.AlthoughtheoverallperformanceofCVCseemsbetterthanUCLID,thelattermanagedtosolveseveralproblemswhereCVCfailed(Figure5(d)).5ObservationsandResearchQuestionsAshasbeenmentionedinSection3,theresultsproducedinourexperimentsmeasuremainlyimplementationsofGDPs.Nevertheless,wetrytoformulatesomemoregeneralobservationsaboutalgorithmicstrengthsandweaknessesfromtheseexperiments,whichshouldbehelpfulinstudyingandimproving.sPDGInsuﬃcientconstraintpropagationinlazyintegrations.TheeagerUCLIDsystemusuallyoutperformslazysystemssuchasICS,CVC,andMath-SATonproblemswhichrequireextensiveconstraintpropagation.Thisseemstobeduetothefactthattheunderlyinglazyintegrationalgorithmsonlypropagateinconsistenciesdetectedbytheconstraintsolver,buttheydonotpropagateconstraintsimpliedbythecurrentlogicalcontext.Supposeahypotheticalproblemwhichcontainstheatoms{x=y,y=z,x=z},andduringthesearchtheatomsx=yandy=zareassignedtotrue,thentheatomx=zcouldbeassignedtotruebyconstraintpropagation(transitivity),butnoneoftheexistinglazyproverspropagatesthisinference.Incontrast,thesekindsofpropagationsareperformedineagerintegrations,sincetheunit-clauseruleofDavis-PutnamlikeSATsolversassumesthejobofpropagatingconstraints.Arithmeticalconstraintsintheeagerapproach.Onarithmetic-intensiveprob-lems,UCLIDusuallyperformsworsethanotherGDPswithdedicatedarithmetic

Voir