Programarea setului de răspunsuri

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 14 octombrie 2020; verificările necesită 9 modificări .

Programarea setului de răspunsuri (ASP ) este o  formă de programare declarativă axată pe probleme de căutare complexe (în mare parte NP-hard ) bazate pe proprietățile semanticii de programare logică stabilă . Sarcina căutării este calculul unui model stabil și seturi de solutori ( în engleză answer set solvers ) - programe pentru generarea de modele stabile care sunt utilizate pentru căutare. Procesul de calcul inclus în construcția unui set de rezolvatori este un superset al unui algoritm DPLL care este întotdeauna finit (spre deosebire de evaluarea interogării din Prolog , care poate duce la o buclă infinită).  

Mai general, tehnica include toate aplicațiile din seturile de răspunsuri de reprezentare a cunoștințelor [1] [2] și utilizează evaluări de interogare în stil Prolog pentru a rezolva problemele care apar în acele seturi de răspunsuri.

Istorie

Metoda de planificare , propusă în 1993 de Dimopoulos, Nebel și Köhler, este un exemplu timpuriu de programare a seturilor de răspuns. Abordarea lor se bazează pe relația dintre planuri și modele stabile. Soininen și Niemelä au aplicat ceea ce este acum cunoscut sub numele de programare bazată pe răspuns la problema configurației produsului. Utilizarea seturilor de decizie pentru căutare a fost identificată ca o nouă paradigmă de programare de către Marek și Truszczynski într-o lucrare care a apărut într-o perspectivă de 25 de ani asupra paradigmei de programare logică publicată în 1999 și în [Niemelä 1999]. Într-adevăr, noua terminologie de „set de răspuns” în loc de „model stabil” a fost propusă pentru prima dată de Lifshitz într-un articol publicat în același volum retrospectiv ca și articolul lui Marek-Trushchinsky.

AnsProlog

Lparse este un program care a fost creat inițial ca un instrument pentru generarea de propoziții de bază de bază ( eng. Symbol grounding problem ) pentru calcularea modelelor de propoziții logice. AnsProlog este limbajul folosit de Lparse, folosit atât de Lparse, cât și de soluții precum assat, clasp, cmodels], gNt, nomore++ și pbmodels.  

Un program AnsProlog este compus din reguli de forma:

< cap > :- < corp > .

Caracterul :-("dacă") este eliminat dacă este <body>gol; astfel de reguli se numesc fapte . Cel mai simplu tip de reguli Lparse sunt reguli constrânse .

Un alt construct util este select . De exemplu, regula:

{ p , q , r }.

înseamnă: alegeți aleatoriu pe care dintre atomi să includeți în modelul stabil. Un program lparse care conține această regulă și nicio altă regulă are 8 modele stabile de subseturi . Definiția modelelor stabile a fost limitată la programe cu alegerea regulilor [2] . Selectarea regulilor poate fi folosită și pentru a scurta formulele logice.

De exemplu, regula de alegere poate fi considerată ca o prescurtare pentru colecția de trei formule „ excluse mijloc ” :

Limbajul lparse ne permite să scriem „constrângeri” asupra regulilor de selecție, cum ar fi

1 { p , q , r } 2.

Această regulă spune: alegeți cel puțin unul dintre atomi, dar nu mai mult de doi. Regula poate fi reprezentată ca o formulă logică:

Limitele stabilite pot fi folosite și ca constrângere, de exemplu:

:- 2 { p , q , r }.

Adăugarea acestei constrângeri la programul Lparse elimină modelele stabile care conțin mai puțin de doi atomi. Regula poate fi reprezentată ca o formulă logică:

.

Variabilele (în majuscule, ca în limbajul Prolog ), sunt folosite în Lparse pentru a scurta colecții de reguli. De exemplu, programul Lparse:

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

are acelasi sens ca:

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

Program:

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

Aceasta este o versiune prescurtată:

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

Gama arată astfel:

< Predicat > ( început .. sfârșit )

unde începutul și sfârșitul sunt valori aritmetice constante. Intervalul este o abreviere folosită în principal pentru a se referi la valori numerice într-un mod de grup.

De exemplu fapt:

a ( 1..3 ).

Aceasta este o versiune prescurtată:

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

Intervalele pot fi, de asemenea, utilizate în reguli cu următoarea semantică:

p ( X ) : q ( X )

