A Decomposition-Based Implementation of Search Strategies(5)

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 355

SUCCESS(Storeσ):Bool

post:SUCCESS(σ)iffσisconsistentandallvariablesareinstantiated.FAILURE(Storeσ):Bool

post:FAILURE(σ)impliesσisinconsistent.

TELL(Storeσ,Constraintc)

pre:σ= c1,...,cn .

post:σ= c1,...,cn,c .

BACKTRACK(Storeσ)

pre:σ= c1,...,cn,c .

post:σ= c1,...,cn .

EVAL(Exprf,Storeσ):int

pre:SUCCESS(σ).

post:EVAL(f,σ)isthevalueoffinσ.

BRANCH(Goalg,Storeσ):(Goal×Store)×(Goal×Store)

pre:¬SUCCESS(σ)∧¬FAILURE(σ);

giscompleteforσ.

post:BRANCH(g,σ)= (gl,cl),(gr,cr) ;

σ (σ∧cl)∨(σ∧cr);

cl∧crisinconsistent;

gliscompleteforclandgriscompleteforcr;

gistheparentofglandgr.

PARENT(Goalg):Goal

pre:gisnottheinitialgoal.

post:PARENT(g)returnstheparentofg.

Fig.1.Speci cationofthemainoperations.

isconsistentandassignsavaluetoeachofitsvariables.Itreturnsfalseother-wise.FunctionFAILURE(σ)returnstrueifσcanbeshowntobeinconsistent.Itreturnsfalseotherwise.1ProcedureTELL(σ,c)addsconstraintctostoreσ.Pro-cedureBACKTRACK(σ)removesthelastconstraintaddedtoσ.Finally,procedureEVAL(f,σ)returnsthevalueofexpressionfinsolutionσ.

2.2SolutionsandOptimalSolutions

Thepurposeofthealgorithmsdescribedinthisarticleisto ndoneorallsolutionstoaconstraintstoreorto ndthesolutionofaconstraintstorethatminimizesanobjectivefunction.Thesolutionsofaconstraintstoreσaregivenby

SOL(σ)={σ |σ σ&SUCCESS(σ )}.

1Observethat,astraditional,FAILURE(σ)mayreturnfalseeventhoughσisinconsistent.

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