Odgovor set programiranje

S Vikipedije, slobodne enciklopedije

Odgovor set programiranje (OKP) je oblik deklarativnog programiranja orijentisano ka teškim (pre svega NP-teško) pretraživanjem problema. Ona se zasniva na stabilnom modelu (odgovor set) semantičke logike programiranja. U OKPu, problemi pretrage se svode na računarske stabilne modele, a odgovor komplet rešenje - programi za generisanje stabilnih modela se koriste za obavljanje pretrage. Računarski proces zaposlen u dizajnu koji za  mnoge odgovore postavlja rešenje je unapređen u DPLL algoritam i, u principu, uvek se završava (za razliku od Prolog procene upita, što može dovesti do beskonačne petlje).

U opštem smislu, OKP obuhvata sve aplikacije odgovora kompleta predstavljanja znanja i korišćenje[1][2] Prolog stila za procene upita za rešavanje problema koji se javljaju u ovim aplikacijama.

Istorija[uredi | uredi izvor]

Metod planiranja predložen 1993. godine Dimopoulos, Nebel i Kohler[3] je rani primer odgovor set programiranja. Njihov pristup se zasniva na odnosu između planova i stabilnih modela.[4] Soininen i Niemela[5] primenjuje ono što je danas poznato kao odgovor set programa na problem konfiguracije proizvoda. Upotreba odgovora postavljenih rešenja za pretragu je identifikovan kao nova paradigma programiranja od Mareka i Truszczinski u novinama koje su se pojavile u 25-godina perspektive na paradigmu logike programiranja objavljene 1999.[6] godine i u [Niemela 1999].[7] Zaista, nova terminologija "Odgovor komplet" umesto "stabilan model" je prvi predložio Lifschitz[8] u novinama se pojavljuju u istom obimu retrospektivno Marek-Truszczinskovom papiru.

Odgovor set programiranje jezik AnsProlog[uredi | uredi izvor]

Larse je ime programa koji je prvobitno nastao kao uzemljenje alata (front-end) za odgovor postavljenih rešenih smodela. Jezik koji Lparse prihvata se sada obično zove AnsProlog *,[9] skraćeno od odgovora set programiranja u logici.[10] Sada se koristi na isti način i u mnogim drugim odgovor set rešenjima, uključujući assat, kopče, cmodela, gNT, nomore++ i pbmodeli. (dlv je izuzetak, a sintaksa ASP programa napisana za DLV je nešto drugačija.)

AnsProlog program se sastoji od pravila u obliku

<head> :- <body> .

Simbol :- ("ako") je pao ako <тело> je prazna; takva pravila nazivaju činjenice. Najjednostavniji tip Lparse pravila su pravila sa ograničenjima.

Još jedna korisna konstrukcija uključena u tom jeziku je izbor. Na primer, pravilo izbora.

{p,q,r}.

kaže: odaberite proizvoljno koji od atoma p,q,r će se uključiti u stabilan model. Lparse program koji sadrži ovaj izbor pravila i nema drugih pravila ima 8 stabilni modela-proizvoljnih podskupova {p,q,r}. Definicija stabilnog modela je generalizovana na programima sa izborom pravila.[11] Choice pravila mogu se tretirati kao skraćenica za propozicijski formula pod stabilnim modelima semantike.[12] Na primer, izbor pravilo iznad može se posmatrati kao skraćenica za povezanost tri "isključen srednji" formula:

Jezik lparse nam omogućava i da piše "primoravaju" Izbor pravila, kao što su

1{p,q,r}2.

Ovo pravilo kaže: izabrati najmanje 1 od atoma p,q,r, ali ne više od 2. Smisao ovog pravila pod stabilnim modelima semantike se predstavljaju propozicionalnom formulom

Kardinalnost granice se mogu koristiti u telu pravila, kao na primer:

:- 2{p,q,r}.

Dodavanje ovog ograničenja na Lparse program eliminiše stabilne modele koji sadrže najmanje 2 atoma p,q,r. Smisao ovog pravila može biti predstavljen propozicionalnom formulom

Promenljive (VELIKIM SLOVIMA, kao u Prolog) se koristi u Lparse da skrate kolekcije pravila koja slede isti obrazac, kao i da skrate zbirke atoma u istom pravilu. Na primer, Lparse program

p(a). p(b). p(c).
q(X) :- p(X), X!=a.

ima isto značenje kao

p(a). p(b). p(c).
q(b). q(c).

Program

p(a). p(b). p(c).
{q(X):-p(X)}2.

je skraćenica za

p(a). p(b). p(c).
{q(a),q(b),q(c)}2.

niz je oblika:

<Predicate>(start..end)

gde su početak i kraj stalni cenjeni aritmetički izrazi. Raspon je sistem znakova prečica koja se uglavnom koristi za definisanje numeričkih domena u kompatibilnom način. Na primer, činjenica

