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

DecompositionforSearchStrategies 359

PROPOSITION2.5(BRANCHINGPROPERTY).LetgbecompleteforσandletBRANCH(g,σ)= (gl,cl),(gr,cr) .Thengl(respectively,gr)iscompleteforσ∧cl(respectively,σ∧cr).

PROOF.Byspeci cationofBRANCH,wehaveσ≡(σ∧cl)∨(σ∧cr)andhenceSOL(σ)=SOL(σ∧cl)∪SOL(σ∧cr).Sincecl∧crisinconsistent,SOL(σ∧cl)∩SOL(σ∧cr)= .SinceSOL(g,σ)iscomplete,wehaveSOL(g,σ∧cl)=SOL(σ∧cl)andSOL(g,σ∧cr)=SOL(σ∧cr)andtheresultfollows.

PROPOSITION2.6(RESTARTINGPROPERTY).Letgbedownward-completeforσandlet g,σ → g1,σ1 →··· → gn,σn beasequenceoftransitionsteps.Then,SOL(gn,σn)=SOL(g,σn).

PROOF.Byde nitionofthetransitionsteps,σn σ.Sincegisdownward-completeforσ,thenSOL(g,σn)=SOL(σn).Theresultfollowsfromthecomplete-nessofgnforσn.

2.5Depth-FirstSearch

Figure2showshowtoimplementadepth- rststrategytodetectsatis abilityofaconstraintstore.FunctionDFSSATISFYexpectsagoalgandaconstraintstoreσandreturnsSATISFIABLE(σ).Itsimplementationcheckswhetherσisasolutionorcanbeshowninconsistent,inwhichcasesitreturnstheappropriateresult.Otherwise,itappliesthebranchingfunctiontoobtain(gl,cl)and(gr,cr).DFSSATISFYaddsconstraintcltothestoreσandperformsarecursivecallwithglandthenewstore.Iftherecursivecallsucceeds,thenDFSSATISFYreturnssuccessfully.Otherwise,itbacktrackstoremoveclfromtheconstraintstoreandexplorestherightbranch.ObservethatDFSSATISFYmaintainsasinglecon-straintstorewhichiscriticalinobtaininggoodmemoryperformanceonlargeap-plications.ThecorrectnessofDFSSATISFYfollowsdirectlyfromProposition2.5.Figure2alsoshowshowtoimplementthetraditionaldepth- rstbranchandboundstrategyofconstraintprogramming[VanHentenryck1989]tominimizeanobjectivefunctionfsubjecttoaconstraintstoreσ.FunctionDFSMINex-pectsagoalg,aconstraintstoreσ,andanobjectivefunctionf.ItreturnsDFSMIN(f,σ).TheimplementationofDFSMIN rstdeclaresanintegerf thatmaintainsthevalueofthebestsolutionfoundsofarandinitializesitto∞.ItthencallsprocedureDFSMINIMIZE(g,σ,f,f ).DFSMINIMIZEupdatesf ifσisasolution.Otherwise,ifσisnotafailure,itappliesthebranchingfunctionandexplorebothdisjunctsrecursively.ObservethattheTELLoperation

TELL(σ,cl∧f<f )

dynamicallyaddsnotonlyclbutalsotheconstraintf<f .Thisoptimizationconstraintrestrictsthesearchtothesolutionsofσ,whichimprovesthevalueofthecurrentbestsolution(whichisdynamicallyadjusted).Asimilarobservationisvalidfortherightdisjunctaswell.

2.6ComputationPaths

Acomputationpathrepresentsthesequenceofbranchingdecisionsfromtherootofthesearchtreetoagivennodeor,moreprecisely,fromaninitial

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