Dacă extensia q є {q(a1); q(a2); … ; q(aN)}, atunci expresia de mai sus este echivalentă semantic cu scrierea: p(a1), p(a2), … , p(aN).

De exemplu:

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

Aceasta este o versiune prescurtată:

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

Generarea de modele stabile

Pentru a găsi un model stabil într-un program Lparse care este stocat într-un fișier ${filename}, utilizați comanda

% lparse ${ nume de fișier } | smodele

Parametrul 0 face ca modelele să găsească toate modelele stabile în program. De exemplu, dacă fișierul testconține reguli:

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

atunci comanda va emite:

% lparse test | smodels 0 Răspuns: 1 Model Stabil: qp Răspuns: 2 Model Stabil: p Răspuns: 3 Model Stabil: rp Răspuns: 4 Model Stabil: qs Răspuns: 5 Model Stabil: rs Răspuns: 6 Model Stabil: rqs

Exemple de programe ASP

Grafic de colorat

n -colorarea unui grafic  este o funcție astfel încât pentru fiecare pereche de vârfuri adiacente . Am dori să folosim ASP pentru a găsi -colorarea unui grafic dat (sau a determina că acesta nu există).

Acest lucru se poate face cu următorul program Lparse:

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

Prima linie definește numerele de culoare. În funcție de alegerea regulilor din linia 2, fiecare vârf trebuie să fie atribuită o culoare unică . Constrângerea de pe linia 3 interzice alocarea aceleiași culori unui vârf și , dacă există o muchie care le conectează.

Dacă combinați acest fișier cu o definiție precum:

v ( 1..100 ). % 1,...,100 de vârfuri e ( 1 , 55 ). % există o margine între 1 şi 55 . . .

și rulați smodels pe el, cu valoarea numerică specificată pe linia de comandă, apoi atomii de formă din datele originale smodels vor fi -coloring .

Programul din acest exemplu ilustrează organizarea „generare și testare” care se găsește adesea în programele ASP simple. Regula alegerii descrie un set de „soluții potențiale”. Apoi vine o constrângere care exclude toate soluțiile posibile care nu sunt acceptabile. Cu toate acestea, procesul de căutare în sine, care acceptă modele și alte seturi de soluții, nu se bazează pe încercare și eroare .

Problema clicei

O clică într-un grafic este un set de vârfuri adiacente în perechi. Următorul program lparse găsește o clică de dimensiune într-un grafic dat sau determină că nu există:

n { în ( X ) : v ( X )}. :- în ( X ), în ( Y ), v ( X ), v ( Y ), X ! = Y , nu e ( X , Y ), nu e ( Y , X ).

Acesta este un alt exemplu de organizație de generare și testare. Alegerea regulilor din linia 1 „creează” toate seturile formate din vârfuri . Restricțiile din linia 2 „elimină” acele seturi care nu sunt clicuri.

Ciclul Hamilton

Un ciclu hamiltonian într-un grafic direcționat este un ciclu care trece prin fiecare vârf al graficului exact o dată. Următorul program lparse poate fi folosit pentru a găsi un ciclu hamiltonian într-un grafic direcționat dat, dacă există unul; 0 se presupune a fi unul dintre vârfurile:

{ în ( X , Y )} :- e ( X , Y ). :- 2 { în ( X , Y ) : e ( X , Y )}, v ( X ). :- 2 { în ( X , Y ) : e ( X , Y )}, v ( Y ). r ( X ) :- în ( 0 , X ), v ( X ). r ( Y ) :- r ( X ), în ( X , Y ), e ( X , Y ). :- nu r ( X ), v ( X ).

Regula de selecție din linia 1 „creează” toate subseturile setului de margini. Trei restricții „elimină” acele submulțimi care nu sunt cicluri hamiltoniene . Ultimul dintre acestea folosește un predicat auxiliar (" accesibil de la 0") pentru a interzice vârfurile care nu îndeplinesc această condiție. Acest predicat este definit recursiv în rândurile 4 și 5.

Analizare

Procesarea și analiza limbajului natural poate fi formulată ca o problemă ASP [3] . Următorul cod analizează expresia latină Puella pulchra in villa linguam latinam discit  - „o fată frumoasă învață latină la țară”. Arborele de sintaxă este exprimat prin predicate arc , care denotă dependențe între cuvintele dintr-o propoziție. Structura calculată este un arbore ordonat liniar.

