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

362 L.MichelandP.Van

Hentenryck

Fig.4.ThesuccessivewavesofLDS.

Inourcontext,theheuristicalwaysselectstheleftdisjunctinanybranch-ingdecision.Hence,wave0simplyfollowsacomputationpathoftheform left,...,left .Wave1explores,explicitlyorimplicitly,allthesolutionswithonediscrepancycomparedtotheheuristic,thatis,allsolutionswhosecompu-tationpathscontainoneoccurrenceofright.Moregenerally,waveiexplores,explicitlyorimplicitly,allthesolutionswhosecomputationpathscontainioc-currencesofright.Forinstance,forauniformsearchtreeofdepth3,LDSwouldexplorethefollowingwaves:

Wave0:{ left,left,left }.

Wave1:{ left,left,right , left,right,left , right,left,left }.

Wave2:{ left,right,right , right,left,right , right,right,left }.

Wave3:{ right,right,right }.

Figure4illustratesthesewavesgraphically.Byexploringthesearchtreeac-cordingtotheheuristic,LDSmayreachgoodsolutions(andthusanoptimalso-lution)muchfasterthandepth- rstandbest- rstsearchforsomeapplications.Itsstrengthisitsabilitytoexplorediversepartsofthesearchtreecontaininggoodsolutionswhichareonlyreachedmuchlaterbydepth- rstsearch.Thisabilityofjumpingtodifferentregionsofthesearchtreeisalsowhatmakesitsimplementationmorechallenging.

4.ANITERATIVEIMPLEMENTATION

IterativeLDSisasimpleimplementationofLDSobtainedbyslightlygener-alizingDFS.Thekeyideaistoexplorethesearchtreeinwavesandtorelaxtherequirementofwaveiwhichisnowallowedtoexploresolutionswithatmostidiscrepancies(insteadofexactlyidiscrepancies).Figure5depictstheimplementationofiterativeLDS.FunctionILDSSATISFYexpectsagoalgandaconstraintstoreσandreturnsSATISFIABLE(σ).ItsimplementationisaloopthatcallsfunctionILDSEXPLOREwithanincreasingnumberofalloweddiscrepancies,startingat0andstoppingwhentheupperboundonthenumberofdiscrepan-ciesMaxDiscrepanciesisreached.2FunctionILDSEXPLOREexpectsagoalg,aconstraintstoreσ,andanumberdofalloweddiscrepancies.Itreturnstrueiffthereexistsasolutionofσthatcanbereachedbyginatmostddiscrepancies.ItsimplementationcloselyresemblesDFSSATISFY.Themaindifferencesarethe2Observethatitisnotdif culttomodifyILDSSATISFYandILDSMINtoremovethisupperbound.Itsuf cestodetermineduringawaveifsometransitionstepswouldhavebeenallowed,hadmorediscrepanciesbeengiven.

ACMTransactionsonComputationalLogic,Vol.5,No.2,April2004.