a(1..3).

je prečica za

a(1). a(2). a(3).

Raspon se takođe može koristiti u organima pravilnika sa istom semantikom.

Uslovno bukvalno ima oblik:

p(X):q(X)

Ukoliko produženje q je {k (a1); k (a2); ...; q (aN)}, gore uslov je semantički ekvivalent pisanju p (a1), p(A2), ..., p(aN) na mestu stanja. Na primer

q(1..2).
a :- 1 {p(X):q(X)}.

je skraćenica za

q(1). q(2).
a :- 1 {p(1), p(2)}.

Stvaranje stabilnih modela[uredi | uredi izvor]

Da biste pronašli stabilan model Lparse programa koji se nalaze u datoteci<имефајла> koristimo komandu

% lparse <filename> | smodels

Opcija 0 nalaže smodelsu da pronađe sve stabilne modele programa. Na primer, ako datoteka testa sadrži pravila

1{p,q,r}2.
s :- not p.

onda komanda

% lparse test | smodels 0

proizvodi izlaz

Одговор: 1
Stable Model: q p Одговор: 2
Stable Model: p Одговор: 3
Stable Model: r p Одговор: 4
Stable Model: q s Одговор: 5
Stable Model: r s Одговор: 6
Stable Model: r q s

Primeri ASP programa[uredi | uredi izvor]

Grafikon bojenja[uredi | uredi izvor]

N-bojenje grafikona G je funkcija boja \ iz svog seta temena do {1,...,n} takva da boje (h) ≠ boje(u) za svaki par susednih temena x, y . Želimo da koristimo ASP da pronađu n-boju datog grafa (ili utvrdi da ne postoji).

Ovo se može ostvariti korišćenjem sledeći program Lparse:

c(1..n).
1 {color(X,I) : c(I)} 1 :- v(X).
:- color(X,I), color(Y,I), e(X,Y), c(I).

Linija 1 definiše brojeve 1,..., n da budu boje. Prema pravilu izbora u liniji 2, jedinstvene boje trebalo bi da bude dodeljen svakom temenu x. Ograničenje u redu 3 zabranjuje dodeljivanje iste boje temenima x i u ako postoji nešto što ih povezuje.

Ako kombinujemo ovu sliku sa definicijom G, kao što su

v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .

i imaju smodels na njemu, sa numeričkim vrednostima n navedenog na komandnoj liniji, onda su atomi oblika boje (...,...) u izlazu smodels će predstavljati n-bojenje .

Program u ovom primeru ilustruje "generiše-i-test" organizaciju koja se često nalazi u jednostavnim ASP programima. Pravilo izbora opisuje skup "mogućih rešenja" - jednostavno nadskup skupa rešenja datog problema pretrage. Nakon toga sledi ograničenje, koje eliminiše sva potencijalna rešenja koja nisu prihvatljiva. Međutim, proces pretraga zaposlen smodels i drugi odgovor postavljenih rešenja se ne zasniva na suđenju i greškama.

Velika klika[uredi | uredi izvor]

Klika u grafu je skup parova susednih temena. Sledeći lparse program pronalazi kliku veličinu ≥ n u datom grafiku, ili utvrdi da ne postoji:

n {in(X) : v(X)}.
:- in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).

Ovo je još jedan primer koji generiše-i-test organizaciju. Pravilo izbora u liniji 1 "stvara" svi skupovi koji se sastoje od ≥ n temena. Ograničenje u liniji 2 "Veeds od" setove koji nisu klike.

Hamiltonijan ciklus[uredi | uredi izvor]

Hamiltonov ciklus u režiji grafika je ciklus koji prolazi kroz svako temene grafika tačno jedanput. Sledeći Lparse program može da se koristi da pronađe Hamiltonov ciklus u datom usmerenom grafiku ako postoji; pretpostavljamo da 0 jedna od temenima.

{in(X,Y)} :- e(X,Y).

:- 2 {in(X,Y) : e(X,Y)}, v(X).
:- 2 {in(X,Y) : e(X,Y)}, v(Y).

r(X) :- in(0,X), v(X).
r(Y) :- r(X), in(X,Y), e(X,Y).

:- not r(X), v(X).

Pravilo izbora u liniji 1 "generiše" sve podskupove skupa ivica. Tri ograničenja "veed out" Podskupovi koje nisu Hamiltonov ciklus. Poslednji od njih koristi pomoćni predikat r(x)("x je dostupan od 0") da zabrani temena koji ne zadovoljavaju ovaj uslov. Ovaj predikat je rekurzivno definisan u redovima 4 i 5.

Ovaj program je primer opštije "generisati, definišu i test" organizacije: uključuje definiciju pomoćnim predikatima koji nam pomaže da eliminišemo sva "loša" potencijalna rešenja.