% ********** introducere propoziție ********** cuvânt ( 1 , puella ). cuvânt ( 2 , pulchra ). cuvânt ( 3 , în ). cuvânt ( 4 , vilă ). cuvânt ( 5 , linguam ). cuvânt ( 6 , latinam ). cuvânt ( 7 , disc ). % ********** lexicon ********** 1 { nod ( X , attr ( pulcher , a , fem , nom , sg )); node ( X , attr ( pulcher , a , fem , nom , sg )) } 1 :- cuvânt ( X , pulchra ). nod ( X , attr ( latinus , a , fem , acc , sg )) :- cuvânt ( X , latinam ). 1 { nod ( X , attr ( puella , n , fem , nom , sg )); nod ( X , attr ( puella , n , fem , abl , sg )) } 1 :- cuvânt ( X , puella ). 1 { nod ( X , attr ( vila , n , fem , nom , sg )); nod ( X , attr ( vila , n , fem , abl , sg )) } 1 :- cuvânt ( X , vila ). nod ( X , attr ( linguam , n , fem , acc , sg )) :- cuvânt ( X , linguam ). nod ( X , attr ( discere , v , pres , 3 , sg )) :- cuvânt ( X , discit ). nod ( X , attr ( în , p )) :- cuvânt ( X , în ). % ********** reguli sintactice ********** 0 { arc ( X , Y , subj ) } 1 :- nod ( X , attr ( _ , v , _ , 3 ) , sg )), nod ( Y , attr ( _ , n , _ , nom , sg )). 0 { arc ( X , Y , dobj ) } 1 :- nod ( X , attr ( _ , v , _ , 3 , sg )), nod ( Y , attr ( _ , n , _ , acc , sg )). 0 { arc ( X , Y , attr ) } 1 :- nod ( X , attr ( _ , n , Sex , Case , Number )), nod ( Y , attr ( _ , a , Gender , Case , Number )). 0 { arc ( X , Y , prep ) } 1 :- nod ( X , attr ( _ , p )), nod ( Y , attr ( _ , n , _ , abl , _ )), X < Y . 0 { arc ( X , Y , adv ) } 1 :- nod ( X , attr ( _ , v , _ , _ , _ )), nod ( Y , attr ( _ , p )), nu frunză ( Y ). % ********** care garantează arboreitatea graficului ********** 1 { rădăcină ( X ) : nod ( X , _ ) } 1. :- arc ( X , Z ) , _ ), arc ( Y , Z , _ ), X ! = Y . :- arc ( X , Y , L1 ), arc ( X , Y , L2 ), L1 ! = L2 . calea ( X , Y ) :- arc ( X , Y , _ ). cale ( X , Z ) :- arc ( X , Y , _ ), cale ( Y , Z ). :- cale ( X , X ). :- rădăcină ( X ), nod ( Y , _ ), X ! = Y , nu calea ( X , Y ). frunză ( X ) :- nod ( X , _ ), nu arc ( X , _ , _ ).

Comparația implementărilor

Sistemele timpurii precum Smodels foloseau backtracking pentru a găsi o soluție. Odată cu dezvoltarea teoriei și practicii în problemele de satisfacție a formulelor booleene (rezolvatori boolean SAT), numărul de rezolvatori ASP proiectați pe baza solutorilor SAT, inclusiv ASSAT și Cmodels, a crescut. Au transformat formula ASP într-o propoziție SAT, au aplicat soluția SAT și apoi au transformat soluția înapoi în forme ASP. Sistemele mai moderne, cum ar fi Clasp, adoptă o abordare hibridă, folosind algoritmi conflictuali, fără a fi convertite complet într-o formă de logică booleană. Aceste abordări permit îmbunătățiri semnificative ale performanței, adesea cu un ordin de mărime mai bune decât metodele anterioare de backtracking.

Proiectul Potassco rulează pe mai multe sisteme de nivel scăzut, inclusiv închizătoare, sistemul de fixare gringo și altele.

Majoritatea sistemelor suportă variabile, nu direct, ci prin transformarea codului cu sisteme precum Lparse sau gringo. Necesitatea justificării imediate poate provoca o explozie combinatorie; astfel, sistemele care efectuează justificarea din mers pot avea un avantaj.

