Програмування наборами відповідей
Парадигми програмування |
---|
|
Програмування наборами відповідей (англ. Answer set programming, ASP) — це форма декларативного програмування, орієнтованого на складні (насамперед, NP-складні) задачі пошуку. Воно засноване на стійкій моделі семантики логічного програмування. В ASP, задача пошуку зводиться до обчислювання стійкої моделі і наборів вирішувачів (англ. answer set solvers) — програм для генерування стійких моделей, що використовуються для пошуку. Обчислювальний процес, включений в конструкцію набору вирішувачів — є посиленням DPLL алгоритму, який завжди є скінченним (на відміну від оцінки запиту в Prolog, що може призвести до нескінченного циклу).
Взагалі, ASP включає всі додатки з наборів відповідей для представлення знань[1][2] та використання оцінки запитів, типу Prolog для вирішення задач, що виникають у цих додатках.
Історія
Планувальний метод, запропонований в 1993 році Янісом Дімопулосом, Бернардом Небелем[en] і Джонатаном Кехлером[3] є раннім прикладом програмування наборами відповідей. Їх підхід заснований на взаємозв'язку проекту зі стійкою моделлю.[4] Т. Шойнен та І. Німель[5] застосували те, що зараз відомо як програмування наборами відповідей для розв'язання задачі конфігурації продукту. Використання наборів вирішувачів для пошуку було визначене як нова парадигма програмування Віктором Мареком[en] і Мар'яном Цужинські в документі, опублікованому в 1999 році.[6][7] Дійсно, в новій термінології «набір відповідей», замість «стабільної моделі», був вперше запропонований Ліфшицем[8], у статті, опублікованій в ретроспективі на роботу Марека-Цужинського.
Мова програмування наборів відповідей AnsProlog
Lparse — це назва програми, яка спочатку була створена як інструмент заземлення[en] для наборів вирішувачів smodels. Мова, яку приймає Lparse, називається AnsProlog.[9] На сьогодні, вона використовується так само, і в багатьох інших вирішувачах, таких, як assat, clasp, cmodels, gNt, nomore++ і pbmodels.
Програма на AnsProlog складається з правил:
<head> :- <body> .
Символ :-
(«if») видаляється, якщо <body>
порожній; такі правила називають фактами. Найпростіший вид правил Lparse є правила з обмеженнями.
Ще однією корисною конструкцією цієї мови є вибір. Наприклад, правило
{p,q,r}.
каже: вибрати довільно, який з атомів включити до стабільної моделі. У lparse-програмі, яка містить це правило вибору і більше ніяких інших правил, є 8 стабільних довільних моделей підмножин . Визначення стабільних моделей було узагальнено до програм з вибором правил.[10] Вибір правил може розглядатися також як абревіатура для пропозиційних формул при стійкій моделі семантики.[11]
Наприклад, правило вибір вище можна розглядати як скорочення для сукупності трьох формул «виключеного третього»:
Мова lparse дозволяє нам писати «обмеження» правил вибору, такі як
1{p,q,r}2.
Це правило говорить: вибрати принаймні 1 з атомів, але не більше 2. Сенс цього правила в рамках стійкої моделі семантики є пропозиційною формулою:
Границя потужності множини може бути використана в тілі правила, наприклад:
:- 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..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-колір на графі — це функція така, що для кожної пари суміжних вершин . Ми хотіли б використовувати 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.[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, Laboratory of Information Processing Science, Helsinki University of Technology
- ↑ 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, с. 357—374
- ↑ Crick, Tom (2009). Superoptimisation: Provably Optimal Code Generation using Answer Set Programming (PDF) (Ph.D.). University of Bath. 20352. Архів оригіналу (PDF) за 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.