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 365

con gurationfailsorsucceeds,RLDSpopsfromthequeueacon gurationwiththesmallestnumberofdiscrepancies.Thiscon gurationbecomesthenewac-tivecon gurationandRLDSproceedsasbeforewiththisnewcon gurationandthenewqueue.AkeystepinimplementingRLDSistorestorethenewactivecon guration.Let

ccpc=<d1,...,dn,dn+1,...,dn+i>

bethecomputationpathofthecurrentactivecon guration,let

oopo=<d1,...,dn,dn+1,...,dn+j>

bethepoppedcomputationpath,andlet

<d1,...,dn>

bethelongestcommonpre xbetweenthesetwopaths.RLDSrestoresthecon gurationuniquelyidenti edbypointwosteps:

(1)itbacktrackstothecon gurationwhosepathis<d1,...,dn>;

oo(2)itrecomputesthesuf x<dn+1,...,dn+j>.

Observethatrestoringacon gurationamountstowalkingtheshortestpathbetweenthetwocon gurationsinthesearchtree.

Figure6describestheimplementationofRLDSforsatis ability.RLDSSATIFYexpectsagoalgandaconstraintstoreσandreturnsSATISFIABLE(σ).Itsimple-mentationcreatesanemptyqueueandcallsRLDSEXPLORE.FunctionRLDSEX-PLOREexpectsagoalg,astoreσ,thecomputationpathpofthecon guration g,σ ,andaqueueQ.Itexploresallthesolutionsthatcanbereachedfrom g,σ andthecon gurationsinQ.Itsimplementation rsttestswhetherσisasolution,inwhichcaseitsucceeds.Ifσisafailure,RLDSEXPLOREmustexplorethecon gurationsinQandthuscallsRLDSEXPLOREQUEUE.Other-wise,RLDSEXPLOREappliesthebranchingfunction,pushestherightdisjunctontothequeue,andexploretheleftdisjunctwiththenewqueue.FunctionRLDSEXPLOREQUEUE(g,σ,pc,Q)exploresthecon gurationsinQ,startingfromcon guration g,σ ,whosepathispc.Ifthequeueisempty,itreturnsfalse.Otherwise,itpopsfromthequeueapathpowiththesmallestnumberofdis-crepancies,restoresthecon gurationuniquelyidenti edbypo,andcallsRLD-SEXPLORErecursivelywiththenewcon gurationandthenewqueue.ProcedureRLDSRESTORErestoresthecon guration.Itassumesthat<d1,...,dn>isthelongestcommonpre xofpoandpc.It rstbacktrackstothecon gurationiden-ti edbythiscommonpre x,restoringtheconstraintstoreσandthegoalg.It

oothenrecomputesthebranchingdecisions<dn+1,...,dn+j>byfollowingthissuf xofpo.

Themainbene tofRLDSistoavoidexploringthesameregionsofthesearchtreeseveraltimes.Asaconsequence,itmaybesubstantiallyfasterthanILDSinpractice.However,RLDSalsohasanumberoflimitations.First,RLDSismoredemandinginmemory:itisnecessarytostorethecomputationpathsofthecon gurationsinthequeue.Thisisatypicalspace/timetradeoffandtherightchoiceprobablydependsontheapplicationathand.Moreimportantperhapsisthelackofrobustnessofthisimplementation.

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