1 Preface SAT COMPETITION 2007- SOLVER DESCRIPTION Scaling and Probabilistic Smoothing (SAP

The first part of this paper is essentially a reprint of the solver description from the 2005 competition, as the software submitted this year is identical to the 2005 software. We entered the SAPS variant implemented in the UBCSAT software package [7], th

SATCOMPETITION2007-

SOLVERDESCRIPTION

ScalingandProbabilisticSmoothing(SAPS)

DaveA.D.Tompkins,FrankHutter,andHolgerH.Hoos

ComputerScienceDepartmentUniversityofBritishColumbia{davet,hutter,hoos}@cs.ubc.ca

1Preface

The rstpartofthispaperisessentiallyareprintofthesolverdescriptionfromthe2005competi-tion,asthesoftwaresubmittedthisyearisidenti-caltothe2005software.WeenteredtheSAPSvariantimplementedintheUBCSATsoftwarepack-age[7],thesourcecodeforwhichisfreelyavailableatdoc.xuehai.net.

Theonlydifferenceto2005isthatwesubmittwoversionsofSAPS,onewiththeoriginaldefaultparameters[4],andonewithanewsetoftunedpa-rameters.Theseparametershavebeenfoundusinganautomaticapproachbasedonlocalsearchinpa-rameterspace[3].Section3givesabriefoverviewofthistuningapproachandshowsverypromisingperformanceoftheautomaticallytunedparameters.

procedureSAPS(F,α,ρ,wp,Psmooth,SAPSthresh)

input:

propositionalformulaF,scalingfactorα,

smoothingfactorρ,randomwalkprobabilitywp,smoothingprobabilityPsmooth,SAPSthresholdSAPSthreshoutput:

variableassignmentAfori:=1..|A|doa(i):=RandSelect({ ,⊥})forj:=1..|CLP|doclp(j):=1while(Fisunsatis edunderA)docurScore:=Eval(F,A,CLP)bestScore:=∞BestVars:=

foreachis.t.variableiappearsinanunsatis edclausedoscore:=Eval(F,Flip(A,i),CLP)ifscore<bestScorethen

bestScore:=scoreBestVars:={i}

elseifscore=bestScorethen

BestVars:=BestVars∪{i}endifendfor

if(bestScore curScore)<SAPSthreshthenk:=RandSelect(BestVars)A:=Flip(A,k)else

withprobabilitywpdo

k:=RandSelect({1..|A|})A:=Flip(A,k)otherwise

foreachjs.t.clausejisunsatis edunderAdoclp(j):=clp(j)×αendfor

withprobabilityPsmoothdoforj:=1..|CLP|do

clp(j):=clp(j)+(1 ρ)×endforendwithendwithendifendwhilereturn(A)

endprocedureSAPS

2SAPSandVariants

TheSAPSalgorithmisaDynamicLocalSearch(DLS)algorithmconceptuallycloselyrelatedtotheExponentiatedSub-Gradient(ESG)algorithmde-velopedbySchuurmans,SoutheyandHolte[5].WhenintroducingSAPS,ourmajorcontributionswereareductioninthealgorithmiccomplexityascomparedtotheESGalgorithmandanewperspec-tiveonhowthetwoalgorithmswerebehaving.TheSAPSalgorithmisdescribedindetailinourpa-per[4]andFigure1containsapseudo-coderepre-sentationthataccuratelyre ectshowtheSAPSal-gorithmhasbeenimplementedinpractice.

SimilartomostDLSalgorithms,SAPSassignsaclausepenaltyclptoeachclause,andthesearchevaluationfunctionofSAPSisthesumoftheclausepenaltiesofunsatis edclauses.Thecoresearchprocedureisagreedydescentwithoutsidewayssteps.Wheneveralocalminimumoccurs(nostepimprovementintheevaluationfunctiongreaterthanSAPSthreshispossible)arandomwalkstepoc-curswithprobabilitywp.Otherwise,ascalingstepoccurs,wherethepenaltiesforunsatis edclausesaremultipliedbythescalingfactorα(i.e.clp′:=

Figure1:TheSAPSalgorithm.Foreachclausejin

Fthereisaclausepenaltyclp(j)inCLP,andisthemeanofallclausepenalties.Eval(F,A,CLP)isthesumofallclp(j)whereclausejisunsatis edinFbyA.Inpractice,Eval(...)valuesarecachedandupdatedaftereach ip.Flip(A,i)returnsthevariableassignmentAwithvariablei ipped.

α·clp).Afterascalingstep,asmoothingstepoccurswithprobabilityPsmooth.Inasmoothing

第1页下一页