A Theoretical Framework for Consistency Techniques in Logic Programming

1. Motivation

Our work aims at the intesration of CTo inside a declarative programmins lansuase in order to solve Constraint Satisfaction Problem· (CSPo).

The clau of CSPo io of great Importance in AI as, for inltance, sraph colouring, graph isomorphisms and homomorphiomo, boolean oatiofiability, ocene and edse labelins and logical puuleo can be oeen ao particular easel of it. A CSP can be defined in the following way . Auume the exiotence of a finite let I of variable· which take respectively their valueo from finite domain· and a let of conotrainll. A conotraint betwe~n k variable· from I io a subset of the carteoian product of thf' respective variable domain· which opecifieo which values of the variable· are compatible with each other. A oolution to a CSP i· an assignment of values to all variable· which oat i·fies all the constraints and the task

io to find one or llll the ·olutions.

CTo are a powerful paradigm for solving CSPs. They should be contrasted to "generate &. test", standard backtracking (depth-firot oearch with chronological backtracking) and dependency-directed backtracking. Clearly, "generate & test" io an unfeasible search procedure as ooon as the oi~e of a problem make· it interesting to conoider. "Generate & test" correspond· to the naive way of writing logic program· for CSPo. For inotance, a "generate & test" for the 8-queens problem· aeneratel a pouible confiauration for the queens and then teot the constraint·. Standard backtracking (ST) , while beina a oubotantial Improvement over "sene rate & teat", leads to a pathological behaviour known ao thraohing. In lop;ic programming, ST correopondo generally to a "sene rate & test" program with coroutining information· or to a program written for teotina the conotrainh ao soon as possible. Dependency­ directed backtrackins [14] hao been introduced in order to avoid one of the thrashina oymptoms but it is more a remedy to a oymptom of the malady and not to the malady itself. Indeed, it i· better to prevent failures than to react order to uae CTt in logic programming. For thia purpose, the next section introduces the domain concept and the unification algorithm is extended to handle it . Next, the inference rule· are defined and their formal propertiea are inveatigated.

Our approach ahould be related in philosophy to the worh on conatrainh in Josie programmins (··I j7, 2Jl. It differa from them as we are not restricted to a aet of built-in constraints. General mechanism· are provided which can be uaed for any constraint to aolve problema in a well-defined clau.

2. Domftins in logic progrftmming.

2 .1. The domftin concept.

Domains provides the baaio for uain1 CTa in Josie programmins. It io often the cue that variable~ ran1e over a finite domain but thia information cannot be expreued clearly in Josie programmin1 lansuasea. DomAin llecltmltioru have been introduced for taking thio fact into account j16].

Definition 1: A domAin declaration for predicate aymbol p of arity n is an expression of the followins form.

domain p(a 1 , ... ,an) where ai is either h or di'

When ai io equal to h, thi· means that the ith arsument of p ranges over the Her-brand univerae. Otherwioe, it means that the ith arsument is a Jilt of variable· which ranges over di' In the followins, the domains di are finite and explicit seta of values (i.e conllanh) .

Definition 2: Let dl, ... ,dn the domains appearins in the domain .declarations of a Josie program PR and different from the Herbrand universe. We note D(PR) the aet { d I d -f8 and d E 2di (1 ::;; i ::;; n)} . We call it the domain aet of the Josie prosram. The domain aet of a logic program contain· all domains we po11ibly need durins the computations.

The resulting l.anguase i· a fint·order lansuase with aggresate variables !6]. This meant that the domain· mutt be seen as unary relationo and an assresate variable as a variable which ranse· over this unary relation. In the following, we refer asgregate variables as d·variables (domain variables), we note x d a variable x ranging over d and we uae a E d to denote d(a) where a is a constant. Also, we use 3P and V'P to denote the existential and universal cloture· of P. Two rulea are added to the usual firat·order validity rules. We auume an interpretation I and a variable . uai1nment A. A(x/Y) i· A with x assigned to y and jd] 1 is the unary relation d defineo in I. The terms are constructed as uaual except that variables can now be usual variables and d·variableo.

1. If the formula has the form 3xdF, then the truth value of the formula is true if there exiata dEjdJ 1 ouch that F has truth value true wrt I and A(xdld ); otherwise ita truth value is falae.
2. If the formula has the form V'xdF, then the truth value of the formula io true if for all dE!dJ 1 we have. that F has truth value true wrt I and A(xd ld); otherwia. ita truth value i· faloe.

The unification algorithm mutt be extended to take the domain· into account . Informally, a d·variable and a conatant can only been unified if the constant it in the domain of the d-variable. Also, when unifyins a variable and a d·variable, the variable it bound to the d-variable. Finally, two d· variables can only be unified if the interaection of their domains ia not empty, in which cue they are bound to a new variable whose domain it thit intenection.

