Програмування наборами відповідей (англ. Answer set programming, ASP) — це форма декларативного програмування, орієнтованого на складні (насамперед, NP-складні) задачі пошуку. Воно засноване на стійкій моделі семантики логічного програмування. В ASP, задача пошуку зводиться до обчислювання стійкої моделі і наборів вирішувачів (англ. answer set solvers) — програм для генерування стійких моделей, що використовуються для пошуку. Обчислювальний процес, включений в конструкцію набору вирішувачів — є посиленням DPLL алгоритму, який завжди є скінченним (на відміну від оцінки запиту в Prolog, що може призвести до нескінченного циклу).
Взагалі, ASP включає всі додатки з наборів відповідей для представлення знань та використання оцінки запитів, типу Prolog для вирішення задач, що виникають у цих додатках.
Історія
Планувальний метод, запропонований в 1993 році Янісом Дімопулосом, [en] і Джонатаном Кехлером є раннім прикладом програмування наборами відповідей. Їх підхід заснований на взаємозв'язку проекту зі стійкою моделлю. Т. Шойнен та І. Німель застосували те, що зараз відомо як програмування наборами відповідей для розв'язання задачі конфігурації продукту. Використання наборів вирішувачів для пошуку було визначене як нова парадигма програмування [en] і Мар'яном Цужинські в документі, опублікованому в 1999 році. Дійсно, в новій термінології «набір відповідей», замість «стабільної моделі», був вперше запропонований Ліфшицем, у статті, опублікованій в ретроспективі на роботу Марека-Цужинського.
Мова програмування наборів відповідей AnsProlog
Lparse — це назва програми, яка спочатку була створена як інструмент [en] для наборів вирішувачів smodels. Мова, яку приймає Lparse, називається AnsProlog. На сьогодні, вона використовується так само, і в багатьох інших вирішувачах, таких, як , clasp, cmodels, gNt, nomore++ і pbmodels.
Програма на AnsProlog складається з правил:
<head> :- <body> .
Символ :-
(«if») видаляється, якщо <body>
порожній; такі правила називають фактами. Найпростіший вид правил Lparse є правила з обмеженнями. Ще однією корисною конструкцією цієї мови є вибір. Наприклад, правило
{p,q,r}.
каже: вибрати довільно, який з атомів включити до стабільної моделі. У lparse-програмі, яка містить це правило вибору і більше ніяких інших правил, є 8 стабільних довільних моделей підмножин . Визначення стабільних моделей було узагальнено до програм з вибором правил. Вибір правил може розглядатися також як абревіатура для пропозиційних формул при стійкій моделі семантики.
Наприклад, правило вибір вище можна розглядати як скорочення для сукупності трьох формул «виключеного третього»:
Мова 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. Наступний код аналізує латинську фразу 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 | Так | Ні | заземлення «на льоту» | |||
Solaris | Безкоштовна | заснований на SAT-вирішувачі | ||||||
Clasp Answer Set Solver | Linux, macOS, Windows | GPL | Так | Так | Ні | Ні | Так | інкрементний, надхненний Sat-вирішувачем |
Cmodels | Linux, Solaris | GPL | Потребує заземлення | Так | інкрементний, надхненний Sat-вирішувачем | |||
DLV | Linux, macOS, Windows | безкоштовна для академічного та некомерційного використання в освітніх цілях, а також для некомерційних організацій | Так | Так | Ні | Ні | Так | Не 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 .
- Gelfond, Michael (2008). Answer sets. У van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (ред.). Handbook of Knowledge Representation. Elsevier. с. 285—316. ISBN . as PDF [ 3 березня 2016 у Wayback Machine.]
- Dimopoulos, Y.; ; 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 . 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 . 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 .
- 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). (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 . 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.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Programuvannya naborami vidpovidej angl Answer set programming ASP ce forma deklarativnogo programuvannya oriyentovanogo na skladni nasampered NP skladni zadachi poshuku Vono zasnovane na stijkij modeli semantiki logichnogo programuvannya V ASP zadacha poshuku zvoditsya do obchislyuvannya stijkoyi modeli i naboriv virishuvachiv angl answer set solvers program dlya generuvannya stijkih modelej sho vikoristovuyutsya dlya poshuku Obchislyuvalnij proces vklyuchenij v konstrukciyu naboru virishuvachiv ye posilennyam DPLL algoritmu yakij zavzhdi ye skinchennim na vidminu vid ocinki zapitu v Prolog sho mozhe prizvesti do neskinchennogo ciklu Vzagali ASP vklyuchaye vsi dodatki z naboriv vidpovidej dlya predstavlennya znan ta vikoristannya ocinki zapitiv tipu Prolog dlya virishennya zadach sho vinikayut u cih dodatkah IstoriyaPlanuvalnij metod zaproponovanij v 1993 roci Yanisom Dimopulosom en i Dzhonatanom Kehlerom ye rannim prikladom programuvannya naborami vidpovidej Yih pidhid zasnovanij na vzayemozv yazku proektu zi stijkoyu modellyu T Shojnen ta I Nimel zastosuvali te sho zaraz vidomo yak programuvannya naborami vidpovidej dlya rozv yazannya zadachi konfiguraciyi produktu Vikoristannya naboriv virishuvachiv dlya poshuku bulo viznachene yak nova paradigma programuvannya en i Mar yanom Cuzhinski v dokumenti opublikovanomu v 1999 roci Dijsno v novij terminologiyi nabir vidpovidej zamist stabilnoyi modeli buv vpershe zaproponovanij Lifshicem u statti opublikovanij v retrospektivi na robotu Mareka Cuzhinskogo Mova programuvannya naboriv vidpovidej AnsPrologLparse ce nazva programi yaka spochatku bula stvorena yak instrument en dlya naboriv virishuvachiv smodels Mova yaku prijmaye Lparse nazivayetsya AnsProlog Na sogodni vona vikoristovuyetsya tak samo i v bagatoh inshih virishuvachah takih yak clasp cmodels gNt nomore i pbmodels Programa na AnsProlog skladayetsya z pravil lt head gt lt body gt Simvol if vidalyayetsya yaksho lt body gt porozhnij taki pravila nazivayut faktami Najprostishij vid pravil Lparse ye pravila z obmezhennyami She odniyeyu korisnoyu konstrukciyeyu ciyeyi movi ye vibir Napriklad pravilo p q r kazhe vibrati dovilno yakij z atomiv p q r displaystyle p q r vklyuchiti do stabilnoyi modeli U lparse programi yaka mistit ce pravilo viboru i bilshe niyakih inshih pravil ye 8 stabilnih dovilnih modelej pidmnozhin p q r displaystyle p q r Viznachennya stabilnih modelej bulo uzagalneno do program z viborom pravil Vibir pravil mozhe rozglyadatisya takozh yak abreviatura dlya propozicijnih formul pri stijkij modeli semantiki Napriklad pravilo vibir vishe mozhna rozglyadati yak skorochennya dlya sukupnosti troh formul viklyuchenogo tretogo p p q q r r displaystyle p lor neg p land q lor neg q land r lor neg r Mova lparse dozvolyaye nam pisati obmezhennya pravil viboru taki yak1 p q r 2 Ce pravilo govorit vibrati prinajmni 1 z atomiv ale ne bilshe 2 Sens cogo pravila v ramkah stijkoyi modeli semantiki ye propozicijnoyu formuloyu p p q q r r p q r p q r displaystyle 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 Granicya potuzhnosti mnozhini mozhe buti vikoristana v tili pravila napriklad 2 p q r Dodavannya cogo obmezhennya v programu Lparse usuvaye stijki modeli yaki mistyat shonajmenshe 2 atomi Sens cogo pravila mozhe buti predstavlenij u viglyadi propozicijnoyi formuli p q p r q r displaystyle thicksim p land q lor p land r lor q land r Zminni veliki literi yak i v Prolozi vikoristovuyutsya v Lparse dlya skorochuvannya kolekcij pravil yaki dotrimuyutsya tiyeyi zh shemi a takozh dlya skorochennya kolekcij atomiv v odne i te zh pravilo Napriklad Lparse programa p a p b p c q X p X X a maye take zh znachennya yak p a p b p c q b q c Programa p a p b p c q X p X 2 ce skorochennya p a p b p c q a q b q c 2 Diapazon maye viglyad lt Predicate gt start end de pochatok i kinec ye konstantnimi arifmetichnimi virazami zi znachennyam Diapazon umovne skorochennya yake vikoristovuyetsya v osnovnomu dlya viznachennya chislovih domeniv sumisnim sposobom Napriklad fakt a 1 3 Ce skorochennya a 1 a 2 a 3 Diapazoni takozh mozhut buti vikoristani v tili pravila z tiyeyu zh semantikoyu Umovnij tekst maye viglyad p X q X Yaksho rozshirennya q ye q a1 q a2 q aN to vishevkazana umova semantichno ekvivalentna zapisu p a1 p a2 p aN na misci umovi Napriklad q 1 2 a 1 p X q X Ce skorochennya dlya q 1 q 2 a 1 p 1 p 2 Stvorennya stijkih modelejDlya znahodzhennya stijkoyi modeli Lparse programi sho zberigayetsya u fajli filename vikoristovuyetsya komanda lparse filename smodels Parametr 0 vkazuye smodels znajti vsi stijki modeli programi Napriklad yaksho fajl test mistit pravila 1 p q r 2 s not p todi komanda vidast 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 sPrikladi program ASPFarbuvannya grafu n kolir na grafi G V E displaystyle G left langle V E right rangle ce funkciya c o l o r V 1 n displaystyle color V to 1 dots n taka sho c o l o r x c o l o r y displaystyle color x neq color y dlya kozhnoyi pari sumizhnih vershin x y E displaystyle x y in E Mi hotili b vikoristovuvati ASP shob znajti n displaystyle n koloriv danogo grafu abo viznachiti sho jogo ne isnuye Ce mozhna zrobiti za dopomogoyu nastupnoyi programi 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 ryadok viznachaye nomeri 1 n displaystyle 1 dots n koloriv V zalezhnosti vid viboru pravil u ryadku 2 unikalnij kolir i displaystyle i povinnen buti priznachenij dlya kozhnoyi vershini x displaystyle x Obmezhennya u ryadku 3 zaboronyaye priznachati odin i toj zhe kolir do vershini x displaystyle x i y displaystyle y yaksho isnuye rebro sho z yednuye yih Yaksho poyednati cej fajl z viznachennyam G displaystyle G takim yakv 1 100 1 100 are vertices e 1 55 there is an edge from 1 to 55 i zapustiti smodels na nomu z chislovim znachennyam n displaystyle n zaznachenim v komandnomu ryadku todi atomi formi c o l o r displaystyle color dots dots u vihidnih danih smodels budut predstavlyati soboyu n displaystyle n kolir G displaystyle G Programa v comu prikladi ilyustruye generate and test organizaciyu yaka chasto zustrichayetsya v prostih ASP programah Pravilo vibir opisuye nabir potencijnih rishen Potim sliduye obmezhennya yake viklyuchaye vsi mozhlivi rishennya yaki ne prijnyatni Odnak sam proces poshuku yakij vzhivaye smodels i inshi nabori virishuvachiv ne osnovani na metodi prob i pomilok Velika klika Klikoyu v grafi nazivayut nabir poparno sumizhnih vershin Nastupna lparse programa znahodit kliku rozmiru n displaystyle geq n v danomu grafi abo viznachaye sho vona ne isnuye n in X v X in X in Y v X v Y X Y not e X Y not e Y X Ce she odin priklad generate and test organization Vibir pravil u ryadku 1 stvoryuye vsi nabori sho skladayutsya z vershin n displaystyle geq n Obmezhennya u ryadku 2 vidsivaye ti nabori yaki ne ye klikami Gamiltoniv cikl Gamiltoniv cikl v oriyentovanomu grafi ye cikl yakij prohodit cherez kozhnu vershinu grafu rivno odin raz Nastupna Lparse programa mozhe buti vikoristana dlya poshuku Gamiltonivskogo ciklu v zadanomu oriyentovanomu grafi yaksho vin isnuye mi pripuskayemo sho 0 ce odna z vershin 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 viboru v ryadku 1 stvoryuye vsi pidmnozhini naboru reber Tri obmezhennya vidsiyuyut ti pidmnozhini yaki ne ye Gamiltonivskimi ciklami Ostannij z nih vikoristovuye dopomizhnij predikat r x displaystyle r x x displaystyle x is reachable from 0 shob zaboroniti vershini yaki ne zadovolnyayut cij umovi Cej predikat viznachayetsya rekursivno v ryadkah 4 ta 5 Cya programa ye prikladom bilsh zagalnogo generate define and test organizuvannya yake vklyuchaye v sebe viznachennya dopomizhnogo predikata yakij dopomagaye nam usunuti vse pogane u potencijnomu rishenni Sintaksichnij analiz Obrobka prirodnoyi movi ta sintaksichnij analiz mozhut buti sformulovani yak problema ASP Nastupnij kod analizuye latinsku frazu Puella pulchra in villa linguam latinam discit krasiva divchina navchayetsya latini na villi Sintaksichne derevo virazhene dugovimi predikatami yaki poznachayut zalezhnosti mizh slovami v rechenni Obchislena struktura ye linijno vporyadkovanim korenevim derevom 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 lt 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 Porivnyannya realizacijRanni sistemi taki yak Smodels vikoristovuvali poshuk z povernennyam shob znajti rishennya Z rozvitkom teoriyi i praktiki u zadachah zdijsnennosti bulovih formul Boolean SAT solvers zbilshuvalasya kilkist ASP virishuvachiv sproektovanih na osnovi SAT virishuvachiv vklyuchno z ASSAT ta Cmodels Voni peretvoryuvali ASP formulu v SAT propoziciyu zastosuvali SAT virishuvach a potim peretvoryuvali rishennya nazad do ASP formi Bilsh suchasni sistemi taki yak Clasp vikoristovuyut gibridnij pidhid vikoristovuyuchi conflict driven algorithms bez povnogo peretvorennya v formu bulevoyi logiki Ci pidhodi dozvolyayut znachno polipshiti produktivnist chasto na poryadok krashi porivnyano z poperednimi algoritmami z povernennyam Proekt Potassco yavlyaye soboyu parasolku dlya bagatoh nizkorivnevih sistem v tomu chisli clasp sistemu zazemlennya gringo ta inshi Bilshist sistem pidtrimuyut zminni ta tilki oposeredkovano shlyahom primusovogo zazemlennya za dopomogoyu zazemlyuyuchih sistem takih yak Lparse chi gringo Neobhidnist zazemlennya mozhe prizvesti do kombinatornih vibuhiv takim chinom sistemi yaki vikonuyut zazemlennya na lotu mayut perevagu Platforma Risi Mehanika Najmenuvannya Operacijna sistema Licenziya Zminni Funkcionalni simvoli Yavni nabori Yavni spiski Pravila viboru ASPeRiX Linux GPL Tak Ni zazemlennya na lotu Solaris Bezkoshtovna zasnovanij na SAT virishuvachi Clasp Answer Set Solver Linux macOS Windows GPL Tak Tak Ni Ni Tak inkrementnij nadhnennij Sat virishuvachem Cmodels Linux Solaris GPL Potrebuye zazemlennya Tak inkrementnij nadhnennij Sat virishuvachem DLV Linux macOS Windows bezkoshtovna dlya akademichnogo ta nekomercijnogo vikoristannya v osvitnih cilyah a takozh dlya nekomercijnih organizacij Tak Tak Ni Ni Tak Ne Lparse sumisnij DLV Complex Linux macOS Windows GPL Tak Tak Tak Tak pobudovanij na vershini DLV ne Lparse sumisnij GnT Linux GPL Potrebuye zazemlennya Tak pobudovanij na vershini smodels nomore Linux GPL kombinovanij Platypus Linux Solaris Windows GPL rozpodilenij Pbmodels Linux zasnovanij na psevdobulevskomu virishuvachi Smodels Linux macOS Windows GPL Potrebuye zazemlennya Ni Ni Ni Ni Smodels cc Linux Potrebuye zazemlennya zasnovanij na SAT virishuvachi Sup Linux zasnovanij na SAT virishuvachiDiv takozhLogika programuvannya Prolog Stabilna model semantikiPosilannyaBaral Chitta 2003 Knowledge Representation Reasoning and Declarative Problem Solving Cambridge University Press ISBN 978 0 521 81802 5 Gelfond Michael 2008 Answer sets U van Harmelen Frank Lifschitz Vladimir Porter Bruce red Handbook of Knowledge Representation Elsevier s 285 316 ISBN 978 0 08 055702 1 as PDF 3 bereznya 2016 u Wayback Machine Dimopoulos Y Kohler J 1997 Encoding planning problems in non monotonic logic programs U Steel Sam Alami Rachid red 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 T 1348 Springer s 273 285 ISBN 978 3 540 63912 1 as Postscript Subrahmanian V S Zaniolo C 1995 Relating stable models and AI planning domains U Sterling Leon red Logic Programming Proceedings of the Twelfth International Conference on Logic Programming MIT Press s 233 247 ISBN 978 0 262 69177 2 as Postscript Soininen T Niemela I 1998 Formalizing configuration knowledge using rules with choices Postscript TKO B142 Laboratory of Information Processing Science Helsinki University of Technology Marek V Truszczynski M 1999 Stable models and an alternative logic programming paradigm U Apt Krzysztof R red The Logic programming paradigm a 25 year perspective PDF Springer s 169 181 ISBN 978 3 540 65463 6 Niemela 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 s 357 374 Crick Tom 2009 PDF Ph D University of Bath 20352 Arhiv originalu PDF za 4 bereznya 2016 Procitovano 21 grudnya 2016 Niemela I Simons P Soinenen T 2000 Stable model semantics of weight constraint rules U Gelfond Michael Leone Nicole Pfeifer Gerald red 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 T 1730 Springer s 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 Arhiv originalu za 15 kvitnya 2015 Procitovano 18 grudnya 2016 DLV System company page DLVSYSTEM s r l Procitovano 16 listopada 2011