An Experimental Evaluation of Ground Decision Procedures
14 Pages
English
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

An Experimental Evaluation of Ground Decision Procedures

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer
14 Pages
English

Description

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 differences, 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 differing characteristics.
Based on these experimental results, we discuss relative strengths and
shortcomings of different systems.
1 Introduction
Decision procedures are an enabling technology for a growing number of appli-
cations of automated deduction in hardware and software verification, 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.Sinceallvariablesareconsideredtobeuniversallyquantified,
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 ...

Subjects

Informations

Published by
Reads 64
Language English

Exrait

AnExperimentalEvaluationofGroundDecisionProcedures?(SubmittedforPublication,January25,2003)LeonardodeMouraandHaraldRueßSRIInternationalComputerScienceLaboratory333RavenswoodAvenueMenloPark,CA94025,USA{demoura,ruess}@csl.sri.comphone+1650859-6136,fax+1650859-2844Abstract.Thereisalargevarietyofalgorithmsforgrounddecisionprocedures,buttheirdifferences,inparticularintermsofexperimen-talperformance,arenotwellstudied.Wedevelopmapsofthebehaviorofgrounddecisionproceduresbycomparingtheperformanceofava-rietyoftechnologiesonbenchmarksuiteswithdifferingcharacteristics.Basedontheseexperimentalresults,wediscussrelativestrengthsandshortcomingsofdifferentsystems.1IntroductionDecisionproceduresareanenablingtechnologyforagrowingnumberofappli-cationsofautomateddeductioninhardwareandsoftwareverification,planning,boundedmodelchecking,andothersearchproblems.Insolvingtheseproblems,decisionproceduresareusedtodecidethevalidityofpropositionalconstraintssuchasz=f(xy)x=z+y→−y=(xf(f(z))).Thisformulaisinthecombinationoflineararithmeticandanuninterpretedfunctionsymbolf.Sinceallvariablesareconsideredtobeuniversallyquantified,theycanbetreatedas(Skolem)constants,andhencewesaythattheformulaisground.Solvingpropositionalformulaswiththousandsofvariablesandhundredsofthousandsofliterals,asrequiredbymanyapplications,isachallengingproblem.Overthelastcoupleofyears,manydifferentalgorithms,heuristics,andtoolshavebeendevelopedinaddressingthischallenge.Mostoftheseapproacheseitheruseextensionsofbinarydecisiondiagrams[1],oranequisatisfiablereductionofpropositionalconstraintformulastopropositionallogic,whichissolvedusing?FundedbySRIInternational,byNSFGrantsCCR-0082560,EIA-0224465,andCCR-0326540,DARPA/AFRL-WPAFBContractF33615-01-C-1908,andNASAContractB0906005.
2aDavis-Putnam[2]searchprocedure.Theirdifferences,especiallyintermsofexperimentalperformance,arenotwellstudied.Ultimately,itisourgoaltodevelopcomprehensivemapsofthebehaviorofgrounddecisionproceduresbycomparingtheperformanceofavarietyoftech-nologiesonbenchmarksuiteswithdifferingcharacteristics,andthestudyinthispaperisanessentialfirststeptowardsthisgoalofcomprehensivebench-markmarking.WehavebeencollectinganumberofexistingbenchmarksforgrounddecisionproceduresandappliedthemtotheCVC/CVCLite[3],ICS[4],UCLID[5],MathSAT[6],Simplify[7],andSVC[8]systems.Thisrequireddevel-opingtranslatorsfromthevariousbenchmarkformatstotheinputlanguagesofthesystemsunderconsideration.Forthediversityofthealgorithmsunderlyinggrounddecisionprocedures,weonlymeasureruntimes.Weanalyzethecompu-tationalcharacteristicsofeachsystemoneachofthebenchmarks,andexposespecificstrengthsandweaknessesofthesystemsunderconsideration.Sincesuchanendeavorshouldultimatelydevelopintoacooperativeongoingactivityacrossthefield,ourmainemphasisinconductingtheseexperimentsisnotonlyonreproducibilitybutalsoonreusabilityandextendibilityofourex-perimentalsetup.Inparticular,allbenchmarksandalltranslatorswedevelopedforconvertinginputformats,andallexperimentalresultsarepubliclyavailableathttp://www.csl.sri.com/users/demoura/gdb-benchmarks.html.Thispaperisstructuredasfollows.InSection2weincludeabriefoverviewonthelandscapeofdifferentmethodsforgrounddecisionprocedures,andinSection3wedescribethedecisionprocedures,benchmarks,andourexperimentalsetup.Section4containsourexperimentalresultsbypairwisecomparingthebehaviorofdecisionproceduresoneachbenchmarkset,andinSection5and6wesummarizesomegeneralobservationsfromtheseexperimentsandprovidefinalconclusions.2GroundDecisionProceduresWeconsidergrounddecisionprocedures(GDP)fordecidingpropositionalsat-isfiabilityforformulaswithliteralsdrawnfromagivenconstrainttheoryT.GDPsareusuallyobtainedasextensionsofdecisionproceduresforthesatisfi-abilityproblemofconjunctionsofconstraintsinT.Forexample,satisfiabilityforaconjunctionofequationsanddisequationsovertermsinUisdecidableinO(nlog(n))usingcongruenceclosure[9].Conjunctionsofconstraintsinrationallineararithmeticaresolvableinpolynomialtime,althoughmanyalgorithmssuchasSimplexhaveexponentialworst-casebehavior.InthetheoryDofdifferencelogic,arithmeticconstraintsarerestrictedtoconstraintsoftheformxycwithcaconstant.AnO(n3)algorithmfortheconjunctionofsuchconstraintsisobtainedbysearching,usingtheBellman-Fordalgorithm,fornegative-weightcyclesinthegraphwithvariablesasnodesandanedgeofweightcfromxtoyforeachsuchconstraints.ForindividualtheoriesTiwithdecidablesatisfiabilityproblems,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.3GivenaprocedurefordecidingsatisfiabilityofconjunctionsofconstraintsinTitisstraightforwardtodecidepropositionalcombinationsofconstraintsinTbytransformingtheformulaintodisjunctivenormalform,butthisisoftenpro-hibitivelyexpensive.Betteralternativesaretoextendbinarydecisiondiagramstoincludeconstraintsinsteadofvariables(e.g.differencedecisiondiagrams),ortoreducethepropositionalconstraintproblemtoapurelypropositionalproblembyencodingthesemanticsofconstraintsintermsofaddedpropositionalcon-straints(see,forexample,Theorem1in[13]).Algorithmsbasedonthislatterapproacharecharacterizedbytheeagernessorlazinesswithwhichconstraintsareadded.IneagerapproachestoconstructingaGDPfromadecisionprocedureforT,propositionalconstraintsformulasaretransformedintoequisatisfiableproposi-tionalformulas.Inthisway,Ackermann[14]obtainsaGDPforthetheoryUbyaddingallpossibleinstancesofthecongruenceaxiomandrenamingunin-terpretedsubtermswithfreshvariables.Intheworstcase,thenumberofsuchaxiomsisproportionaltothesquareofthelengthofthegivenformula.Otherthe-oriessuchasS-expressionsorarrayscanbeencodedusingthereductionsgivenbyNelsonandOppen[10].VariationsofAckermann’strickhavebeenused,forexample,byShostak[15]forarithmeticreasoninginthepresenceofuninter-pretedfunctionsymbols,andvariousreductionsofthesatisfiabilityproblemofBooleanformulasoverthetheoryofequalitywithuninterpretedfunctionsym-bolstopropositionalSATproblemshaverecentlybeendescribed[16],[17],[18].Inasimilarvein,aneagerreductiontopropositionallogicworksforconstraintsindifferencelogic[19].Incontrast,lazyapproachesintroducepartofthesemanticsofconstraintsondemand[13],[20],[6],[21].Letφbetheformulawhosesatisfiabilityisbeingchecked,andletLbeaninjectivemapfromfreshpropositionalvariablestotheatomicsubformulasofφsuchthatL1[φ]isapropositionalformula.WecanuseapropositionalSATsolvertocheckthatL1[φ]issatisfiable,buttheresultingtruthassignment,sayl1...ln,mightbespurious,thatisL[l1...ln]mightnotbeground-satisfiable.Ifthatisthecase,wecanrepeatthesearchwiththeaddedlemmaclause(¬l1...∨¬ln)andinvoketheSATsolveron(¬l1...∨¬ln)L1[φ].Thisensuresthatthenextsatisfyingassignmentreturnedisdifferentfromthepreviousassignmentthatwasfoundtobeground-unsatisfiable.Insuchanofflineintegration,aSATsolverandaconstraintsolvercanbeusedasblackboxes.Incontrast,inanonlineintegrationthesearchforsatisfying
4(a)Math-SATsuite(c)SALsuite(b)UCLIDsuite(d)SEPsuiteFig.1.Numberofboolean(darkgray)andnon-boolean(lightgray)variablesineachproblem.assignmentsoftheSATsolverissynchronizedwithconstructingacorrespondinglogicalcontextofthetheory-specificconstraintsolver.Inthisway,inconsistenciesdetectedbytheconstraintsolvermaytriggerbacktrackinginthesearchforsatisfyingpropositionalassignments.Aneffectiveonlineintegrationcannotbeobtainedwithablack-boxdecisionproceduresbutrequirestheconstraintsolvertoprocessconstraintsincrementallyandtobebacktrackableinthatnotonlytheacurrentlogicalcontextismaintainedbutalsocontextscorrespondingtobacktrackingpointsinthesearchforsatisfyingassignments.Thebasicrefinementloopinthelazyintegrationisusuallyacceleratedbyconsideringnegationsofminimalinconsistentsetsofconstraintsor“good”over-approximationsthereof.Theseso-calledexplanationsareeitherobtainedfromanexplicitlygeneratedproofobjectorbytrackingdependenciesoffactsgeneratedduringconstraintsolverruns.3ExperimentalSetupWedescribethesetupofourexperimentsincludingtheparticipatingsystems,thebenchmarksandtheirmaincharacteristics,andtheorganizationoftheex-perimentsitself.Thissetuphasbeenchosenbeforeconductinganyexperiments.3.1Systems.ThesystemsparticipatinginthisstudyimplementawiderangeofdifferentsatisfiabilitytechniquesasdescribedinSection2.AlltheseGDPsarefreelyavailableanddistributed,andineachcasewehavebeenusingthelatestversion(asofJanuary10,2004).Weprovideshortdescriptionsinalphabeticalorder.
5TheCooperatingValidityChecker(CVC1.0a)[3]isaGDPforthecombinationoftheoriesincludinglinearrealarithmeticA,uninterpretedfunctionsymbolsU,functionalarrays,andinductivedatatypes.Propositionalreasoningisobtainedbymeansofalazy,onlineintegrationofthezChaffSATsolverandaconstraintsolverbasedonaShostak-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)isaGDPforthecombinationofdifferencelogicandun-interpretedfunctionsymbols.ItusesaneagertransformationtoSATproblems,whicharesolvedusingzChaff[5].Theuseofothertheoriessuchaslambdaex-pressionsandarraysisrestrictedinordertoeliminatetheminpreprocessingsteps.Math-SAT[6]isaGDPforlineararithmeticbasedonablack-boxconstraintsolver,whichisusedtodetectinconsistenciesinconstraintscorrespondingtopartialBooleanassignmentsinanofflinemanner.TheconstraintengineusesaBellman-FordalgorithmfordifferencelogicconstraintsandaSimplexalgorithmformoregeneralconstraints.Simplify[7]isaGDPforlineararithmeticA,uninterpretedfunctionsU,andarraysbasedontheNelson-Oppencombination.Simplifyuseshome-grownSATsolvingtechniques,whichdonotincorporatemanyefficiencyimprovementsfoundinmodernSATsolvers.However,Simplifygoesbeyondtheothersystemsconsideredhereinthatitincludesheuristicextensionsforquantifierreasoning,butthisfeatureisnottestedhere.StanfordValidityChecker(SVC1.1)[8]decidespropositionalformulaswithun-interpretedfunctionsymbolsU,rationallineararithmeticA,arrays,andbitvec-tors.ThecombinationofconstraintsisdecidedusingaShostak-likecombinationextendedwithbinarydecisiondiagrams.3.2BenchmarksuitesWehaveincludedintothisstudyfreelydistributedbenchmarksuitesforGDPswithconstraintsinAandUandcombinationsthereof.Theseproblemsrange
6fromstandardtimedautomataexamplestoequivalencecheckingformicropro-cessorsandthestudyoffault-tolerantalgorithms.Forthetimebeingwedonotseparatesatisfiableandunsatisfiableinstances.Sincesomeofthebenchmarksaredistributedinclausalandotherinnon-clausalform,itisdifficulttoprovidemeasuresonthedifficultyoftheseproblems,butFigure1containsthenum-berofvariablesforeachbenchmarkproblem.Thedarkgraybarsrepresentsthenumberofbooleanandthelightgraybarsthenumberofnon-booleanvariables.TheMath-SATbenchmarksuite(http://dit.unitn.it/~rseba/Mathsat.html)iscomposedoftimedautomataverificationproblems.Theproblemsaredistributedonlyinclausalnormalformandarithmeticisrestrictedtocoefficientsin{−1,0,1}.Thisbenchmarkformatalsoincludesextra-logicalsearchhintsfortheMath-SATsystem.Thissuitecomprises280problems,159ofwhichareinthedifferencelogicfragment.ThesizeoftheASCIIrepresentationoftheseproblemsrangesfrom4Kbto26Mb.AscanbeseeninFigure1(a)mostofthevariablesareboolean.1BenchmarksuiteSatUnsatUnsolvedMath-Sat3722419UCLID0362SAL2116729SEP980Table2.Classification.TheUCLIDbenchmarksuite(http://www-2.cs.cmu.edu/~uclid)isderivedfromprocessorandcachecoherenceprotocolverifications.Thissuiteisdis-tributedintheSVCinputformat.Inparticular,propositionalstructuresarenon-clausalandconstraintsincludeuninterpretedfunctionsUanddifferenceconstraintsD.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,110ofwhichareinthedifferencelogicfragment,thesizeoftheASCIIrepresentationoftheseproblemsrangesfrom1Kbto300Kb.Mostofthebooleanvariablesareusedtoencodecontrolflow(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,andconstraintsindifferencelogic.Thissuiteincludesonly17problems,thesizeoftheASCIIrepresentationoftheseproblemsrangesfrom1.5Kbto450Kb.Wedevelopedvarioustranslatorsfromtheinputformatusedineachbench-marksuitetotheinputformatacceptedbyeachGDPdescribedontheprevioussection,butMath-SAT.WedidnotimplementatranslatortotheMath-SATformatbecauseitonlyacceptsformulasintheCNFformat,andatranslationtoCNFwoulddestroythestructuralinformationcontainedintheoriginalfor-mulas.Inaddition,nospecificsareprovidedforgeneratinghintsforMath-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,wewereabletosetaside4machineswithidenticalconfigurationforourexperiments,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.1andconfiguredinoptimizedmode.Table1containsthecommandlineoptionsusedtoexecuteeachGDP.34ExperimentalResultsTable2showsthenumberofsatisfiableandunsatisfiableproblems4foreachbenchmark,andaproblemhasbeenclassified“Unsolved”whennoneoftheGDPscouldsolveitwithinthetimeandmemoryrequirements.ThescattergraphsinFigures2and3includetheresultsofrunningCVC,ICS,UCLID,MathSAT,andSVContheMath-SATbenchmarks,Figure4containstheruntimesofCVC,ICS,SVC,UCLIDontheUCLIDbenchmarks,andFigure5)reportsonourresultsofrunningCVC,ICS,SVC,andUCLIDontheSALbenchmarks3In[20]thedepthfirstsearchheuristic(option-dfs)isreportedtoproducethebestoverallresultsforCVC,butwedidnotuseitbecausethisflagcausesCVCtoproducemanyincorrectresults.4Forvaliditycheckers,satisfiableandunsatisfiableshouldbereadasinvalidandvalidinstancesrespectively.
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.TheplotscomparingUCLIDcontainonlytheproblemsinthedifferencelogicfragmentsupportedbyUCLID.TheresultsshowthattheoverallperformanceofICSisbetterthanthoseofUCLID,CVCandSVConmostproblemsofthissuite.WiththeexceptionofMath-SAT(whichwasappliedonlytoitsownbench-markset),everyothersystemfailedonatleastseveralproblems—mainlyduetoexhaustionofthememorylimit.Also,theMath-SATproblemsprovedtobeanon-trivialtestonparsersasSVC’sparsercrashedonseveralbiggerproblems
11(seeTable1).TheperformanceofSVCisaffectedbythesizeoftheproblemsandtheCNFformatused(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.sPDGInsufficientconstraintpropagationinlazyintegrations.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