Prinudno logičko programiranje

Prinudno logičko programiranje je oblik prinude programa, u kojem logika programiranja je proširena na koncepte za ograničenje zadovoljstva. Prinudni logički program je logika programa koji sadrži ograničenja u telu klauzula. Primer klauzule uključujući ograničenja je A(X,Y) :- X+Y>0, B(X), C(Y). U ovoj klauzuli, X+Y>0 je ograničenje; A(X,Y), B(X), i C(Y) su literali kao u redovnom logičkom programiranju. Ova klauzula kaže jedan uslov pod kojim je izjava A(X,Y) drži: X+Y je veći od nule i oba B(X) i C(Y) su istinita.

Kao i redovno logičko programiranje, programi se upita o verovatnoći cilja, koji može da sadrži ograničenja pored literala. Dokaz za cilj se sastoji od klauzula čija su zadovoljiva ograničenja i literali koji mogu da koriste i druge klauzule tela. Izvršenje se vrši preko tumača, koji polazi od cilja i rekursivno skenira klauzule pokušavajući da dokaže cilj. Ograničenja sa kojima se susreću tokom ovog pregleda se nalaze u određenim ograničenim prodavnicama. Ako ovaj skup nalazi unsatisfiable, prevodilac se povlači, pokušavajući da iskoriste druge odredbe za dokazivanje cilja. U praksi, zadovoljivosti na ograničenje prodavnici može se proveriti pomoću nepotpunih algoritama, koji ne otkrije uvek nedoslednost.

Pregled

Formalno, prinudni logički programi su kao redovne programske logike, ali tela klauzula mogu da sadrže ograničenja, pored redovnih programskih logičkih literala. Kao primer, X>0 je ograničenje, a uključena je u poslednjoj klauzuli sledećeg prinudnog logičkog programa.

 B(X,1):- X<0.
 B(X,Y):- X=1, Y>0.
 A(X,Y):- X>0, B(X,Y).

Kao u redovnom logičkom programiranju, vrednovanje cilja kao što je A(X,1) zahteva ocenu tela poslednje klauzule sa Y=1. Kao u redovnoj logici programiranja, zauzvrat zahteva dokazivanje samog cilja B(X,1). Za razliku od redovne logike programiranja, takođe zahteva da ograničenje treba da zadovolj: X>0, ograničenje u telu poslednje klauzule (u redovnom logičkom programiranju, X>0 se ne može dokazati, osim ako je X vezan za potpuno prizemljeni rok i izvršenje programa neće uspeti ako to nije slučaj).

Da li će ograničenje biti zadovoljno ne može uvek da se odredi kada ograničenje naiđe. U ovom slučaju, na primer, vrednost X nije određena prilikom vrednovanja zadnje klauzule. Kao rezultat toga, ograničenje X>0 nije zadovoljno ni povređeno u ovom trenutku. Umesto postupanja u proceni B(X,1), a zatim proveravanja da li je rezultiralo vrednosti X kao pozitivne kasnije, prevodilac prodavnice ograničenja X>0, a zatim nastavlja u proceni B(X,1); Na ovaj način, prevodilac može da detektuje kršenje ograničenja X>0 tokom procene B(X,1), i odmah odustane ako je to slučaj, umesto da čekaju procenu B(X,1) da zaključi.

U principu, procena ograničenja logike programa odvija se kao u redovnom logičkom programu, ali ograničenja sa kojima se susreću tokom procene se nalaze u određenoj ograničenoj prodavnici. Kao primer, vrednovnje gola A(X,1) prihodi sa ocenjivanja tela prvog dela rečenice sa Y=1; Ova procena dodaje X>0 za ograničenje prodavnice i traži gol B(X,1) da se dokaže. Dok pokušava da dokaže taj cilj, prva klauzula je primenjiva, ali njegova vrednost dodaje X<0 za ograničenje prodavnice. Ovaj dodatak čini ograničenje prodavnica unsatisfiable, a prevodilac povlači, uklanjanje poslednjeg dodatka od ograničenje prodavnice. Evaluacija druge klauzule dodaje X=1 i Y>0 za ograničenje prodavnice. Pošto je ograničenje prodavnica zadovoljivo i nijedna druga bukvalno nije je ostala da se dokaže, prevodilac prestaje sa rešenjem X=1, Y=1.

Semantika

Semantika ograničenih logičkih programa može da se definiše u smislu virtuelne prevodioce koji održava par G, S tokom izvršenja. Prvi element ovog para se zove trenutni cilj; Drugi element se zove ograničenje prodavnice. Sadašnji cilj sadrži literal prevodioca pokušava da dokaže i može da sadrži i neka ograničenja da pokušava da zadovolji; ograničena prodavnica sadrži sve zadovoljive prepreke prevodioca koje je do sada preuzela.

