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.