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
356 L.MichelandP.VanHentenryck
Aconstraintstoreσissatis able,denotedbySATISFIABLE(σ),ifitssolutionsetisnon-empty,thatis,
SATISFIABLE(σ)≡SOL(σ)= .
Theminimumvalueoffinσ,denotedbyMIN(f,σ),isthesmallestvaluetakenbyfinanysolutionofσ,thatis,
MIN(f,σ)= minσ∈SOL(σ)EVAL(f,σ ).
Aminimalsolutionoffinσisasolutionofσwhichminimizesf,thatis,asolutionσ suchthat
EVAL(f,σ )=MIN(f,σ).
Intherestofthearticle,weonlypresentalgorithmstodeterminethesatis -abilityofaconstraintstoreandto ndtheminimumvalueofafunctioninaconstraintstore.Satis abilityisusefultointroducethemainideasbehindthealgorithmsandtheirproperties.Minimizationisparticularlyimportantsinceitillustrates,inasimpleway,manyissuesarisingwhenintroducingglobalcutsandnogoodsindynamicsearchprocedures.
2.3SearchProcedures
Searchproceduresareusedto ndsolutionstoconstraintstores.Asmen-tionedearlier,itisimportanttoconsiderdynamicsearchprocedures,sincetheyraisethemaindif cultiesinimplementingsearchstrategiesef cientlyandarewidelyusedinpractice.Indeed,standardlabelingproceduresgenerallychoosethenextvariabletoassigndynamically(e.g.,usingthe rst-failprin-ciple[HaralickandElliot1980]).Theymayalsoorderthesequenceofvaluesdynamically,onceagainusinginformationfromtheconstraintstore.Similarly,injob-shopscheduling,thechoiceofthemachinetoscheduleandthechoiceofthetasktorankontheselectedmachineisgenerallydynamic.Inaddition,somesearchproceduresarerandomized(e.g.,Nuijten[1994]).
Tocapturethedynamicandrandomizednatureofcomplexsearchproce-dureswhileretainingahighlevelofabstraction,weassumethatsearchproce-duresarespeci edbygoalsas,forinstance,inconstraintlogicprogramming.Inaddition,tosimplifythepresentation,weonlyuseonebranchingoperationBRANCH(g,σ),whichrewritesthegoalgintotwosubgoals,possiblyusingin-formationfromtheconstraintstoreandrandomization.Thespeci cationofFunctionBRANCHisalsogiveninFigure1togetherwiththespeci rmallyspeaking,functionBRANCH(g,σ)rewritesgintoadisjunction
(gl∧cl)∨(gr∧cr),
whereclandcrpartitionsthesetofsolutionsofσ.Thegoalsglandgrareassumedtobecompletesearchproceduresforσ∧clandσ∧cr,respectively.Observethattheorderofthedisjunctionsisimportantforthepurposeofthisarticleasthebranchingfunctionrecommendstoexploretheleftdisjunctbeforetherightone.
ACMTransactionsonComputationalLogic,Vol.5,No.2,April2004.