U početku, trenutni cilj je cilj i ograničena prodavnica je prazna. Prevodilac nastavlja uklanjanjem prvog elementa iz trenutnog cilja i njenom analizom. Detalji ove analize su ispod objašnjeni, ali na kraju ove analize može proizvesti uspešan završetak ili neuspeh. Ova analiza može da podrazumeva rekurzivne pozive i dodavanje novih literale do trenutnog cilja i novog ograničenja za ograničenje prodavnice. Prevodilac se povlači ako je neuspeh generisan. Uspešan prestanak se generiše kada je struja cilj prazna i ograničenje prodavnica zadovoljivo.

Detalji analize bukvalno su skinuti sa ciljem koji sledi. Nakon uklanjanja ovoga bukvalno ispred rešenja, on se proverava da li je ograničenje ili bukvalno. Ako je ograničenje, ona se dodaje ograničenoj prodavnici. Ako je bukvalna, klauzula čija je glava ima isti predikat bukvalno koji je izabran; klauzula je prepisana zamenom svoje promenljive sa novim varijablama (varijable se ne javlja u cilju): rezultat se zove sveža varijanta klauzulom; telo sveže varijante klauzule se zatim stavlja ispred cilja; jednakost svakog argumenta bukvalno sa odgovarajućim jednim od svežeg varijante glave nalazi se u ispred rešenja kao dobra.

Neki provere se vrše tokom tih operacija. Posebno, ograničenje prodavnica proverava doslednost svaki put kada se novo ograničenje dodaje na njega. U principu, kad god je ograničenje prodavnica unsatisfiable algoritam može da odustane. Međutim, provera unsatisfiable na svakom koraku će biti neefikasna. Iz tog razloga, nepotpuna zadovoljivost žetona se može koristiti. U praksi, zadovoljivosti se proveravaju pomoću metode koje pojednostavljuju nametanja radnji, to jest, prepisati ga u ekvivalentne ali jednostavnije obliku za rešavanje. Ove metode ponekad, ali ne uvek dokažu unsatisfiable jednog unsatisfiable ograničenja prodavnica.

Prevodilac je dokazao cilj kada je struja cilja prazna, a ograničenje prodavnica nije otkriveno unsatisfiable. Rezultat izvršenja je trenutni set (simplified) ograničenja. Ovaj skup može da obuhvati ograničenja kao što je X=2 da sila promenljivih na specifičnu vrednost, ali može obuhvatiti ograničenja kao što X>2 da samo vezuju promenljive a da nema posebnu vrednost.

Formalno, semantika prinudne logike programiranja je definisana u smislu izvođenja. Tranzicija je par parova Gol/prodavnica, ističe G, S --> G', S'. Takav par navodi mogućnost odlaska iz stanja G, S u stanje G', S'. Takva tranzicija je moguće u tri moguća slučaja: * елемент G је ограничење C, G' = G\ {C} и S' = S' = S u {C}; Другим речима, ограничење може да се помера са циљем ка ограниченој продавници

* element G bukvalno L(t1,...,tn), postoji klauzula prepisana koristeći nove promenljive, je L(t'1,...,t'n): - B, G' je G sa L(t1,...,t'n) zamenjena t1 = t'1,...,tn = t'n, B, i S' = S; Drugim rečima, bukvalno može biti zamenjeno telo sveže varijante klauzulom koji ima isti predikat u glavi, dodajući telo sveže varijante i gore jednakosti pojmova do cilja

* S i S' ekvivalentni u skladu sa specifičnom ograničenom semantikom Niz prelaza je poreklo. A cilj G može dokazati da li postoji izvođenje iz G,0 u 0, S za neko zadovoljivo ograničenje prodavnica S. Semantika formalizuje moguće evolucije tumača da proizvoljno bira literale u cilju procesa i klauzula da zameni literale. Drugim rečima, cilj dokazan ovom semantikom ako postoji niz izbora literala i klauzula, među mnogim eventualno onih, koji dovode do praznog cilja i zadovoljive prodavnice.

Aktualni prevodioci obrađuju elemente cilja u LIFO red : elementi se dodaju u prednji i obrađuju od napred. Oni takođe biraju klauzulu drugog pravila prema redosledu kojim su pisane, i prepiše ograničenje prodavnici kada je modifikovana.

