Програмування наборами відповідей

Програмування наборами відповідей (англ. Answer set programming, ASP) — це форма декларативного програмування, орієнтованого на складні (насамперед, NP-складні) задачі пошуку. Воно засноване на стійкій моделі семантики логічного програмування. В ASP, задача пошуку зводиться до обчислювання стійкої моделі і наборів вирішувачів (англ. answer set solvers) — програм для генерування стійких моделей, що використовуються для пошуку. Обчислювальний процес, включений в конструкцію набору вирішувачів — є посиленням DPLL алгоритму, який завжди є скінченним (на відміну від оцінки запиту в Prolog, що може призвести до нескінченного циклу).

Взагалі, ASP включає всі додатки з наборів відповідей для представлення знань[1][2] та використання оцінки запитів, типу Prolog для вирішення задач, що виникають у цих додатках.

Історія

Планувальний метод, запропонований в 1993 році Янісом Дімопулосом, Бернардом Небелем і Джонатаном Кехлером[3] є раннім прикладом програмування наборами відповідей. Їх підхід заснований на взаємозв'язку проекту зі стійкою моделлю.[4] Т. Шойнен та І. Німель[5] застосували те, що зараз відомо як програмування наборами відповідей для розв'язання задачі конфігурації продукту. Використання наборів вирішувачів для пошуку було визначене як нова парадигма програмування Віктором Мареком і Мар'яном Цужинські в документі, опублікованому в 1999 році.[6][7] Дійсно, в новій термінології «набір відповідей», замість «стабільної моделі», був вперше запропонований Ліфшицем[8], у статті, опублікованій в ретроспективі на роботу Марека-Цужинського.

Мова програмування наборів відповідей AnsProlog

Lparse — це назва програми, яка спочатку була створена як інструмент заземлення для наборів вирішувачів smodels. Мова, яку приймає Lparse, називається AnsProlog.[9] На сьогодні, вона використовується так само, і в багатьох інших вирішувачах, таких, як assat, clasp, cmodels, gNt, nomore++ і pbmodels.

Програма на AnsProlog складається з правил:

<head> :- <body> .

Символ :- («if») видаляється, якщо <body> порожній; такі правила називають фактами. Найпростіший вид правил Lparse є правила з обмеженнями. Ще однією корисною конструкцією цієї мови є вибір. Наприклад, правило

{p,q,r}.

каже: вибрати довільно, який з атомів $p,q,r$ включити до стабільної моделі. У lparse-програмі, яка містить це правило вибору і більше ніяких інших правил, є 8 стабільних довільних моделей підмножин $\{p,q,r\}$ . Визначення стабільних моделей було узагальнено до програм з вибором правил.[10] Вибір правил може розглядатися також як абревіатура для пропозиційних формул при стійкій моделі семантики.[11]

Наприклад, правило вибір вище можна розглядати як скорочення для сукупності трьох формул «виключеного третього»:

(p\lor \neg p)\land (q\lor \neg q)\land (r\lor \neg r).

Мова lparse дозволяє нам писати «обмеження» правил вибору, такі як

1{p,q,r}2.

Це правило говорить: вибрати принаймні 1 з атомів, але не більше 2. Сенс цього правила в рамках стійкої моделі семантики є пропозиційною формулою:

$(p\lor \thicksim p)\land (q\lor \thicksim q)\land (r\lor \thicksim r)\land (p\lor q\lor r)\land \thicksim (p\land q\land r)$

Границя потужності множини може бути використана в тілі правила, наприклад:

:- 2{p,q,r}.

Додавання цього обмеження в програму Lparse усуває стійкі моделі, які містять щонайменше 2 атоми. Сенс цього правила може бути представлений у вигляді пропозиційної формули

$\thicksim ((p\land q)\lor (p\land r)\lor (q\land r))$ .

Змінні (великі літери, як і в Пролозі), використовуються в 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..3).

Це скорочення:

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

Фарбування графу

n-колір на графі $G=\left\langle V,E\right\rangle$ — це функція $color:V\to \{1,\dots ,n\}$ така, що $color(x)\neq color(y)$ для кожної пари суміжних вершин $(x,y)\in E$ . Ми хотіли б використовувати ASP щоб знайти $n$ -кольорів даного графу (або визначити, що його не існує).

Це можна зробити за допомогою наступної програми 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 рядок визначає номери $1,\dots ,n$ кольорів. В залежності від вибору правил у рядку 2, унікальний колір $i$ повиннен бути призначений для кожної вершини $x$ . Обмеження у рядку 3 забороняє призначати один і той же колір до вершини $x$ і $y$ якщо існує ребро, що з'єднує їх. Якщо поєднати цей файл з визначенням $G$ таким як

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

і запустити smodels на ньому, з числовим значенням $n$ зазначеним в командному рядку, тоді атоми форми $color(\dots ,\dots )$ у вихідних даних smodels будуть представляти собою $n$ -колір $G$ .

Програма в цьому прикладі ілюструє «generate-and-test» організацію, яка часто зустрічається в простих ASP програмах. Правило вибір описує набір «потенційних рішень». Потім слідує обмеження, яке виключає всі можливі рішення, які не прийнятні. Однак, сам процес пошуку, який вживає smodels і інші набори вирішувачів не основані на методі проб і помилок.

Велика кліка

Клікою в графі називають набір попарно суміжних вершин. Наступна lparse-програма знаходить кліку розміру $\geq n$ в даному графі, або визначає, що вона не існує:

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 «створює» всі набори, що складаються з вершин $\geq n$ . Обмеження у рядку 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 «створює» всі підмножини набору ребер. Три обмеження «відсіюють» ті підмножини, які не є Гамільтонівськими циклами. Останній з них використовує допоміжний предикат $r(x)$ (« $x$ is reachable from 0»), щоб заборонити вершини, які не задовольняють цій умові. Цей предикат визначається рекурсивно в рядках 4 та 5.

