A Decomposition-Based Implementation of Search Strategies(8)

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

358 L.MichelandP.VanHentenryck

¬SUCCESS(σ)∧¬FAILURE(σ)BRANCH(g,σ)= (gl,cl),(gr,cr) ;

rrexpressthatacon guration g,σ canberewritten,astheresultofbranching,into gl,σ∧cl or gr,σ∧cr whenσisnotasolutionandisnotshowninconsistent.

Theoperationalsemanticscharacterizesthesetofsolutionswhichcanbereachedfromagoalgandaconstraintstoreσbyapplyingthetransitionrules. Itisexpressedintermsofthetransitiveclosure →of →.

De nition2.1(OperationalSemantics).Letgbeagoalandσbeacon-straintstore.Thesetofsuccessfulcomputationsof g,σ ,denotedbySOL(g,σ),isde nedas

SOL(g,σ)={σ | g,σ →σ }.

2.4.2HypothesesandPropertiesofSearchProcedures.Asmentioned,thisarticlerestrictsattentiontocompletesearchprocedures,thatis,goalsthatcan ndallsolutionstoaconstraintstore.

De nition2.2(Completeness).Letgbeagoalandσbeaconstraintstore.GoalgiscompleteforσifSOL(g,σ)=SOL(σ).

Itisnaturaltoexpectthat,ifgiscompleteforσ,thenitisalsocompleteforallconstraintstoresσ suchthatσ σ,sinceaddingmoreconstraintstoastoreshouldpreservecompletenessofthesearchprocedure.Thisjusti esthefollowing,stronger,notionofcompleteness.

De nition2.3(DownwardCompleteness).Letgbeagoalandσbeacon-straintstore.Goalgisdownward-completeforσifgiscompleteforallσ satisfyingσ σ.

Thisarticlealsorestrictsattentiontoterminatingsearchproceduresthatis,onceagain,naturalinconstraintsatisfaction.

De nition2.4(Termination).Letgbeagoalandσbeaconstraintstore.Goalgis niteforσifthereexistsnoin nitesequenceoftransitionsteps

g,σ → g1,σ1 →··· → gn,σn →···

Thealgorithmsdescribedinthisarticlereceive,asinputs,agoalgandacon-straintstoreσsuchthatgisdownward-completeand niteforσ.TheycomputethesetSOL(σ)or,equivalently,thesetSOL(g,σ).Thealgorithmsdifferinthewaytheyexplorethetransitionsteps,thatis,howtheychosetoexplorethecon gurationsgeneratedbybranching.Wenowpresenttwopropertiesofcom-pletesearchprocedures.Thebranchingpropertyguaranteesthecompletenessofsubgoalswhiletherestartingpropertymakesitpossibletousetheoriginalsearchprocedureonintermediarystores.

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