Treći mogući vid tranzicije je zamena ograničenje prodavnice sa ekvivalentnim jedan. Ovo zamena je ograničena na one koje se obavljaju specifičnim metodama, kao što je ograničenje razmnožavanja. Semantika ograničenja logike programiranja je parametarsko ne samo na vrstu ograničenja koristi, ali i metodi za prepravljanje ograničenja prodavnice. Specifične metode koje se koriste u praksi zamene ograničenja prodavnice sa jednim koji je jednostavnije da reši. Ako je ograničenje prodavnica unsatisfiability, ovo pojednostavljivanje može otkriti ovaj unsatisfiability ponekad, ali ne uvek.

Rezultat procene za cilj protiv ograničene logike programa je definisan ako je cilj dokazan. U ovom slučaju, postoji izvođenje od početnog para na paru, gde je cilj je prazan. Ograničenje prodavnica ovog drugog para smatra se rezultatom procene. To je zato što ograničenje prodavnica sadrži sve prepreke pretpostavlja zadovoljive da dokažu cilj. Drugim rečima, cilj je pokazao za sve promenljive vrednosti koje zadovoljavaju ova ograničenja.

Parovima jednakost u pogledu dva literale često se kompaktno označavaju L(t1,...,tn) = (t'1,...,t'n): ovo je skraćenica za ograničenja t1 = t'1,...,tn = t'n. Zajednička varijanta semantike za ograničenje logičkog programiranja dodaje L(t1,...,tn) = L(t'1,...,t'n) direktno na ograničenje prodavnice radije nego do cilja.

Uslovi i ograničenja

Različite definicije termina se koriste, stvarajući različite vrste prinuda logičkog programiranja: preko drveća, realnih brojeva ili konačnih domena. Neka vrsta ograničenja koja je uvek prisutna je jednakost uslova. Takva ograničenja su neophodna, jer je prevodilac dodaje t1 = t2 do cilja kad god literala P(...t1...) je zamenjen sa telom klauzule sveže varijante čiji je načelnik P(...t2...) .

Stablo uslovi

Ograničenje logike programiranje sa tri termina oponaša redovnu logiku programiranja skladištenja supstitucije kao ograničenja u ograničenoj prodavnici. Pravila su promenljive, konstante, i funkcija simbola koje se primenjuju na drugim terminima. Jedina ograničenja smatraju se jednakosti i nejednakosti između termina. Jednakost je posebno važna, jer ograničenja poput t1 = t2 često generiše prevodioca. Ravnopravnosti ograničenja o uslovima može biti pojednostavljena, koja je rešena, putem ujedinjenja:

Ograničenje t1 = t2 može biti pojednostavljeno ako su oba termina simboli funkcija koje se primenjuju na drugim terminima. Ako su dva simbola funkcija isti i broj subterms je takođe isti, ovo ograničenje može biti zamenjena sa poravnavanjem jednakosti subterms. Ako se uslovi sastoje od simbola različitih funkcija ili istog funktora ali na različitim brojem mandata, ograničenje je unsatisfiable.

Ako je jedan od dva termina promenljiva, jedinu dozvoljenu vrednost promenljive može uzeti drugi termin. Kao rezultat toga, drugi termin može da zameni promenljivu u trenutnom cilju i ograničenje prodavnice, tako praktično uklanja promenljivu iz razmatranja. U konkretnom slučaju jednakosti promenljive sa sobom, ograničenje može biti uklonjeno kao i uvek zadovoljno.

U ovom obliku ograničenje zadovoljstva, promenljive vrednosti su termini.

Reals

Ograničenje logike programiranje sa realnih brojeva koristi prave izraze i termine. Kada ne koriste nikakvu funkciju simboli, termini su izrazi preko realnih brojeva, verovatno uključujući i varijable. U tom slučaju, svaka promenljiva može imati samo realan broj kao vrednost.

Da budemo precizni, termini su izrazi preko promenljivih i realnih konstanti. Jednakost između termina je vrsta ograničenja koja je uvek prisutna, kao prevodilac generiše jednakost uslova tokom izvršenja. Kao primer, ako je prvi literal trenutnog cilj A(X+1) i prevodilac je izabrao klauzulu da je A(Y-1):-Y=1 posle prepravljanja je promenljiva, ograničenja koja se dodaju rezultatu su X+1=Y-1 i Y=1. Pravila pojednostavljenja koja se koristi za funkcije simbola se očigledno ne koriste: X+1=Y-1 nije unsatisfiable samo zato što je prvi izraz izgrađen korišćenjem + a drugi koriste - .

Reals i funkcija simboli mogu da se kombinuju, što je dovelo do termina koji se izržavaju preko realnih brojeva i funkcija simbola koji se primenjuju u drugim terminima. Formalno, varijable i konstante su pravi izrazi, kao i svaki aritmetička operator nad drugim izrazima. Varijable, konstante (zero ariti funkcijom simboli) i izrazi su termini, kao i bilo koji simbol funkcija primenjuje se na kraju. Drugim rečima, termini se grade preko izraza, dok se izrazi grade preko brojeva i varijabli. U ovom slučaju, promenljive se kreću preko realnih brojeva i uslova. Drugim rečima, promenljiva može da pravi broj kao vrednost, dok druga ima termin.