Ця програма є прикладом більш загального «generate, define and test» організування, яке включає в себе визначення допоміжного предиката, який допомагає нам усунути все «погане» у потенційному рішенні.

Синтаксичний аналіз

Обробка природної мови та синтаксичний аналіз можуть бути сформульовані як проблема ASP.[12] Наступний код аналізує латинську фразу 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, та інші.

Більшість систем підтримують змінні, та тільки опосередковано, шляхом примусового заземлення за допомогою заземлюючих систем, таких як Lparse чи gringo. Необхідність заземлення може призвести до комбінаторних вибухів; таким чином, системи які виконують заземлення на льоту мають перевагу.

Платформа			Риси					Механіка
Найменування	Операційна система	Ліцензія	Змінні	Функціональні символи	Явні набори	Явні списки	Правила вибору
ASPeRiX	Linux	GPL	Так				Ні	заземлення «на льоту»
ASSAT	Solaris	Безкоштовна						заснований на SAT-вирішувачі
Clasp Answer Set Solver	Linux, macOS, Windows	GPL	Так	Так	Ні	Ні	Так	інкрементний, надхненний Sat-вирішувачем
Cmodels	Linux, Solaris	GPL	Потребує заземлення				Так	інкрементний, надхненний Sat-вирішувачем
DLV	Linux, macOS, Windows[13]	безкоштовна для академічного та некомерційного використання в освітніх цілях, а також для некомерційних організацій	Так	Так	Ні	Ні	Так	Не Lparse сумісний
DLV-Complex	Linux, macOS, Windows	GPL		Так	Так	Так	Так	побудований на вершині DLV — не Lparse сумісний
GnT	Linux	GPL	Потребує заземлення				Так	побудований на вершині smodels
nomore++	Linux	GPL						комбінований
Platypus	Linux, Solaris, Windows	GPL						розподілений
Pbmodels	Linux	?						заснований на псевдобулевському вирішувачі
Smodels	Linux, macOS, Windows	GPL	Потребує заземлення	Ні	Ні	Ні	Ні
Smodels-cc	Linux	?	Потребує заземлення					заснований на SAT-вирішувачі
Sup	Linux	?						заснований на SAT-вирішувачі

Див. також

Посилання

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. as PDF Архівовано 3 березня 2016 у Wayback Machine.
Dimopoulos, Y.; Nebel, B.; Köhler, J. (1997). Encoding planning problems in non-monotonic logic programs. У 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. с. 273–285. ISBN 978-3-540-63912-1. as Postscript
Subrahmanian, V.S.; Zaniolo, C. (1995). Relating stable models and AI planning domains. У Sterling, Leon. Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming. MIT Press. с. 233–247. ISBN 978-0-262-69177-2. as Postscript
Soininen, T.; Niemelä, I. (1998). Formalizing configuration knowledge using rules with choices (Postscript) (TKO-B142). Проігноровано невідомий параметр |institution= (довідка)
Marek, V.; Truszczyński, M. (1999). Stable models and an alternative logic programming paradigm. У Apt, Krzysztof R. The Logic programming paradigm: a 25-year perspective (PDF). Springer. с. 169–181. ISBN 978-3-540-65463-6.
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.
Lifschitz, V. (1999). Action Languages, Answer Sets, and Planning. In Apt, 1999, pp. 357–374
Crick, Tom (2009). Superoptimisation: Provably Optimal Code Generation using Answer Set Programming (Ph.D.). University of Bath. 20352. Архів оригіналу за 4 березня 2016. Процитовано 21 грудня 2016.
Niemelä, I.; Simons, P.; Soinenen, T. (2000). Stable model semantics of weight constraint rules. У 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. с. 317–331. ISBN 978-3-540-66749-0. as Postscript
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. as Postscript
Dependency parsing. Архів оригіналу за 15 квітня 2015. Процитовано 18 грудня 2016.
DLV System company page. DLVSYSTEM s.r.l. Процитовано 16 листопада 2011.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] Baral, Chitta (2003). Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press. ISBN 978-0-521-81802-5.

[2] 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. as PDF Архівовано 3 березня 2016 у Wayback Machine.

[3] Dimopoulos, Y.; Nebel, B.; Köhler, J. (1997). Encoding planning problems in non-monotonic logic programs. У 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. с. 273–285. ISBN 978-3-540-63912-1. as Postscript

[4] Subrahmanian, V.S.; Zaniolo, C. (1995). Relating stable models and AI planning domains. У Sterling, Leon. Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming. MIT Press. с. 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). Проігноровано невідомий параметр |institution= (довідка)

[6] Marek, V.; Truszczyński, M. (1999). Stable models and an alternative logic programming paradigm. У Apt, Krzysztof R. The Logic programming paradigm: a 25-year perspective (PDF). Springer. с. 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, pp. 357–374

[9] Crick, Tom (2009). Superoptimisation: Provably Optimal Code Generation using Answer Set Programming (Ph.D.). University of Bath. 20352. Архів оригіналу за 4 березня 2016. Процитовано 21 грудня 2016.

[10] Niemelä, I.; Simons, P.; Soinenen, T. (2000). Stable model semantics of weight constraint rules. У 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. с. 317–331. ISBN 978-3-540-66749-0. as Postscript

[11] 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. as Postscript

[12] Dependency parsing. Архів оригіналу за 15 квітня 2015. Процитовано 18 грудня 2016.

[dlvsystem.com-13] DLV System company page. DLVSYSTEM s.r.l. Процитовано 16 листопада 2011.