Програмування наборами відповідей: відмінності між версіями
Створено шляхом перекладу сторінки «Answer set programming» |
(Немає відмінностей)
|
Версія за 18:30, 18 грудня 2016
Програмування наборами відповідей (ASP)- це форма декларативного програмування , орієнтованого на складні (насамперед NP-складні) пошуки проблем. Він заснований на стійкій моделі (наборі) семантики логічного програмування. В ASP, пошук проблеми зводиться до обчислювальних стабільних моделей, і наборів вирішувачів (answer set solvers) — програми для створення стабільних моделей—використовуються, щоб виконувати пошук. Обчислювальний процес, включений в конструкцію набору вирішувачів (answer set solvers) - є посиленням DPLL алгоритму і, в принципі, він завжди закінчується (на відміну від запиту оцінки в Prolog, що може призвести до нескінченного циклу).
В більш загальному сенсі, ASP включає всі додатки з наборів відповідей для представлення знань[1][2] та використання Пролог-запиту типу оцінки для вирішення проблем, що виникають у цих додатках.
History
Мова програмування наборів відповідей AnsProlog
Lparse - це назва програми, яка спочатку була створена в якості інструменту (front-end) заземлення для наборів вирішувачів smodels. Мова, яку приймає Lparse зараз зазвичай називають AnsProlog.[3] на сьогоднішній день використовується так само в багатьох інших наборів вирішувачів, в тому числі assat, clasp, cmodels, gNt, nomore++ і pbmodels.
Програма на AnsProlog складається з правил вигляду
<head> :- <body> .
Символ :- ("if") видаляється, якщо <body> порожній; такі правила називають факти. Найпростіший вид Lparse правил є правила з обмеженнями.
Ще одна корисна конструкція цієї мови - вибір. Наприклад, правило вибір
{p,q,r}.
каже: вибрати довільно, який з атомів включити до стабільної моделі. У lparse програмі, яка містить це правило вибір і ніяких інших правил має 8 стабільних моделей—довільні підмножини . Визначення стабільних модель було узагальнено до програм з вибором правил.[4] Вибір правил може розглядатися також як абревіатури для пропозициональных формул при стабільній моделі семантики.[5] Наприклад, правило вибір вище можна розглядати як скорочення для сукупності трьох формул "виключеного третього":
Мова lparse дозволяє нам писати "обмеження" правил вибору, такі як
1{p,q,r}2.
Це правило говорить: вибрати принаймні 1 з атомів , але не більше 2. Сенс цього правила в рамках стійкої моделі семантики є пропозиційною формулою
Cardinality bounds можуть бути використані в тілі правила, наприклад:
:- 2{p,q,r}.
Додавання цього обмеження в програмі Lparse усуває стійкі моделі, які містять щонайменше 2 атомів . Сенс цього правила може бути представлений у вигляді пропозиційної формули
Змінні (великі літери, як і в Пролозі) використовуються в Lparse для скорочування колекціъ правил, які дотримуються тієї ж схемі, а також скоротити колекцій атомів в одне і те ж правило. Наприклад, Lparse програма
p(a). p(b). p(c).
q(X) :- p(X), X!=a.
має таке ж значення, як
p(a). p(b). p(c).
q(b). q(c).
Програма
p(a). p(b). p(c).
{q(X):-p(X)}2.
це скорочення
p(a). p(b). p(c).
{q(a),q(b),q(c)}2.
Діапазон має вигляд:
<Predicate>(start..end)
де початок і кінець є константними арифметичними виразами зі значенням. Діапазон - умовне скорочення, яке використовується в основному для визначення числових доменів сумісним способом. Наприклад, той факт,
це скорочення
a(1). a(2). a(3).
Діапазони також можуть бути використані в тілі правила з тією ж семантикою. Умовний текст має вигляд:
p(X):q(X)
Якщо розширення q є {q(a1); q(a2); ... ; q(aN)}, то вищевказана умова семантично еквівалентна запису p(a1), p(a2), ... , p(aN) на місці умови. Наприклад
q(1..2).
a :- 1 {p(X):q(X)}.
це скорочення для
q(1). q(2).
a :- 1 {p(1), p(2)}.
Створення стійких моделей
Щоб знайти стійку модель Lparse програми, що зберігається у файлі ${filename} ми використовуємо команду
% lparse ${filename} | smodels
Параметр 0 вказує smodels знайти всі стійкі моделі програми. Наприклад, якщо файл test містить правила
1{p,q,r}2.
s :- not p.
тоді команда покаже вивід
% lparse test | smodels 0
Answer: 1
Stable Model: q p
Answer: 2
Stable Model: p
Answer: 3
Stable Model: r p
Answer: 4
Stable Model: q s
Answer: 5
Stable Model: r s
Answer: 6
Stable Model: r q s
Приклади програм ASP
Фарбування графа
-колір на графі функція така, що для кожної пари суміжних вершин . Ми хотіли б використовувати ASP знайти -кольорів даного графа (або визначити, що його не існує).
Це можна зробити за допомогою наступної програми Lparse:
c(1..n).
1 {color(X,I) : c(I)} 1 :- v(X).
:- color(X,I), color(Y,I), e(X,Y), c(I).
1 рядок визначає номери кольорів. В залежності від вибору правил у рядку 2, унікальний колір повиннен бути призначений для кожної вершини . Обмеження у рядку 3 забороняє призначати один і той же колір до вершини і якщо існує ребро, що з'єднує їх. Якщо поєднати цей файл з визначенням таким як
v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .
і запустити smodels на ньому, з числовим значенням зазначеним в командному рядку, потім атоми форми у вихідних даних smodels буде представляти собою -колір .
Програма в цьому прикладі ілюструє "generate-and-test" організацію, яка часто зустрічається в простих ASP програмах. Правило вибір описує набір "потенційних рішень" — простий набір рішень для даного пошуку проблеми. Потім слідуэ обмеження, яке виключає всі можливі рішення, які не прийнятні. Однак, сам процес пошуку, який вживаэ smodels і інші набори вирышувачів не основані на методі проб і помилок.
Велика кліка
Клікою в графі називають набір попарно суміжних вершин. Наступна lparse програма знаходить кліку розміру в даному графі, або визначає, що вона не існує:
n {in(X) : v(X)}.
:- in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).
Це ще один приклад generate-and-test organization. Вибір правил у рядку 1 "створює" всі набори, що складаються з вершин . Обмеження у рядку 2 "відсіває" ті набори, які не є кліками.
Гамільтонів цикл
Гамільтонів цикл в орієнтованому графі є цикл , який проходить через кожну вершину графа рівно один раз. Наступна Lparse програма може бути використана для пошуку Гамільтонівського циклу в заданому орієнтованому графі, якщо він існує; ми припускаємо, що 0-це одна з вершин.
{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).
Правило вибору в рядку 1 "створює" всі підмножини набору ребер. Три обмеження "відсіюють" ті підмножини, які не є Гамільтонівськими циклами. Останній з них використовує допоміжний предикат (" is reachable from 0"), щоб заборонити вершини, які не задовільняють цій умові. Цей предикат визначається рекурсивно в рядках 4 та 5.
Ця програма є прикладом більш загального "generate, define and test" організування: це включає в себе визначення допоміжного предиката, який допомагає нам усунути все "погане" у потенційному рішені.
Синтаксичний аналіз
Обробка природної мови, синтаксичний аналіз можуть бути сформульовані як проблема ASP.[6] Наступний код аналізує латинську фразу Puella pulchra in villa linguam latinam discit "красива дівчина навчається латині на віллі". Синтаксичне дерево виражене дуговими предикатами, які позначають залежності між словами в реченні.
Обчислена структура є лінійно впорядкованим кореневим деревом.
% ********** 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, _, _).
Порівняння реалізацій
Ранні системи, такі як Smodels, використовували пошук з поверненням, щоб знайти рішення. Як теорія і практика Boolean SAT solvers розвивалися, ряд ASP вирішувачів були побудовані на SAT вирішувачах, включаючи ASSAT і Cmodels. Вони перетворювали ASP формулу в SAT пропозицію, застосували SAT вирішувач, а потім перетворювали рішення назад до ASP форми. Більш сучасні системи, такі як Clasp, використовують гібридний підхід, використовуючи conflict-driven algorithms без повного перетворення в форму булевої логіки. Ці підходи дозволяють значні поліпшення продуктивності, часто на порядок вищі порівняно з попередніми алгоритмами з поверненням.
Проект Potassco являє собою "парасольку" для багатьох систем нижче, в тому числі clasp, система заземлення (gringo), додаткова система (iclingo), обмежені вирішувачі (clingcon), action language для ASP компіляторів (coala), розподілені MPI реалізації (claspar), і багато інших.
Більшість систем підтримують змінні, але тільки опосередковано, шляхом примусового заземлення за допомогою заземлюючого системи, такі як Lparse або грінго в якості переднього плану. Необхідність заземлення може призвести до комбінаторний вибух положення; таким чином, системи, які виконують на льоту заземлення може мати перевагу.
| Platform | Features | Mechanics | ||||||
|---|---|---|---|---|---|---|---|---|
| Name | OS | Licence | Variables | Function symbols | Explicit sets | Explicit lists | Disjunctive (choice rules) support | |
| ASPeRiX | Linux | GPL | Так | Ні | on-the-fly grounding | |||
| ASSAT | Solaris | Freeware | SAT-solver based | |||||
| Clasp Answer Set Solver | Linux, macOS, Windows | GPL | Yes, in Clingo | Так | Ні | Ні | Так | incremental, SAT-solver inspired (nogood, conflict-driven) |
| Cmodels | Linux, Solaris | GPL | Requires grounding | Так | incremental, SAT-solver inspired (nogood, conflict-driven) | |||
| DLV | Linux, macOS, Windows[7] | free for academic and non-commercial educational use, and for non-profit organizations[7] | Так | Так | Ні | Ні | Так | not Lparse compatible |
| DLV-Complex | Linux, macOS, Windows | GPL | Так | Так | Так | Так | built on top of DLV — not Lparse compatible | |
| GnT | Linux | GPL | Requires grounding | Так | built on top of smodels | |||
| nomore++ | Linux | GPL | combined literal+rule-based | |||||
| Platypus | Linux, Solaris, Windows | GPL | distributed, multi-threaded nomore++, smodels | |||||
| Pbmodels | Linux | ? | pseudo-boolean solver based | |||||
| Smodels | Linux, macOS, Windows | GPL | Requires grounding | Ні | Ні | Ні | Ні | |
| Smodels-cc | Linux | ? | Requires grounding | SAT-solver based; smodels w/conflict clauses | ||||
| Sup | Linux | ? | SAT-solver based | |||||
Посилання
- ↑ Baral, Chitta (2003). Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press. ISBN 978-0-521-81802-5.
- ↑ Gelfond, Michael (2008). Answer sets. У van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (ред.). Handbook of Knowledge Representation. Elsevier. с. 285—316. ISBN 978-0-08-055702-1.
- ↑ (Дипломна робота).
{{cite thesis}}: Пропущений або порожній|title=(довідка) - ↑ Niemelä, I.; Simons, P.; Soinenen, T. (2000). Stable model semantics of weight constraint rules. У 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. с. 317—331. ISBN 978-3-540-66749-0.
{{cite book}}:|editor-first=з пропущеним|editor-last=(довідка) - ↑ Ferraris, P.; Lifschitz, V. (January 2005). Weight constraints as nested expressions (PDF). Theory and Practice of Logic Programming. 5 (1-2): 45—74. doi:10.1017/S1471068403001923.
- ↑ Dependency parsing
- ↑ а б DLV System company page. DLVSYSTEM s.r.l. Процитовано 16 November 2011.