Jednakost dva mandata može biti pojednostavljena primenom pravila za stabla, ako nijedan od ova dva termina nije pravi izraz. Na primer, ako dva termina imaju istu funkciju simbol i broj subterms, njihova ravnopravnost ograničenja može biti zamenjena jednakostima subterms.

Finite domeni

Treća klasa ograničenja koristi se za ograničenje logičkog programiranje koje daje konačan domen. Vrednosti promenljivih su u ovom slučaju uzete iz konačnog domena, često od celih brojeva. Za svaku promenljivu, drugačiji domen može se odrediti X::[1..5], na primer znači da je vrednost X između 1 i 5. domenu promenljive može se dati nabrajajući sve vrednosti promenljive se mogu uzeti; Stoga, deklaracija iznad domena može se takođe napisati X:: [1,2,3,4,5]. Ovaj drugi način navodeći domen omogućava domene koji nisu sastavljeni od celih brojeva, kao što su X:: [George, Mari, John]. Ako domen promenljive nije određen, pretpostavlja se da se skup celih brojeva predstavlja na jeziku. Grupi varijabla može se dati isti domen koristeći deklaraciju kao [X,Y,Z]::[1..5].

Domen promenljive može da se smanji tokom izvršavanja. Zaista, kao prevodilac dodaje ograničenja na ograničenje prodavnice, obavlja nametanja propagiranja da sprovodi neku vrstu lokalne doslednosti, i ove operacije može smanjiti domen varijabli. Ako se domen promenljive isprazni, ograničenje prodavnica je nedosledno, i algoritam se povlači. Ako domen promenljive postaje singl, promenljivoj može biti dodeljena jedinstvena vrednost u svom domenu. Oblici doslednosti obično sprovode se luk doslednosti, hiper-luk doslednosti, i vezanu doslednost. Sadašnji domen promenljive može se razgledati primenom specifičnih literala; Na primer, dom(X,D) sazna trenutni domen D jedne promenljive X.

Što se tiče domena realnih brojeva, funktori mogu koristiti domene celih brojeva. U ovom slučaju, termin može biti izraz preko celih brojeva, konstanta, ili primena funktora nad drugim terminima. Promenljive mogu da uzmu proizvoljan termin kao vrednost, ako njen domen nije naveden da je skup celih brojeva ili konstanti.

Ograničenje prodavnica

Ograničenje prodavnica sadrži zadovoljiva ograničenja koja su trenutno preuzeta. Može se smatrati da je ono trenutna zamena je za redovno logičko programiranje. Kada su dozvoljeni samo drvo uslovi, ograničenje prodavnica sadrži ograničenja u vidu t1=t2; ova ograničenja se pojednostavi ujedinjenja, što je rezultiralo ograničenja oblik promenljiva = rok; takva ograničenja su ekvivalent izmeni.

Međutim, ograničenje prodavnica može da sadrži i ograničenja u vidu t1!=t2, ako su razlike != između termini dozvoljene. Kada su dozvoljeni ograničenja preko realnih brojeva ili konačnih domena, ograničenje prodavnica takođe može da sadrži domen-specifična ograničenja kao što su X+2=Y/2, itd

Ograničenje prodavnica proširuje koncept trenutne zamene na dva načina. Prvo, ona ne sadrži samo ograničenja koja proističu iz izjednačavanja bukvalno sa glavom sveže varijantne klauzule, već i ograničenja tela klauzula. Drugo, ne sadrži samo ograničenja na oblik promenljiva = vrednost, ali i ograničenja posmatranog ograničenju jezika. Iako je rezultat uspešne evaluacije redovna logika programa je konačna supstitucija, rezultat za ograničenje logike programa je konačno ograničenje prodavnica, koje mogu da sadrže ograničenja na oblik promenljive = vrednost, ali u celini može da sadrži proizvoljna ograničenja.

Domain specifična ograničenja mogu doći do ograničenja prodavnica do tela klauzula i do izjednačavanja bukvalno sa klauzulnom glavom: na primer, ako prevodilac prepisuje doslovno A(X+2) sa klauzulom čije sveže varijanta glava A(Y/2), ograničenje X+2=Y/2 dodaje se u ograničenje prodavnice. Ako se promenljiva pojavljuje u stvarnoj ili ograničenom domenu izražavanja, može samo uzeti vrednost u realnim brojevima ili konačnom domenu. Takva promenljiva ne može da uzme termin napravljen od funktora primenjen na drugim terminima kao vrednost. Ograničenje prodavnica je unsatisfiable ako je promenljiva u obavezi da preduzme obe vrednosti specifične oblasti i funktora primenjen na uslove.