2.2. Properties of the domftin concept.

We now propertiea. define formally the alsorithm We firat need tome notiona. and atudy It·

Definition 3: We aay that the range of t i· included in a domain d, noted ltl E d, if t it a conatant E d or a d· variable xdl auch that dl ~ d.

Deftnltlon 4: An d·oubatitution fJ it a finite aet of the form {v 1 jt 1 , ... ,vn/tn}, where

1. each v 1 i· either a variable or a d-varlable.

2. ti it a term diatinct from vI'

3. v 1 , ... ,v n are all diatinct.

4. if vi Ia a d-variable vd 1 , ltil E dl.

Definition II: We aay that two d·tubatitutiona (J and A agree on a aet V of variable· and d·variablea, denoted fJ = A!\11 iff z.fJ = z.A for each x E V where = denote· the ayntactic equality.

Definition 6: fJ i· a d·inotance of A in V, denoted A :5 6, iff (J = 6 o AjVJ for tome d·tubatitution 6. In the following, we uae A6 inatead of 6 o A.

Definition 'T: A d-aubatitution 11 i· an d·unifier of tome non-empty and finite aubaet S={t 1 , ... ,tn} where t 1 it a literal or a term iff t 1 11 = ... = t n 11; we alto aay that f1 unifiet S. UNI(S) it the set of all d·unifien of S. f1 I· called a moll general d-uni/ier or d-mgu of S iff for each fJ E UNI(S), (J ::;; f1!varo(S)J impliea 11 ::;; fJ!van(S)J where vara(S) ia the set of all variable or d·varlable aymbolt in s.

In the following, we use aubatitution and msu lnatead of d· substitution and d·mgu. We now preaent the unification algorithm. In this algorithm, S denote· a finite aet of predicate· or terms, the empty aubatitution and the disagreement aet is defined at usual (for inatance 110]).

UNIFICATION ALGORITHM.

1. Put k= 0 and f1 0 =c
2. If Su k ia a aingleton, then atop; 11 k is the aubatltutlon returned by the alsorithm. Otherwiae, find the diaasreement set of Dk of Su k'
3. If there exist v and t in Dk auch that v i· a variable that doeo not occur in t , the.n put "k+l=f1k{v/t}, increment k and ao to 2.
4. If there exiot vd and a conatant c in Dk auch that c
5. E d, then put f1k+l =-11k{vdfc}, increment k and 10 to 2.
6. If there exiat vdl and wd 2 in Dk auch that dl 2 d2 then put "k+I=Uk{vdl fwd 2 ), increment k and 10 to 2. 6. If there exiat vdl and wd 2 in Dk auch that d3 = dl n 02 f e then put ,k+l=uk{vd 1 /&d 3 ,wd 2 j&d 3 } where &d 3 io a new variable rangin1 over d3, increment k and so to 2. 7. Otherwlae, atop; S it not unifiable.

Clearly, this algorithm terminates becauae S contain· only finitely many variable· and each application of ltepa 3, .. ,6 decreuea by one the number of varlablea. We now prove that the unification algorithm doea Indeed find a m1u of a unifiable aet of &erma or predicatea. U Ia a 1enerall&atlon of tbe uaual unification theorem (aee for inltance ]10]).

Theorem 8: (Unification theorem).

Let S a finite set of term· or predlcatea. If S Ia unifiable, then the unification algorithm terminate· and 1ive1 an m1u for S. If S i1 not unifiable, then the unification al1orithm terminate· and reportl tbla fact .

Proof We have already noted that tbe al1orltbm alway· terminate·. It aufficea to ahow that If S II unifiable, then the algorithm finda an m1u. In fact, If S II not unifiable, then the algorithm cannot terminate at atep 2 and, alnce It doe· terminate, It muat terminate at atep 7. Tbua It reporta the fact that S Ia not unifiable.

Auume then that S Ia unifiable and let 9 be any uniAer for S. We prove firat that, for k~O, If cr 11 Ia the aubatltutlon 1lven at the kth Iteration of the al1orithm, then there exlata a aubatitution 7k auch that 8 = cr~o7~oJvan(S)J .