Zavisnost analize[uredi | uredi izvor]

U obradi prirodnih jezika, zavisnost zasnovana na raščlanjavanju može biti formulisana kao ASP problem.[13] Sledeći kod parsira latinsku rečenicu Puella pulchra in villa linguam latinam discit "lepa devojka uči latinski u vili". Sintaksa drvo je izražena od strane luka predikata koji predstavljaju zavisnost između reči osude. Izračunata struktura je linearno naredno ukorenjeno stablo.

% ********** input sentence **********
word(1, puella). word(2, pulchra). word(3, in). word(4, villa). word(5, linguam). word(6, latinam). word(7, discit).
% ********** lexicon **********
1{ node(X, attr(pulcher, a, fem, nom, sg));
   node(X, attr(pulcher, a, fem, nom, sg)) }1 :- word(X, pulchra).
node(X, attr(latinus, a, fem, acc, sg)) :- word(X, latinam).
1{ node(X, attr(puella, n, fem, nom, sg));
   node(X, attr(puella, n, fem, abl, sg)) }1 :- word(X, puella).
1{ node(X, attr(villa, n, fem, nom, sg));
   node(X, attr(villa, n, fem, abl, sg)) }1 :- word(X, villa).
node(X, attr(linguam, n, fem, acc, sg)) :- word(X, linguam).
node(X, attr(discere, v, pres, 3, sg)) :- word(X, discit).
node(X, attr(in, p)) :- word(X, in).
% ********** syntactic rules **********
0{ arc(X, Y, subj) }1 :- node(X, attr(_, v, _, 3, sg)), node(Y, attr(_, n, _, nom, sg)).
0{ arc(X, Y, dobj) }1 :- node(X, attr(_, v, _, 3, sg)), node(Y, attr(_, n, _, acc, sg)).
0{ arc(X, Y, attr) }1 :- node(X, attr(_, n, Gender, Case, Number)), node(Y, attr(_, a, Gender, Case, Number)).
0{ arc(X, Y, prep) }1 :- node(X, attr(_, p)), node(Y, attr(_, n, _, abl, _)), X < Y.
0{ arc(X, Y, adv) }1 :- node(X, attr(_, v, _, _, _)), node(Y, attr(_, p)), not leaf(Y).
% ********** guaranteeing the treeness of the graph **********
1{ root(X):node(X, _) }1.
:- arc(X, Z, _), arc(Y, Z, _), X != Y.
:- arc(X, Y, L1), arc(X, Y, L2), L1 != L2.
path(X, Y) :- arc(X, Y, _).
path(X, Z) :- arc(X, Y, _), path(Y, Z).
:- path(X, X).
:- root(X), node(Y, _), X != Y, not path(X, Y).
leaf(X) :- node(X, _), not arc(X, _, _).

Poređenje implementacija[uredi | uredi izvor]

Rani sistemi, kao što su Smodels, Polovni odustajanje da pronađu rešenja. Kao teorija i praksi Bulov SAT rešavača razvijao, jedan broj ASP solvers izgrađene su na vrhu SAT rešavača, uključujući Assat i Cmodels. Ovo pretvorena ASP formulu u SAT propozicijama, primenjeno SAT solver, a zatim rešenja konvertuje u ASP formi. Noviji sistemi, kao što su kopča, koristite hibridni pristup, koristeći algoritme sukobom-driven inspirisane SAT, bez puno pretvaranje u Boolean logičkoj-formi. Ovi pristupi omogućavaju značajno poboljšanja performansi, često reda veličine, preko ranije pomacima algoritama.

Potassco projekat deluje kao kišobran za mnoge sisteme ispod, uključujući kopču, uzemljenje sistema (gringo), postepene sisteme (iclingo), ograničenja rešenja (clingcon), akcioni jezik do ASP kompajlera (coala), distribuirani MPI implementacije (claspar) , i mnogi drugi.

Većina sistema podržava varijable, već samo posredno, tako što bi primoralo uzemljenje, pomoću uzemljenja sistema kao što je Lparse ili stranac kao prednji kraj. Potreba za uzemljenje može prouzrokovati eksploziju kombinatornog klauzula; dakle, sistemi koji obavljaju on-the-fli uzemljenje možda ima prednost.