Nakon ograničenja se dodaje ograničenje prodavnice, neke operacije se izvode na ograničenje prodavnice. Koji poslovi se obavljaju zavisi performansi domena i ograničenja. Na primer, ujedinjenje se koristi za konačno drveće jednakosti, promenljivo eliminisanje jednačina polinoma preko realnih brojeva, ograničenje širenja kako bi se sproveo neki oblik lokalne doslednosti za konačan domen. Ove operacije su usmerene na donošenje ograničenja prodavnica jednostavnije da se proveri za zadovoljivost i rešenje.

Kao rezultat tih operacija, dodavanje novih ograničenja mogu promeniti stare. Bitno je da prevodilac može da poništi ove promene kada je povlači. Najjednostavniji način je slučaj za prevodioca da spase kompletno stanje u prodavnici svaki put kada pravi izbor (da bira klauzulu da prepravim za cilj). Efikasnijih metoda za dozvoljavajuće ograničenje prodavnica da se vrati u prethodno stanje postoji. Konkretno, samo da sačuvate promene na ograničenje prodavnici postignut između dve tačke izbora, uključujući i promene na starim ograničenja. Ovo se može uraditi jednostavnom uštedom stare vrednosti na ograničenja koja su modifikovana; ovaj metod se naziva zaostaje. Napredniji metod je da sačuvate promene koje su urađeno na modifikovanim ograničenja. Na primer, linearni ograničenje se menja promenom svoju koeficijent: štedi razliku između starog i novog koeficijenta omogućava vraćanje promenu. Ovaj drugi metod se zove semantički povlačenje izjave, jer su semantika promene je prilično sačuvan od stare verzije samo ograničenja.

Označavanje

Označavanje literala se koristi na varijabli preko konačnih domenima da proverite zadovoljivost ili delimičnu zadovoljivost o ograničenju prodavnica i da nađe zadovoljavajući zadatak. Obeležavanje bukvalno ima oblik označavanja ([varijabli]), gde je argument lista varijabli preko konačnih domena. Kad god se prevodilac procenjuje takav bukvalan, obavlja pretragu nad domenom varijabli na listi će naći zadatak da zadovoljava sva relevantna ograničenja. Tipično, to se radi formi povlačenje izjave: promenljive se vrednuju kako, pokušavajući sve moguće vrednosti za svaki od njih, i odustajanje kada se otkrije nedoslednost.

Prva upotreba obeležavanja liberala je da stvarne provere zadovoljivosti ili delimično zadovoljivosti na ograničenje prodavnice. Kada prevodilac dodaje ograničenje za ograničenje prodavnice, on samo sprovodi jedan oblik lokalne doslednosti u tome. Ova operacija ne može detektovati nedoslednost čak i ako je ograničenje prodavnica unsatisfiable. Obeležavanje bukvalno preko skupa varijabli sprovodi proveru zadovoljivosti od ograničenja preko ovih varijabli. Kao rezultat toga, koristeći sve promenljive navedene u rezultatima ograničenje prodavnicu u proveru zadovoljivosti u prodavnici.

Druga upotreba obeležavanja liberala je zapravo da odredi procenu varijabli koje zadovoljava ograničenje prodavnice. Bez etiketiranja liberala, promenljivim se dodeljuju vrednosti samo kada je ograničenje prodavnica sadrži ograničenja oblika X=vrednosti i kada se lokalna doslednost smanjuje domen promenljive na jednoj vrednosti. Obeležavanje bukvalno preko nekih varijabli prisiljava ove promenljive da se procene. Drugim rečima, posle etikete liberal razmatra, sve varijable kojima se dodeljuju vrednosti.

Tipično, ograničenja logičkih programa su napisani na takav način da se obeležavanja literali ocenjuje tek nakon što se više ograničenja mogu akumulirati u ograničenje prodavnice. To je zato što obeležavanja literala sprovode pretragu, a pretraga je efikasnija ako postoje više ograničenja da budu zadovoljni. Problem zadovoljstvo ograničenje je tipično rešenje ograničenja logike programa koji ima sledeću strukturu:

решење(X):-ограничења(X), етикетирање(X)
ограничење(X):- (сва ограничења CSP-а)