Suppoae firat that k=O. Then we can put 7o = 9, alnce 9 = t8. Next, auppoae for aome k~O, there exlata cr 11 auch that 8 = cr k 7 ~olvan(S)J . If Scr k Ia a aln1leton, then the al1orlthm terminate· at atep 2. Hence we can confine attention to the caae when Scr k Ia not a aln1leton. We want to ahow that the al1orlthm will produce a ·further aubatltution IT k+ 1 and that there exlatl a aubatltution 7k+l auch that 8 = 1Tk+l7ktl]vara{S)J. Since scr 11 Ia not a alngleton, the al1orlthm will determine the dlaa1reemen t aet D k of SIT k an.d 10 to Step 3. Since fJ=IT~o7~olvan{S)J and 8 unlfiea S, It follow· that 7 11 unlfiea 0 11 . Thua 0 11 muat contain either a variable or a

d·varlable.

Suppoae first that 0 11 contain· a variable v and let t another term of 0 11 . Then v cannot occur In t becauae v7 11 = t7 11 . We can auppoae that {v/t} II Indeed the aubatltution choaen at atep 3. Thua crk+l = cr 11 {v/t}. We now define 7k+1 = 7 11 \{v/v7 11 }). If 7k bu a blndln1 for v, then

7k {v/V7k} u 7ktl "Jk {v/t")'k} u "~'k+l "~'k {v/t")'k+l} u "~'k+1

If ")'k doe~ not have a blndln1 for v, then ")'k+l = ")' 11 , each element of 0 11 Ia a variable and ")' 11 = {v/t}'lk+l' Thua 8 = ITk "Jk]van(S)J IT 11 {v/t}"J 11 + 1 ]vare(S)J = crk+l"~'k+JJvan{S)J , u required .

Now, If 0 11 doe· not contain a variable, It contain· a d· variable. The atepa .f and 6 can be handled In the aame way aa the atep 3.

We now conalder a&ep 6. Let v1d 1 and v2d 2 be the two d·varlablea In 0 11 and we 1uppo1e that the aubatltutlon choaen In thl1 atep Ia {v1d 1 jad 3 ,v2d 2 /ad 3 ) where ,d 3 II a new variable. We fire& note that v1dl and v2d 2 have blndln1· In ")' 11 . Alao, alnce ]v1dl"Jkl. E dl, ]v1d 2 ")' 11 ] E d2 and v1d 1 7 11 = v2d 2 .,. 11 , we have that ]v1d 1 ")' 11 ] E d3 and ]v2d 2 ")' 11 ] E d3. U follow· that {ad 3 Jvldl"Jk} I· a d· aubatitution. We now define 6 = ")'II u {ad 3 /vld 1 ")' 11 }. We have that

Now we can complete the proof. If S Ia unifiable, then we have ahown that the al1orlthm mult terminate at step 2 and, If It terminate· at the kth Iteration, then fJ = cr 11 ")' 11 ]van(S)J. Since IT k Ia a unifier of S, thla equality 1how1 that It Ia Indeed an m1u for S. V

We refer SLD·reaolution with thl· extended unification al1orlthm u SLDD·reaolution. The notion· of SLDD·refutation and SLDD·anawer aubatitutlona are defined by analo1i to tbe SLD cue. The reader can verify eully that the m1u and llftln1 lemmu u well u theorem· 7.1 and 8 . .f In ]10] bold for SLDD·reaolution. Tbua, SLDD·reaolutlon II both aound and complete for definite clauae1. Thl1 reault correaponda to the one of ]6] which bu abown that reaolutlon Ia aound and complete when extended for bandlln1 d·varlabln Allo, &be aame reaul& can be proved If we · awl&cb to a many·aorted lo1lc alnce the domain nt au1mented by &be herbrand unlveree and the empty nt can be or1anlaed u a meet·aemllanlce ]18]. The domain concept Ia a neceanry extenalon for conalatency tecbnlqun to be applied but II not In it·aelf u lntereatln1 u other extenalon1 like, for lnatance, LOGIN ]1]. Before preaentin1 the Inference rulea, we define the conatralntl we

conaldered. ·

Deftultloo 01 Let p be a n·ary predicate aymbol. p Ia a cOtU!raillt I« for any 1round term· & 1 , ... ,t 0 , either p{t 1 , ... ,tn) bu a auccealful refutation or p{t 1 , ... ,t 0 ) bu only finitely failed derlvationa.

3. Forward checking in logic program­ ming.

Forwortl clltclrlrlf Ia often conaldered u one of the moat emclent procedure· for aolviDI CSPa. Intuitively I a CODI&ralnt can be uaed In forward cbeckln1 u aoon u at moat one variable occur· In 1&. In tbll cue, tbe ae& of poaalble valufl for the variable II reduced to the aet of value· wblcb ntllfy the constraint. Tbua, a pro1ram baaed on forward cbeckln1 1lvea a value to a variable, uaea all cona&ralntl which contain·