Platforma Funkcija Mehanika
Ime OS Licenca Promenljiva Funkcija simbola Eksplicitni setovi Eksplicitne liste Disjunktivna (izbor pravila) podrška
ASPeRiX Arhivirano na sajtu Wayback Machine (8. novembar 2016) Linux GPL Da Ne uzemljenje u letu
ASSAT Solaris Besplatan softver SAT osnova rešenja
Clasp Answer Set Solver Linux, Mac OS, Windows GPL Da u Clingu Da Ne Ne Da postepeni, SAT rešenje inspirisan (NoGood, konflikt-driven)
Cmodels Linux, Solaris GPL Zahteva uzemljenje Da postepeni, SAT rešenje inspirisan (NoGood, konflikt-driven)
DLV Linux, Mac OS, Windows[14] free for academic and non-commercial educational use, and for non-profit organizations[14] Da Da Ne Ne Da Ne kompatibilan Lpars
DLV-Complex Linux, Mac OS, Windows Freeware Da Da Da Da izgrađen na vrhu DLV - Ne kompatibilan Lpars
GnT Linux GPL Zahteva uzemljenje Da izgrađen na vrhu smodela
nomore++ Linux GPL kombinovani bukvalno + pravilno - osnova
Platypus Linux, Solaris, Windows GPL distribuira, multi-threaded nomore ++ smodels
Pbmodels Linux ? Pseudo-bulovo rešenje na bazi
Smodels Linux, Mac OS, Windows GPL Zahteva uzemljenje Ne Ne Ne Ne
Smodels-cc Arhivirano na sajtu Wayback Machine (15. novembar 2015) Linux ? Zahteva uzemljenje SAT rešenje zasnovano; smodela v / konfliktnim tačkama
Sup Linux ? SAT rešenje na osnovi

Vidi još[uredi | uredi izvor]

Reference[uredi | uredi izvor]

  1. ^ Baral 2003.
  2. ^ Gelfond, Michael (2008). „Answer sets”. Ur.: van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce. Handbook of Knowledge Representation (PDF). Elsevier. str. 285—316. ISBN 978-0-08-055702-1. Arhivirano iz originala 03. 03. 2016. g.  as PDF
  3. ^ Dimopoulos, Y.; Nebel, B.; Köhler, J. (1997). „Encoding planning problems in non-monotonic logic programs”. Ur.: Steel, Sam; Alami, Rachid. Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, France, September 24–26, 1997, Proceedings. Lecture notes in computer science: Lecture notes in artificial intelligence. 1348. Springer. str. 273—285. ISBN 978-3-540-63912-1.  as Postscript
  4. ^ Subrahmanian, V.S.; Zaniolo, C. (1995). „Relating stable models and AI planning domains”. Ur.: Sterling, Leon. Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming. MIT Press. str. 233—247. ISBN 978-0-262-69177-2.  as Postscript
  5. ^ Soininen, T.; Niemelä, I. (1998), Formalizing configuration knowledge using rules with choices (Postscript) (TKO-B142), Laboratory of Information Processing Science, Helsinki University of Technology 
  6. ^ Marek, V.; Truszczyński, M. (1999). „Stable models and an alternative logic programming paradigm”. Ur.: Apt, Krzysztof R. The Logic programming paradigm: a 25-year perspective (PDF). Springer. str. 169—181. ISBN 978-3-540-65463-6. 
  7. ^ Niemelä, I. (1999). „Logic programs with stable model semantics as a constraint programming paradigm” (Postscript,gzipped). Annals of Mathematics and Artificial Intelligence. 25: 241—273. doi:10.1023/A:1018930122475. 
  8. ^ Lifschitz, V. (1999). „Action Languages, Answer Sets, and Planning”.  In Apt 1999, str. 357–374
  9. ^ Crick, Tom (2009). Superoptimisation: Provably Optimal Code Generation using Answer Set Programming (PDF) (Ph.D.). University of Bath. Docket 20352. Arhivirano iz originala (PDF) 4. 3. 2016. g. Pristupljeno 28. 11. 2015. 
  10. ^ Davila, Rogelio. „AnsProlog, an overview”. Arhivirano iz originala (PowerPoint) 08. 12. 2015. g. Pristupljeno 28. 11. 2015. 
  11. ^ Niemelä, I.; Simons, P.; Soinenen, T. (2000). „Stable model semantics of weight constraint rules”. Ur.: Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald. Logic Programming and Nonmonotonic Reasoning: 5th International Conference, LPNMR '99, El Paso, Texas, USA, December 2–4, 1999 Proceedings. Lecture notes in computer science: Lecture notes in artificial intelligence. 1730. Springer. str. 317—331. ISBN 978-3-540-66749-0.  as Postscript
  12. ^ Ferraris, P.; Lifschitz, V. (2005). „Weight constraints as nested expressions” (PDF). Theory and Practice of Logic Programming. 5 (1-2): 45—74. doi:10.1017/S1471068403001923. 
  13. ^ „Dependency parsing”. Arhivirano iz originala 15. 4. 2015. g. Pristupljeno 28. 11. 2015. 
  14. ^ a b „DLV System company page”. DLVSYSTEM s.r.l. Pristupljeno 16. 11. 2011. 

Literatura[uredi | uredi izvor]

Spoljašnje veze[uredi | uredi izvor]