Kada prevodilac ocenjuje cilj rešavanja (args), stavlja telo sveže varijante prve klauzule u trenutni cilj. Pošto prvi cilj je ograničenja (X'), druga klauzula se ocenjuje, a ova operacija kreće sve ograničenja u trenutnom cilju i na kraju u ograničenje prodavnice. Bukvalno označavanje (X') se onda procenjuju, zbog čega je potraga za rešenje o ograničenju prodavnice. Pošto ograničenje prodavnica sadrži upravo ograničenja originalnog problema zadovoljstva prepreka, ova operacija traži rešenje prvobitnog problema.

Program reformulations

Dato ograničenje logike programa se može preformulisati da poboljša svoju efikasnost. Prvo pravilo je da obeležavanja literali će biti postavljeno nakon što se više ograničenja na obeleženim literalima akumulira u ograničenje prodavnice. Dok u teoriji A(X):- označavanje (X),X>0 je ekvivalentno A(X):-X>0, označavanje (X), potraga koja se obavlja kada se prevodilac susreće sa etiketiranjem liberala na ograničenje radnja koja ne sadrži ograničenja X>0. Kao rezultat toga, ona može generisati rešenja, kao što su X=-1, koja su kasnije saznali da se ne zadovoljavaju ovim ograničenjima. S druge strane, u drugoj formulaciji se pretres vrši samo kada je ograničenje već u ograničenju prodavnice. Kao rezultat toga, traži se vraća samo rešenja koja su u skladu sa tim, iskoristivši činjenicu da dodatna ograničenja smanjuju prostor za pretragu.

Drugi reformulacija koja može povećati efikasnost je da postavite ograničenja pred reči u telu klauzula. Opet, A(X):-B(X),X>0 i A(X):-X>0,B(X) u principu protivvrednosti. Međutim, prvi može zahtevati više računanja. Na primer, ako je ograničenje prodavnica sadrži ograničenja X<-2, prevodilac rekursivno procenjuje B(X) u prvom slučaju; ako uspe, onda sazna da je ograničenje prodavnica u suprotnosti sa prilikom dodavanja X>0. U drugom slučaju, kada se procenjuje da je klauzula, prevodilac prvi dodaje X>0 za ograničenje prodavnice, a onda eventualno ocenjuje B(X). Od ograničenja prodavnice posle dodavanja X>0 ispostavi se da nisu u skladu, rekuezivna evaluacija B(X) se ne obavlja uopšte.

Treća reformulacija koja može povećati efikasnost je dodatak viška ograničenja. Ako programer zna (bilo kojim sredstvima) da rešenje nekog problema zadovoljava specifičnaa ograničenja, mogu uključiti tu prepreku da izazove nedoslednost o ograničenju prodavnice u najkraćem mogućem roku. Na primer, ako se unapred zna da će procena B(X) rezultirati pozitivnoj vrednosti X, programer može dodati X>0 pre bilo kakve pojave B(X). Kao primer, A(X,Y):-B(X),C(X) neće uspeti na kraju A(-2,Z), ali ovo je saznao tokom evaluacije subgoal B(X). S druge strane, ako je iznad klauzula zamenjena A(X,Y):-X>0,A(X),B(X), prevodilac povlači čim ograničenje X>0 se dodaje u ograničenja prodavnica, koja se dešava pred evaluacijom B(X) i počinje.

Ograničena pravila za rukovanje

Ograničena pravila za rukovanje su prvobitno definisana kao samostalni formalizam za određivanje ograničenja rešenja, a kasnije su ugrađene u logičkom programiranju. Postoje dve vrste prinude pravila rukovanja. Pravila prve vrste navode da, pod određenim uslovima, skup ograničenja je ekvivalentan drugom. Pravila druge vrste navode da, pod određenim uslovima, skup ograničenja podrazumeva još jednu. U jeziku ograničenje logika programiranja podržava ograničenje rukovanja pravila, programer može da koristi ova pravila da precizira mogući rewritings na ograničenje prodavnice i moguće dopune ograničenja prema njemu. U nastavku su primer pravila:

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

Prvo pravilo kaže da, ako B(X) koje podrazumeva prodavnica, ograničenje A(X) može se prepisati kao C(X). Kao primer, N*X>0 možemo zapisati kao X>0, ako prodavnica implicira da N>0. Simbol <=> podseća na jednakost u logici, i kaže da je prvo ograničenje ekvivalentno ovom drugom. U praksi, to znači da će prvo ograničenje biti zamenjeno sa drugom.

Drugo pravilo navodi da je drugo ograničenje posledica prvog, ako je ograničenje u sredini podrazumeva ograničenje prodavnice. Kao rezultat toga, ako je A(X) u ograničenju prodavnice i B(X) podrazumeva ograničenje prodavnice, a zatim se C(X) može dodati prodavnici. Za razliku od slučaja ekvivalencije, ovo je dodatak, a ne zamena: novo ograničenje se dodaje, ali ono staro ostaje.