at moe& one variable, chooaea a value for &he next variable, uaea &he cona&ralnh and ao on until all variable· have received valuea. If, durln1 &he aearch, a cona&raln& cannot be aatlafied (1& reduce· &he ae& of poulble valuea for a variable to &be empty ae&), the aearcb procedure 1lvea another value to &be prevloualy ual1ned variable. Tbla aec&lon define· &be FCIR and Ita uae for a 1·neral control mechanlam, forward declara&lona, and for the Implementation of aome bull&·ln predlca&ea. They enable pro1rama prevloualy bued on a ST or "1enera&e " tea&" aearcb to uae a forward checkln1 a&ratel)'.

3.1. The inference rule.

Deftnltlon lOa A literal p(x 1 , ... ,xn) In the reaolven& Ia fonuord clleclu&ble Iff p Ia a cont&ralnt and all lh ar1umenh are 1round but one which I· a d·varlable. Thl1 d·varlable Ia called the forward-variable.

Deftnltlon lla The forward checkiDa Inference rule (PCIR).

Let G 1 be the 1oal · .... A 1 , ... ,Am. 1 ,P,Am+ 1 , ... ,Ak' and PR be a lo1lc program. Gl+ 1 Ia derived from G 1 ualn1 m1u 8 1 + 1 via PR If the followln1 condition· hold

1. P I· forward checkable and xd Ia the forward· variable.
2. dnew = {a E d I PR I= P{x/a}} and dnew f {}.
3. 8 1 +1 I·
4. {xd /e) If dnew = {e).
5. . {xd /&dnew} where ,dnew 11 a new variable otherwlae.
6. G 1 + 1 Ia the 1oal 1 +-(A 1 , ... ,Am. 1 'Am+ 1 , ... ,Ak)tl 1 + 1 ·.

Since a 1round lnttance of a conltralnt either tucceedt or finitely lalla, the 1et dnew In point 3 of the definition can , be computed eully (for lnttance by u·ln1 SLDD·reaolutlon)".i The FClR can be teen u a 1eneral mecbanlam for enforcln1 node~ contlatency 111).

The FCIR provide~ a theoretical founda&lon (1) for a ·1eneral control mecbanltm, forward declara&lona, &bat can be uted whatever the kind of conatralnh to be ta&ltfied and ,(2) for the lmplementa&lon of aome bull&·ln conatralnh.

Forward declara&lona 1171 provide a 1eneral method· for u1in1 forward checkln1 lntlde lo1lc pro1rammln1. A forward declaration for a predicate 1ymboJ p of arity n ' II 'an expreulon of &he followln1 form·.

forward p(a 1 , ... ,an) where a 1 I· either 1 either d. Thi1 declaralion, which i· unique for a parlicular predicate 1ymbol, apecifiet &hat a literal p(t 1 , ... ,&n) In &he reaolven~ can ·"< be aelec&ed only when all lh ar1umenh correapondln1 to a '1' In &he declaraliun are 1round and when I& I· either 1round or forward checkable. When I& I· forward checkable, the FCIR mua& be uted to reaolve I&; o&herwlte, normal derh:alion 11 applied.

Forward declaration· are bet& combined wl&b ' a 1pecial; purpote compu&alion rule.

Deftnltlon Ua A computation rule Ia efficient wrt the forward declaration·, If I& telec&a only a pre.!llcate tubmiUed to forward deciaralion when It Ia around or forward checkable and If, whenever the retolven& contain· literal· 1ubmiUed to a forward declaration which are either forward-checkable or 1round, It telech one of them. ·

The main ln&ertlh of a efficient compu&alion rule wr& the forward declaration· are for expreulveneu and efficiency. Cona&ralnh can be ata&ed before the 1enera&on and &he Interpreter/complier Ia reapontlble to aelec& them a& an appropriate computation ltep. Tbua, forward declaration· will ad u precondltlonl to &he telec&lon of a predicate and can be teleded u toon u poulble for reduclns the aearch apace. Thl· ln&rodurea a 'dalo·"""·"' computation u, for lnt&ance, In the conltraln& lansuaae of 116) and a senerall&ed form of

forward checkln1.

