Программирование наборов ответов: различия между версиями

Содержимое удалено Содержимое добавлено

Линейный

Версия от 19:03, 6 апреля 2018

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

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

История

Метод планирования, предложенный в 1993 году Димопулосом, Небелем и Кёлером^[3], является ранним примером программирования набора ответов. Их подход основан на взаимосвязи между планами и стабильными моделями^[4]. Soininen и Niemelä^[5] применили то, что теперь известно как программирование на основе ответа, к проблеме конфигурации продукта. Использование решающих наборов ответов для поиска было идентифицировано как новая парадигма программирования Марека и Трущинского в статье, появившейся в 25-летней перспективе по парадигме логического программирования, опубликованной в 1999 году ^[6] и в [Niemelä 1999] ^[7]. ] Действительно, новая терминология «набора ответов» вместо «стабильной модели» была впервые предложена Лифшицем ^[7] в статье, выходящей в том же ретроспективном объеме, что и статья Марека-Трущинского.

Язык программирования набора задач AnsProlog

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

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

<head> :- <body> .

Символ :- («if») убирается, если <body> пуст; такие правила называются фактами. Простейший вид правил Lparse это правила с ограничениями. Еще одной полезной конструкцией является выбор. Например, правило

{p,q,r}.

означает: выберите случайно, какой из атомов $p,q,r$ включить в стабильную модель. В lparse-программе, которая содержит это правило и больше никаких других правил, имеет 8 стабильных моделей подмножеств $\{p,q,r\}$ . Определение стабильных моделей было ограничено до программ с выбором правил.^[4] Выбор правил также может использоваться для сокращения формул логики.

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

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

Язык lparse позволяет нам писать «ограничения» правил выбора, такие как

1{p,q,r}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 устраняет устойчивые модели, которые содержат менее двух атомов.Правило можно быть представлено в виде логической формулы:

$\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.^[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, та інші.

Більшість систем підтримують змінні, та тільки опосередковано, шляхом примусового заземлення за допомогою заземлюючих систем, таких як 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^[7]	бесплатная для академического и некоммерческого использования	Да	Да	Нет	Нетs	Да	Не 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. Knowledge Representation, Reasoning and Declarative Problem Solving. — Cambridge University Press, 2003. — ISBN 978-0-521-81802-5.
↑ Gelfond, Michael. Answer sets // Handbook of Knowledge Representation. — Elsevier, 2008. — P. 285–316. — ISBN 978-0-08-055702-1. as PDF
↑ ¹ ² Crick, Tom (2009). Superoptimisation: Provably Optimal Code Generation using Answer Set Programming (PDF) (Ph.D.). University of Bath. Docket 20352.
↑ ¹ ² Niemelä, I. 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 / I. Niemelä, P. Simons, T. Soinenen. — Springer, 2000. — Vol. 1730. — P. 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
↑ ¹ ² ³ DLV System company page (неопр.). DLVSYSTEM s.r.l.. Дата обращения: 16 ноября 2011.

Внешние ссылки

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

[2] Gelfond, Michael. Answer sets // Handbook of Knowledge Representation. — Elsevier, 2008. — P. 285–316. — ISBN 978-0-08-055702-1. as PDF

[:0-3] ¹ ² Crick, Tom (2009). Superoptimisation: Provably Optimal Code Generation using Answer Set Programming (PDF) (Ph.D.). University of Bath. Docket 20352.

[:1-4] ¹ ² Niemelä, I. 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 / I. Niemelä, P. Simons, T. Soinenen. — Springer, 2000. — Vol. 1730. — P. 317–331. — ISBN 978-3-540-66749-0. as Postscript

[:2-5] 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

[:3-6] ¹ ² Dependency parsing

[dlvsystem.com-7] ¹ ² ³ DLV System company page (неопр.). DLVSYSTEM s.r.l.. Дата обращения: 16 ноября 2011.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

Программирование наборов ответов: различия между версиями

Версия от 19:03, 6 апреля 2018

Содержание

История

Язык программирования набора задач AnsProlog

Генерация устойчивых моделей

Примеры программ ASP

Окрашивание графа

Большой клик

Гамильтонов цикл

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

Сравнение реализаций

Ссылки

Внешние ссылки

Навигация

Программирование наборов ответов: различия между версиями

Версия от 19:03, 6 апреля 2018

История

Язык программирования набора задач AnsProlog

Генерация устойчивых моделей

Примеры программ ASP

Окрашивание графа

Большой клик

Гамильтонов цикл

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

Сравнение реализаций

Ссылки

Внешние ссылки

Навигация

Поиск