Ekvivalencija omogućava pojednostavljenje nametanja prodavnice zamenom nekih ograničenja sa nekim jednostavnijim; posebno ako je treće ograničenje u pravilu ekvivalencije istina, a drugo ograničenje je podrazumijevano, prvo ograničenje je uklonjeno iz ograničenja prodavnice. Zaključak omogućava dodavanje novih ograničenja, što može dovesti do dokazivanja nedoslednosti o ograničenju prodavnice, a može generalno smanjiti količinu potrage potrebne da uspostavi svoju zadovoljivosti.

Logika programiranja odredbi u vezi sa ograničenim pravilima za rukovanje može da se koristi za specifikaciju metoda za utvrđivanje zadovoljivosti na ograničenje prodavnice. Različite klauzule se koriste za sprovođenje različitih izbora metoda; ograničeno rukovanje pravila se koriste za korigovanje ograničenja prodavnice tokom izvršenja. Kao primer, može implementirati odustajanje sa jedinicom prostiranja na ovaj način. Neka (L) predstavlja propozicionalnu klauzulu, u kojoj su literali na listi u istom redosledu kao što se ocenjuju. Algoritam može biti implementiran koristeći klauzule za izbor dodeljivanja literala za tačno ili netačno, i ograničenim rukovanjem pravila da odredi širenje. Ova pravila propisuju da ([ l | L ]) se može ukloniti ako je l = istina sledi iz prodavnice, i može se napisati kao ima (L) ako je l lažno sledi iz prodavnice. Slično tome, ([l]) može biti zamenjen sa l = istina. U ovom primeru, izbor vrednosti za promenljivu je realizovan korišćenjem klauzule logičko programiranje; međutim, može se kodirani u ograničenim pravilima rukovanja koristeći produžno nazovi disjunktivno ograničenje rukovanja pravila ili CHR^∨.

Odozdo prema gore evaluacija

Standardna strategija evaluacije logičkih programa je odozgo nadole i dubine prvog: od gola, jedan broj odredaba su identifikovane kao moguće za dokazivanje cilja, a rekurzija nad literalima njihovih tela se vrši. Alternativa strategija je da počnu od činjenica i koriste klauzule za izvođenje novih činjenica; Ova strategija se zove odozdo prema gore. Smatra se bolje od one od vrha nadole kada je cilj da proizvede sve posledice datog programa, umesto dokazivanja gola. Posebno, pronalaženje posledice programa u standardnoj odozgo nadole i dubine prvog načina ne može se prekinuti dok odozdo nagore strategija za vrednovanje ne prestane.

Strategija evaluacije odozdo nagore održava skup činjenica koje smo pokazali do sada tokom evaluacije. Ovaj set je inicijalno prazan. Sa svakim korakom, nove činjenice su izvedene primenom programa klauzula u postojećim činjenicama, i dodaju u skup. Na primer, procena odozdo prema gore od sledećeg programa zahteva dva koraka:

A(q).
B(X):-A(X).

Skup posledica je inicijalno prazan. Na prvom koraku A(q) je jedina klauzula čije se telo može dokazati (jer je prazna), i A(q) se stoga dodaje u trenutni skup posledica. Na drugom koraku, pošto je A(q) dokazano, druga klauzula može koristiti i B(q) koje je dodato u posledicama. Pošto nijedna druga posledica se ne može dokazati iz {A(q),B(q)}, izvršenje prestaje.

Prednost evaluacije odozdo prema gore preko odozgo nadole je da ciklus izvođenja ne proizvode beskonačnu petlju. To je zato što dodavanje posledica trenutan skup posledica koji već sadrži nema efekta. Kao primer, dodavanje treće klauzule da gore program generiše ciklus izvođenja u evaluaciji odozgo nadole:

A(q).
B(X):-A(X).
A(X):-B(X).

Na primer, dok ocenjivanje svih odgovora do cilja A(X), odozgo nadole strategija će proizvoditi sljedeća izvođenja:

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

Drugim rečima, jedina posledica A(q) je proizvedena prva, ali onda algoritam ciklusa tokom izvođenja ne proizvodi bilo koji drugi odgovor.

Strategija odozdo prema gore nema isti nedostatak, kao i posledice koje su već izvedene i nemaju efekta. Na gore program, strategija odozdo prema gore počinje dodajući A(q) na skupu posledica; u drugom koraku, B(X):-A(X) se koristi za izvođenje B(q); u trećem koraku, jedine činjenice koje se mogu izvesti iz tekućih posledica su A(q) i B(q), koji su međutim, već u skupu posledica. Kao rezultat toga, algoritam se zaustavlja.

