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 357

Mostreasonablesearchprocedurescanbeexpressedintermsofbranchingfunctions.Inatraditionallabelingprocedure,clandcrmaybeconstraintsoftheformx=vandx=v,wherexandvaretheselectedvariableandvaluerespectively.Injob-shopscheduling,clandcrareconstraintsoftheformrank=randrank>r,whererankisthevariablerepresentingtherankofagiventaskonamachineandrrepresents,say,the rstrankavailableonthemachineinthecurrentconstraintstore.Itispossibletogeneralizethisoperationfurther(e.g.,tohaven-arybranchesormoregeneraloperationsinsteadofconstraintsclandcr)butthisisnotnecessaryforthepurposeofthisarticle.

2.4PropertiesofSearchProcedures

Thisarticlerestrictsattentiontocompletesearchprocedures,thatis,goalsthatcan ndallsolutionstoaconstraintstore.Italsoassumesthatgoalsalwaysterminate,thatis,thereisnoin nitesequenceofbranchings.Finally,thisarticlealsoassumesthat,ifagoaliscompleteforaconstraintstoreσ,itisalsocompleteforanyconstraintstoreσ∧c,wherecisaconstraintoverasubsetofthevariablesofσ.Thesethreeassumptionsaresatis edbyall“reasonable”searchproceduresforconstraintsatisfactionproblems.Together,theyalsoimplythatagoalgiscompleteforaconstraintstoreσ obtainedafteranumberofbranchingsfromgandaninitialconstraintstoreσ.Therestofthissectionformalizestheseconcepts.

2.4.1TheOperationalSemantics.Theformalizationusesanoperationalsemanticsbasedonatransitionsystem(SOSsemantics)[Plotkin1981].Thecon gurationsofthetransitionsystemrepresentthecomputationstates;theyareoftheform g,σ andσ.Con gurationsoftheformσareterminalandrepresentsolutions(i.e.,SUCCESS(σ)holds).Transitionsrepresentcomputationstepsandatransitionγ →γ canbereadas“con gurationγnondeterminis-ticallyreducestoγ .”Transitionrulesarede nedusingtheformat

<condition1>...<conditionn>expressingthefactthatatransitionfromγtoγ cantakeplaceiftheconditionsareful lled.Thereareonlythreetransitionrulesintheoperationalsemantics.Therule

SUCCESS(σ)

expressesthatthecomputationterminatesassoonastheconstraintstoreisasolution.Therules

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

llACMTransactionsonComputationalLogic,Vol.5,No.2,April2004.