Search strategies, that is, strategies that describe how to explore search trees, have raised much interest for constraint satisfaction in recent years. In particular, limited discrepancy search and its variations have been shown to achieve significant imp

364 L.MichelandP.VanHentenryck

conditiond>=0whichtestswhethersuf cientlymanydiscrepanciesareleftandtherecursivecallfortherightdisjunctwhichdecrementsthenumberofalloweddiscrepancies.Figure5alsopresentsthefunctionILDSMINwhichisasimilargeneralizationofDFSMINfortheminimizationproblem.

ThecorrectnessofILDSSATISFYfollowsdirectlyfromthefactthatitslastcalltoILDSEXPLORE,thatis,

ILDSEXPLORE(g,σ,MaxDiscrepancies)

isequivalenttoILDSSATISFY(g,σ).ThecorrectnessofILDSMINfollowsasimilarargument.ThelastcalltoILDSMINIMIZEimplicitlyexploresthesamesearchtreeasDFSMINIMIZE.Ofcourse,itislikelythatonlyasmallportionofthattreeisactuallyexplored,sincef issupposedtobeoptimalornear-optimalatthatcomputationstage.

Besidesthesimplicityofitsimplementation,iterativeLDShastwomainben-e ts.Ontheonehand,iterativeLDSinheritsthememoryef ciencyofDFS.Ontheotherhand,iterativeLDSisveryrobust.Sinceitslastiterationmim-icksDFS,thebranchingfunctionmaybedynamicorrandomized.Minimizationdoesnotraiseanydif cultyeitherandthesearchprocedurecanbeeasilyen-hancedtoaccommodatenogoodsandglobalcuts.Observehoweverthat,whenthebranchingfunctionisdynamicorrandomized,waveidoesnotnecessarilyexplorethecon gurationsencounteredinwavei 1.Thisdoesnotaffectcor-rectnessofcourse,sincethelastiterationexplores,implicitlyorexplicitly,thewholesearchspace.

ThemaininconvenienceofiterativeLDSis,ofcourse,itsexecutiontime.Byrelaxingtherequirementsonthewaves,iterativeLDSmayexploreseveraltimesthesamesearchregions.Korf[1996]proposedacleverimplementationofLDStoavoidexploringthesameregionswhenthemaximumdepthisknown.However,thenewimplementationisnotrobustwithrespecttorandomization,dynamicsearchprocedureswithglobalcuts,sincethereisnoguaranteethatthesamechoiceswillbemade.Wenowstudyimplementationsaimingataddressingthislimitation.

5.ARECOMPUTATIONIMPLEMENTATION

WenowpresentRLDS,animplementationofLDSbasedonrecomputation.RLDScanbeseenasaninstantiationofthegenericsearchstrategyinPerron

[1999].Thepresentationinthissectionisasigni cantre nementofthesearchstrategyalgorithmpresentedinVanHentenrycketal.[2000]inordertomakebacktrackingandrecomputationasexplicitaspossibleand,moregenerally,tohighlightalltheissuesinvolvedinarecomputationimplementation.

RLDSorganizesthesearcharoundanactivecon gurationandaqueueofcon gurations.Theactivecon gurationrepresentsthecon gurationthatRLDScurrentlyexplores,whilethequeuerepresentscon gurationstobeex-ploredsubsequently.Thecon gurationsinthequeuearenotstoredexplicitlybutarerepresentedbytheircomputationpaths.Eachtimeabranchingoccursontheactivecon guration,RLDSpushestherightdisjunctontothequeueandtheleftdisjunctbecomestheactivecon guration.WhenevertheactiveACMTransactionsonComputationalLogic,Vol.5,No.2,April2004.