Platformă Particularități Mecanica
Nume Sistem de operare Licență Variabile Simboluri de funcții Seturi explicite Liste explicite Reguli de selecție
ASPERIX [4] linux GPL da Nu justificare din mers
ASSAT [5] Solaris Gratuit bazat pe solutorul SAT
Rezolvare set de răspunsuri închizătoare [6] Linux , macOS , Windows GPL da da Nu Nu da bazat pe solutorul SAT
modele [7] Linux , Solaris GPL Necesită justificare da bazat pe solutorul SAT
DLV Linux , macOS , Windows [8] Gratuit pentru uz academic și non-comercial da da Nu nr da nu este compatibil cu Lparse
Complex DLV [9] Linux , macOS , Windows GPL da da da da bazat pe DLV  - incompatibil cu Lparse
GNT [10] linux GPL Necesită justificare da pe baza modelelor
nomore++ [11] linux GPL combinate
Platypus [12] Linux , Solaris , Windows GPL distribuite
Pbmodels [13] linux ? bazat pe rezolvatorul pseudoboolean
Modele [14] Linux , macOS , Windows GPL Necesită justificare Nu Nu Nu Nu
Smodels-cc [15] linux ? Necesită justificare bazat pe solutorul SAT
Sup [16] linux ? bazat pe solutorul SAT

Note

  1. ↑ Ferraris, P.; Lifschitz, V. Constrângeri de greutate ca expresii imbricate  (neopr.)  // Teoria și practica programării logice. - 2005. - ianuarie ( vol. 5 , nr. 1-2 ). - S. 45-74 . - doi : 10.1017/S1471068403001923 . ca Postscript Arhivat pe 22 septembrie 2017 la Wayback Machine
  2. ↑ 1 2 Niemelä, I.; Simons, P.; Soinenen, T. Stable model semantics of weight constraint rules // Logic Programming and Nonmonotonic Reasoning: 5th International Conference, LPNMR '99, El Paso, Texas, USA, December 2–4, 1999 Proceedings  (English) / Gelfond, Michael; Leone, Nicole; Pfeiffer, Gerald. - Springer, 2000. - Vol. 1730. - P. 317-331. - (Note de curs în informatică: Note de curs în inteligența artificială). — ISBN 978-3-540-66749-0 . ca Postscript Arhivat la 15 octombrie 2008 la Wayback Machine
  3. ↑ Analizarea dependențelor (downlink) . Consultat la 6 aprilie 2018. Arhivat din original pe 15 aprilie 2015. 
  4. ↑ ASPeRiX . Preluat la 6 aprilie 2018. Arhivat din original la 8 noiembrie 2016.
  5. ↑ >ASSAT: Răspuns setat de solutorii SAT
  6. ↑ clasp: un rezolvator ASP . Consultat la 6 aprilie 2018. Arhivat din original la 16 noiembrie 2018.
  7. ↑ CMODELS - Sistem de programare Answer Set . Consultat la 6 aprilie 2018. Arhivat din original la 2 decembrie 2005.
  8. ↑ Pagina companiei DLV System . DLVSYSTEM srl. Consultat la 16 noiembrie 2011. Arhivat din original pe 2 ianuarie 2012.
  9. ↑ dlv-complex—dlv-complex . Preluat la 6 aprilie 2018. Arhivat din original la 1 iulie 2017.
  10. ↑ TCS - Software - lpeq . Preluat la 6 aprilie 2018. Arhivat din original la 25 decembrie 2017.
  11. ↑ nomore: un Solver pentru programe logice . Preluat la 6 aprilie 2018. Arhivat din original la 4 februarie 2019.
  12. ↑ platypus: o platformă pentru programarea setului de răspunsuri distribuite . Preluat la 6 aprilie 2018. Arhivat din original la 8 aprilie 2018.
  13. ↑ Sursa . Preluat la 6 aprilie 2018. Arhivat din original la 7 martie 2017.
  14. ↑ Calcularea semanticii modelului stabil . Preluat la 6 aprilie 2018. Arhivat din original la 24 martie 2018.
  15. ↑ Models_cc . Preluat la 6 aprilie 2018. Arhivat din original la 15 noiembrie 2015.
  16. ↑ SUP - Sistem de programare Answer Set . Preluat la 6 aprilie 2018. Arhivat din original la 30 martie 2018.

Link -uri

  Accesați articolul Wikidata  Dicționare și enciclopedii