Example 1 Contlder &he problem of colourln1 a map In (our colort. A Josle prosram for aolvln1 thla problem will Include a conttralnt dlfferent(X, Y) which hold· If X and Y are different colon. h can be defined u a finite aet of uaertlon· of &he form

dlfreren&(color1,color2)

dlfreren&(color1,color3) +­

dlfferent(color1,color4) +-

whe're color1, color2, color3 and color4 are the cona&anh for the poulble colon. Alto, the forward declaration 'forward dlfferent(d,d)' tpeclfiet we wan& a forward checklns ute of this predicate. Now, If the retolven& contain· a literal 'dlfferen&(color1,xd)' with d = {color1, ... ,color4}, the FCIR will return a blndlna {xd Jad 1 ) where d1 = d \ {color1}. Tbla prune· the tearcb 1pace In a 'a priori' way by reduclns the 11& of poulble ve,luet which can be auisned to xd.

The FCIR provide· alao a theoretical foundation for the Implementation of bull&·ln conttralnh which are &he prlmltivea of the loalc lan1uase (e.a arithmetic conltrainta). In uaual loalc lansua1ea, &hete cont&raln&a can only be uaed for &eatln1 value~ and &hua only reduce the tearcb apace In an ·a poaterlorl way". However, the FCIR can be apeclall&ed for tbete conltralnh which now can not only teat value· but can alto prune the aearch apace when only one d·variable i1 left unlnllantiated. Contlder a non·equall&y conltraln& between ln&eaen (i.e x f y which bold· If x and y are different ln&e1er1).· ln u1ual lo1ic lan,ualet 1 &he non-equality predicate Ia Implemented by mean of the · nesatlon aa failure" rule and &bua can only be telec&ed when both ar1ument1 are 1round. By redefinin1 tbla conl&ralnt aa apeciali&a&ion of the FCIR, the aame prunlns u the above different predicate is achieved but In a more efficient way.

3.2. Properties of the FCIR.

We now prove &he toundneu and comple&eneu of the FCIR. The firt& two Jemmu allow u1 to "remove" a value from the domain of a d·variable If tbi· value doea not aa&idy a

cont&raln&.

Lemma 13: Let F a conjunction of predlca&et con&ainin1 x 1 , ... ,xn a· variable~. Let PR a Josle program and Mpr I&· minimal model . Then (I::.Mpr 3F) -. (PR I= 3F) . Proof: Let M be a model of PR. We ahow &hat 3F i· &rue In M. If M I· a model, we can define a Herbrand

model Mh of PR aa followa

Mh = {p(&l'"'''n)lp(t 1 , ... ,tn) Ia Included In &he Herbrand bue and Ia &rue In M}

Since i=Mpr3F, &hen it Ia true in all Herbrand model· _ and I=Mh 3F. h follow· that there exia& term t 1 , ... ,tn in &he Herbrand unlverte tuch &hat I=Mh F{x 1 /tl' ... ,xn/tn}. By definllion of Mh and alnce F{x 1 Jt 1 , ... ,xn/tn} Is a conjunrlion of sround predicate~, F{x 1 /& 1 , ... ,xn/tn} is true In M. Tho·, 3F Ia true In M. V

• A almllar conatruct hu been used in ItO] .

Lemma 14: Le& PR be a Josle prosram, d and dnew be non-empty domain· auch that d = {a 1 , ... ,ap} and dnew = d\{a 1 }, 'let P, P 1 , ·.. ,P m be poaltive llterala auch that P contain· a free variable xd and {xd,x 1 , ··· ,x 0 } are the ae& of free varlablea occurrlns In P, P 1 , ... ,P m. We note Q the tl wff P 1 1\ ··· 1\P m and F the wff 3z 3zl" ·. 3z"{P 1\ Q). Then

PR l~3z 1 ... 3z 1 l{z 11 /ct 1 } lmpllea F=. PR F{z 11 ;i"'w} Proof: Since PR Ia a aet of definite clauaea, It admlh a minimal model, noted Mpr, which Ia the lnteraection of all modela of PR. Since we know that PR l~3zl" ·· 3z"P{z 11 /ct 1 }, It follow· that

• PR l~3zr ·. 3z"(P{z 11 Jca 1 } 1\ Q{z 11 /ct 1 }}
• tl tl · lf.y,, 3z 1 .·. 3z"(P{z jca 1 } 1\ Q{z jca 1 }) (lemma 12}
• lf.y,,F{ztl/cal}

Hence, the followins are equivalent.

• PR I= F
• I=Mpr F
• tl tl · I=Mpr F{z Jca 1 } v ... v F{z Jca,}
• tl tl · I=Mpr F{z Jca 1 } or ... or I=Mpr F{z Jca,}
• tl tl · I= MprF{z /ct2} or ··· or I= MprF{z /ctl'})
• tl tl · I= MprF{z /ct 2 } v ... v F{z Jca,}
• I=M F{xd Jxdnew} pr
• PR I= F{z 11 /ztlnew} (by lemma 13} V

Note that thia lemma Ia no looser true If PR ia an arbitrary eet of clauaea.

Lemma U: ((~3(QAP))/\\IP) = ((~3Q}A\IP).

Theorem 16: Soundneu of the FCIR.

Consider PR be a Josie prosram, G 1 a coal '..- " Al' ..· ,Am·l'P'Am+l' ''''Ak' where P ia a forward checkable literal and xd ia the forward variable. We auume that d = {a 1 , ... , an' b 1 , ... , bm} and dnew : {b 1 , ... , bm} both beins not empty. We alao auume that {xd,x 1 , ... ,x 1 } ia the ae& of all free varlablea of G i' We note Q aa A 1 1\ ... 1\ Am-I 1\ Am+ 1 1\ ... 1\ Ak. and reatate G 1 aa ~3z 11 3z 1 ... 3z 1 (Q 1\ P). We prove that G; = PR Gi+ 1 .

Proof:

From point 3 of the definition of the FCIR, we know

• d d 1. PR I~ P{x Ja 1 } 1\ .. . 1\ PRI~P{x /an}.
• 2_ PR I= \lztlnew P{xd /zdnew} .

Then, by (1) and aucceuive application· of lemma 13, ~3z 11 3z 1 ... 3z 1 (Q 1\ P) Ia equivalent in PR to

• 3 tlnew 3 3 { tl/ tlnew} · .., z z 1 ... z 1 Q z z
• Q91+1
• Gi+l V

We now turn to the completeneu of the FCIR. We fint define an SLDFC·reaolutlon u a proof procedure which uaea the FCIR for fonord checkable predicate· and SLDD· reaolution otherwlae. We alao apeak about SLDFC·refutation and SLDFC-anawer aubatltution.

Theorem 1 T: Completenel8 of the FCIR. Let PR a Josie prosram and G a coal. If there exlah a SLDD· refutation of PRu{G} with a SLDD·anawer aubatitution 9, then there exiat a SLDFC-refutation of PRu{G} with a SLDFC·anawer aubatitution 11 auch that 11 ~ 9.

Proof We prove It by induction on the lensth of the SLDD·refutation.

Suppoae I = 1 and G ia forward-checkable. Then, let x be the forward checkable variable and 11 the aubatitution reaultins· from the application of the FCIR. Then, given any SLDD·anawer aubatitutlon 9, by definition of the FCIR, there exiah a SLDFC·refutation with SLDFC·anawer aubatitution 11 auch that 11 ~ 9.

Suppoae the reault holda for I -~ I and we ahow that it holda for I = i+l. Let G = '.-A 1 1\ .. ,I\A"I\P'. Suppoae P

ia forward checkable, x ia the forward variable and {x/zd} ia the aubltitution reaultins from the application of the .FCIR. Conaider a SLDD·refutation of PRu{G} with SLDD·anawer aubatitution 9 and auppose 9 have a bindins for x. Let 9 be {x 1 jt 1 , ... ,xnftn,xft}. Since, by definition ,of the FClR, It I E d, 9 can be restated u 6 = 6·6· where 6· = {x/zd} and 6· = {x 1 jt 1 , ... ,x 0 /t 0 ,zd /t}. It follows 'that ,- 9 = 6]var(G}] and thua 9 can be viewed aa a re"atriction of 6 to the varlablea of G. A lao, ':J',Ru{-:-(A 1 A ... AAnAP}6} haa a SLDD·refutation (the aame ii ai. - ~he,. one which return a 9 except for the unifiers and the Initial coal} of the aame length with SLDD-anawer aubatltution € . Now, we can conatruct a SLDD-refutation <>,f; PRu{.-(A 1 A ... AAn}6}(by removing the ateps concernins the refutation of P6) with SLDD-anawer substitution €. By · tl\e lifting lemma, PRu{(A 1 A ... AAn}6'} has a SLDD· refutation with SLDD·anawer aubatitution t/1 ouch that t/1 ~ 6· . By induction hypotheais, there exiat a SLDFC· refutation of PRu(~· (A 1 A .. . /\A )6'} with SLDFC-anawer ~ n · oub~titution u· aurh that u· $ t/1. It follow a that

. \)'

6'11· S 6'1/1 S 6·6· = 9]var(G}I

Thu'a, it exiat a SLDFC·refutation of PRu{ G} with a SLDFC·anawer oubatitution 11 which ia a reatridion of 6·u· to the variable· of G ouch that 11 S 9. V

4. < Lo~kohead in logic programming.

-~ There ~xiata other CTa which use constraints even when aever~<l . variablea appe~<r in them. Typical examples are Jooka\oe~d ]SI and the arc and path-consistency algorithm· ]11.,' 13,_)9]. For inotance, given a .conatraint "C(x,y)", a lookallead 'uoe of It consiall in ~liminating from the domain of ... ' all the valuea which are not consiotent with any value of the domain of y and vice·veroa for y. The reduction of the aearclo apace io done earlier than in forward checking but ito rouiputation coot Ia higher. Aloo, the con·traint C(x,y) Ia not neceuary aolved by thia treatment and muat be reconsidered later on. The LAIR and looA:aAeo.d declaratiolll are Introduced in logic programming in order to uae lookabead whatever the kind of conatrainta used in the program. Therefore, programs previoualy baaed on a ST or "generate It tell" aearch now use Walt& filtering-like algorithm or Iookabead. Tbia ia especially Important in areaa lil!e viaion and qualitative reasoning !8).

4.1. The inference rule.

Definition 18: A literal p(t 1 , ... ,tn) In the resolvent ia looA:aAeo.d cloecluJble iff p Ia a conatralnt and there exlata at leaat one ti which ia a domain-variable and each of the other arguments ia either ground or a domain-variable. The domain-variable· in t 1 , ... ,tn are called the looA:aAeo.d 1111riablu.

Definition 19: ,The lookabead Inference rule (LAIR). Let G 1 be the goal '+- A 1 , ... ,Am·l'P'Am+l'"''Ak' and PR be a logic program.

Gi+l ia derived from G 1 uaing mgu 8i+l via PR If the following conditione bold

1. P Ia lookahead checkable and x1' ... ,xn are the lookabead varlablea wboae domain· are dxl, .. . ,dxn.
2. dxj 2. For each xj , let
3. a . d&j = { yj E dxj I 3 y 1 E dxl, ... , 3 yj·l E dxj·l, 3 yj+l E dxj+l, .. . , 3 yn E dxn such that PR I= P8 with 8 = {x 1 /y 1 , ... ,xnjyn}) and d&j f {}.
4. &i u
5. a new variable of domain d&j If d&j {e 1 , ... ,e 1 } I > 1.
6. the conatant e If d&j {e) .
7. 3· 8i+l = {xl/&1' ... ,xnf·n}
8. Gl+ 1 Ia the goal
9. '+- (A1, ... ,Am·l'Am+l''"'Ak)8 1+ 1· if at most one &i ia a d·variable.
10. ~- (A1, ... ,Am·l'P'Am+l'"''Ak)8 1+ 1· otherwise.

The LAIR can be aeen u a general mecbaniam for enforcing a k-conalatency between the k lookabead varlablea. The LAIR reducea the aearch apace In 'a priori way' and earlier than a forward checking uae of the . conatralnt. However, It takea alao more computation time to produce thla reduction. Note also, that when only one variable occura In P, the LAIR reducea to the FCIR.

The LAIR Ia the theoretical foundation for mechanlam called Iookahead declarationa. A declaration for a predicate aymbol p of arity expreaaion of the following form. a control look ahead n ia an

lookahead p(a 1 , ... ;an) where ai ia either g either d. Thla declaration, which is unique for a particular predicate aymbol, apecifiea that a literal p(t 1 , ... ,tn) In the resolvent can be selected only when all Ita argumenta corresponding to a 'g' In the declaration are ground and when It ia either ground or lookahead 'theckable. When it Ia lookahead checkable, the LAIR mull be uaed to reaolve it; otherwise, normal derivation Ia applied.

The computation rule Ia even more important for the LAIR than for the FCIR. We first define a efficient computation rule wrt lookahead declarations.

Definition :110: A computation rule is efficient wrt the lookahead declarationa, if a literal p(x 1 , ... ,xn) In the resolvent aubmiUed to a iookahead declaration ia only aelected if either it is lookahead checkable or all ita argument· are ground .

A efficient computation rule wrt lookahead declaration· givea ua few informations about when to aelect a lookahead constraint. It ia clear that aelecting it too early can induce aome unproductive work (no new Information· are inferred) and that a late selection reduces the pruning of the aearch apace. It Ia not difficult to define efficient computation rulea which aelect only lookahead conatralnta which are likely to produce new informationa. The definition of the LAIR ahould not be aeen aa auggeating a particular Implementation. Actual implementation· should be baaed, for inatance, on · generaliutiona of AC-3 111) or AC-4 112).

Example: Conaider a viaion problem In a three-faced vertex world. d = {>,<,+,·} Ia the aet of pouible labela for the vertex. Constraint· in the problem are given by the "ao·called" fork, L, T and arrow junctions. For instance, the fork junction can be defined as followa .

Also, a lookahead declaration 'looltabead fork(d,d,d)' can be spf'rified. If the re·olvent contain· a literal 'fork(xld,x2d,x3d)', an application of the LAIR retur111 the substitution {xld /&ldl ,x2d /&2d 2 ,x3d /&3dl} where dl {>,+,·} and d2 = {+,·}.

Finally, the LAIR can be apeciali&ed for aome conatrainta (e.g an inequality condraint between two lntegen). Thla will achieve the pruning defined by the LAIR in a very efficient way.

4. 2. Properties of the_ LAIR.

Theorem U: Soundneu of the LAIR.

The proof of thia theorem ia a almple generalintion of the aoundneu proof of the FCIR.

There ia no equivalent (or the LAIR to theorem 16. Tbua, a proof procedure using the LAIR for lookabead checkable predicatea and SLDD·reaolution otberwlae will not be complete. The reaaon Ia that the LAIR ia uaed only to remove inconsillent valuea and not for making choices. A aufficient condition to ensure completeneu Ia to provide generatora of valuea for the variablea occurring in predicate· aubmltted t~ lookabead declarations. Tbla reault wu expected u the L/.IR can be aeen aa a general mecbaniam for enforcing a k· consistency between the k lookabead variablea and it ia well· known that enforcing a k·consistency throughout a network of conltrainta ia not generally aufficient for aolvin1 arbitrary problema.

5. P8rti8l look8head in logic progrftm­ ming.

Tbia aection providea a theoretical baaia (or building-In aome constraint. in aucb a way that there ar~ neither a apecialiulion of the FCIR or a apecialiution of the LAIR. It is motivated by the exiltence of oome conatrainta for which, on one band, forward checking ia not appropriate (the reduction of the search space occura too late In the computation) and lookahead use ia too coatly (in computation time) while, on the other band, It ia pouible to uae .thia constraint for reducing drastically the aearch apace with a small amount of computation. Examplei of aucb conatralnta a" linear equation· and lnequaUone on natural numbere which can be handled by a reaeor1inc about variation Intervale I9J. For lndance, clven

R E (0,1)

E, T E (0,2,3,4,5,6,7,8,9}

we can Infer T = 0 and E E {8,9} Iince 1 ~ R + E + 1 ~ 11 and 10 :S 10 + T :S19 which implle· 10 + T :S 11 and R + E + 1 ~ 10. Such kind of reuonlnc II very lntereeUnc elnce It reduree draeUcally the eearch apace while Induciae almoet no overhead. Since It can happen that not all the lnconeletent value· are removed, they are a epeclal cue of the PLAIR. Theee conetralnu have been applied eucce11fully In &Hu rancinc from crypt-arithmetic to lntecer linear procrammlnc. We now define an Inference rule we call the parUal lookahl'ad Inference rule which Ia of no uee per 11 but provide· a theoreUcal bule for buildlnc In eome particular clue of conetrainU. The LAIR can be eeen u a particular cue of it. h roneieU in replacin1 the point 3 and 5 In the LAIR definition by the followinc two pointe.

1. For each "J' let
2. d1j 2 ( yj E dxj I 3 y 1 E dx1, ... , 3 yj-1 E dxj-1, 3 yj+J E dxj+1, ... , 3 Yn E dxn euch that PR I= P9 with 9 = (x 1 fyl' ... ,x.fyn)) and d1j F ().
3. d1j !;; dxj.

2. Gl+l II ·- (A1, ... ,Am·1'P'Am+1''"'Ak)91+1'

Tile Ht d1j 11 not defined In thl· Inference rule and 11 dependent of each particular con1tralnt. What we have defined II a theoretical framework for ju1tlfyln1 certain kinde of epeclall&atlon. The eoundneaa of the PLAIR can eaally be proved from the eoundne11 of LAIR.

6. Conclusion.

CTa a" a powerful paradl1m for eolvlnc CSPa. While btlnc the bula for aome auc"ce11ful problem·aolven, thla paradlcm hu not been taken Into account durln1 the dealcn of procrammla1 lancuacea. However, there exlaU a Inherent lnternt to build a declarative lancuace bued on thl· paradicm u It lncreuea both nexibility for atatlnc and aolvlnc the problem.

Thla paver hu preaented a theoretical framework for lntecratlnc CT· lnalde loclc procrammlnc. Several new Inference rulea have been defined and their formal propertiea have been proved. Aleo, the lntereat of aome cluaea of computation rule· wrt the expreulv~>ne"' ar1d the efficiency have been atre11ed ir1 thla roatext.

Thll make· lock pro11rammin1 not only a cood lan1Ua1e for atatiDI CSPa but alao an efficient tool for aolvlnc them u confirmed by our firat experlmenu.

Acknowledgeme-nts.

• I cracefully acknowledse many helpful dlscu11ions concernlnc thla reHarch with M. Dincbu, H. Gallaire and H. Simonis. In addiUon, L. Viellle provided a careful criUcism on a fint verelon of thl· paper.