U gornjem primeru, koriste se samo činjenice iz podzemnih literala. Generalno, svaka klauzula koja sadrži samo ograničenja u telu smatra se činjenicom. Na primer, klauzula A(X):-X>0,X<10 smatra činjenicu kao dobrom. Za ove produžene definicije činjenica, neke činjenice mogu biti ekvivalent dok ne sintaksičeski jednake. Na primer, A(q) je ekvivalentno A(X):-X=q i oba su ekvivalentna A(X):-X=Y, Y=q. Da bi se rešio ovaj problem, činjenice su prevedene na normalnu formu u kojoj glava sadrži tuple svih-različitih varijabli; dve činjenice su onda ekvivalentne ako su njihova tela ekvivalentna na varijabli glave, to jest, njihovi setovi rešenja su isti kada su ograničeni na ove varijable.

Kao što je opisano, odozgo prema gore pristup ima prednost ne uzimajući u obzir posledice koje su već izvedene. Međutim, još uvek možemo izvući posledice koje su podrazumevale one koje su već izvedene dok ne bude jednak bilo koji od njih. Kao primer, procena odozdo prema gore od sledećih programa je beskonačan:

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

Odozdo prema gore evaluacioni algoritam prvo proizlazi da je A(X) istinit za =0 i X>0. U drugom koraku, prva činjenica sa trećom klauzulom omogućava izvođenje A(1). U trećem koraku A(2) je izvedena, itd Međutim, ove činjenice su se već podrazumevale činjenicom da je A(X) istinit za bilo nenegativan X. Ovaj nedostatak može da se prevaziđe tako što će se entailment činjenice dodati u trenutan skup posledica. Ako je nova posledica već podrazumevala skup, nije dodat na njega. Od činjenice se čuvaju kao klauzule, eventualno sa "lokalnim promenljivima", entailment je ograničen zbog varijabli njihovih glava.

Uporedno prinudno logičko programiranje

Istovremene verzije prinudnog logičkog programiranja nemaju za cilj programiranje istovremenih procesa, nego rešavanja problema ograničenja zadovoljstva. Ciljevi u prinudnom logičkom programiranju se istovremeno procenjuju; istovremena procena je stoga programirana kao procena cilja od strane prevodioca.

Sintaktički, istovremeno prinudno logičko programiranje je slično ne-istovremenim programima, jedini izuzetak je da odredbe uključuju čuvara, koji su ograničenja koja mogu da blokiraju primenu klauzule pod određenim uslovima. Semantički istovremeno ograničenje logike programiranja razlikuje se od svojih ne-istovremenih verzija jer evaluacija cilja nema za cilj da ostvari istovremeno proces nego nalaženje rešenja za problem. Pre svega, ta razlika utiče na to kako se prevodilac ponaša kada se više od jedne klauzule primenjuje: ne istovremeno ograničenje logike programiranja rekursivno bira sve klauzule; istovremeno ograničenje logike programiranja bira samo jednu. Ovo je najočigledniji efekat namenjen na usmerenje prevodioca, koji nikada nije revidirao izbor od ranije uzet. Ostali efekti su semantička mogućnost da se cilj ne može dokazati, dok evaluacija ne padne, i na poseban način za izjednačavanje cilja i klauzula glavu.

Aplikacije

Ograničenje logike programiranja je primenjeno na mnogim poljima, poput građevinarstva, mašinstva, digitalne verifikacije kola, automatizovanje rasporeda, kontrola vazdušnog saobraćaja, finansija, i drugih.

Istorija

Ograničenje logike programiranja uveli su Jaffar i Lassez u 1987. Oni su generalizovali zapažanje da je termin jednačine i disequations Prolog II. specifičan oblik ograničenja, i generalizovanje ove ideje proizvoljnom ograničenom jeziku. Prve implementacije ovog koncepta su Prolog III, CLP(R), i CHIP.

Vidi još

Literatura

Dechter, Rina (2003). Constraint processing. Morgan Kaufmann. ISBN 978-1-55860-890-0.
Apt, Krzysztof (2003). Principles of constraint programming. Cambridge University Press. ISBN 978-0-521-82583-2.
Marriott, Kim; Stuckey, Peter J. (1998). Programming with constraints: An introduction. MIT Press. ISBN 978-0-262-13341-8.
Frühwirth, Thom; Abdennadher, Slim (2003). Essentials of constraint programming. Springer. ISBN 978-3-540-67623-2.
Jaffar, Joxan; Maher, Michael J. (1994). „Constraint logic programming: a survey”. Journal of logic programming. 19/20: 503—581. doi:10.1016/0743-1066(94)90033-7.
Colmerauer, Alain (1987). „Opening the Prolog III Universe”. Byte. August.