Программирование наборов ответов

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

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

История

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

AnsProlog

Lparse — программа, изначально была созданная как инструмент заземления (англ. Symbol grounding problem) для решателя smodels. AnsProlog — язык, используемый Lparse, используется как в Lparse, так и в таких решателях, как assat, clasp, cmodels], gNt, nomore++ и pbmodels.

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

<head> :- <body> .

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

Ещё одной полезной конструкцией является выбор. Например, правило:

{p,q,r}.

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

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

(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))$ .

Переменные (в верхнем регистре, как и в языке Prolog), используются в 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,\dots ,n$ цветов. В зависимости от выбора правил в строке 2, уникальный цвет $i$ должен быть назначен для каждой вершины $x$ . Ограничение в строке 3 запрещает назначать один и тот же цвет к вершине $x$ и $y$ если существует ребро, соединяющее их.

Если совместить этот файл с определением $G$ таким как:

v(1..100). % 1,...,100 вершины
e(1,55). % существует ребро между 1 и 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 организации. Выбор правил в строке 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$ достижимый из 0»), чтобы запретить вершины, которые не удовлетворяют этому условию. Этот предикат определяется рекурсивно в строках 4 и 5.

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

Обработка естественного языка и синтаксический анализ могут быть сформулированы как проблема ASP^[3]. Следующий код анализирует латинскую фразу 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, используют гибридный подход, используя конфликтующие алгоритмы без полного преобразования в форму булевой логики. Эти подходы позволяют значительно улучшить производительность, часто на порядок качественно лучше по сравнению с предыдущими методами с возвращением.

Проект Potassco работает поверх многих низкоуровневых систем, в том числе clasp, систему обоснователей gringo, и других.

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

Платформа			Особенности					Механика
Название	Операционная система	Лицензия	Переменные	Функциональные символы	Явные наборы	Явные списки	Правила выбора
ASPeRiX^[4]	Linux	GPL	Да				Нет	обоснование «на лету»
ASSAT^[5]	Solaris	Бесплатная						основан на SAT-решателе
Clasp Answer Set Solver^[6]	Linux, macOS, Windows	GPL	Да	Да	Нет	Нет	Да	основан на SAT-решателе
Cmodels^[7]	Linux, Solaris	GPL	Требует обоснования				Да	основан на SAT-решателе
DLV	Linux, macOS, Windows^[8]	Бесплатная для академического и некоммерческого использования	Да	Да	Нет	Нетs	Да	не Lparse совместимый
DLV-Complex^[9]	Linux, macOS, Windows	GPL		Да	Да	Да	Да	основан на DLV — несовместимый c Lparse
GnT^[10]	Linux	GPL	Требует обоснования				Да	основан на smodels
nomore++^[11]	Linux	GPL						комбинированные
Platypus^[12]	Linux, Solaris, Windows	GPL						распределённый
Pbmodels^[13]	Linux	?						основан на псевдобулевском решателе
Smodels^[14]	Linux, macOS, Windows	GPL	Требует обоснования	Нет	Нет	Нет	Нет
Smodels-cc^[15]	Linux	?	Требует обоснования					основан на SAT-решателе
Sup^[16]	Linux	?						основан на SAT-решателе

Примечания

↑ Ferraris, P.; Lifschitz, V. Weight constraints as nested expressions (неопр.) // Theory and Practice of Logic Programming. — 2005. — January (т. 5, № 1—2). — С. 45—74. — doi:10.1017/S1471068403001923. as Postscript
↑ ¹ ² Niemelä, I.; Simons, P.; Soinenen, T. 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 (англ.) / Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald. — Springer, 2000. — Vol. 1730. — P. 317—331. — (Lecture notes in computer science: Lecture notes in artificial intelligence). — ISBN 978-3-540-66749-0. as Postscript
↑ Dependency parsing (неопр.). Дата обращения: 6 апреля 2018. Архивировано из оригинала 15 апреля 2015 года.
↑ ASPeRiX
↑ [1]
↑ clasp: an ASP solver
↑ CMODELS - Answer Set programming System
↑ DLV System company page (неопр.). DLVSYSTEM s.r.l.. Дата обращения: 16 ноября 2011.
↑ dlv-complex - dlv-complex
↑ TCS - Software - lpeq
↑ nomore: a Solver for Logic Programs
↑ platypus: a Platform for Distributed Answer Set Programming
↑ http://www.cs.uky.edu/ai/pbmodels/
↑ Computing the Stable Model Semantics
↑ Smodels_cc
↑ http://www.cs.utexas.edu/users/tag/sup/

Ссылки

[:2-1] Ferraris, P.; Lifschitz, V. Weight constraints as nested expressions (неопр.) // Theory and Practice of Logic Programming. — 2005. — January (т. 5, № 1—2). — С. 45—74. — doi:10.1017/S1471068403001923. as Postscript

[:1-2] ¹ ² Niemelä, I.; Simons, P.; Soinenen, T. 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 (англ.) / Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald. — Springer, 2000. — Vol. 1730. — P. 317—331. — (Lecture notes in computer science: Lecture notes in artificial intelligence). — ISBN 978-3-540-66749-0. as Postscript

[:3-3] Dependency parsing (неопр.). Дата обращения: 6 апреля 2018. Архивировано из оригинала 15 апреля 2015 года.

[4] ASPeRiX

[5] [1]

[6] sp: an ASP solver

[7] CMODELS - Answer Set programming System

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

[9] v-complex - dlv-complex

[10] TCS - Software - lpeq

[11] re: a Solver for Logic Programs

[12] typus: a Platform for Distributed Answer Set Programming

[13] ttp://www.cs.uky.edu/ai/pbmodels/

[14] Computing the Stable Model Semantics

[15] Smodels_cc

[16] ttp://www.cs.utexas.edu/users/tag/sup/

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

Программирование наборов ответов

Содержание

История

AnsProlog

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

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

Раскраска графа

Задача о клике

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

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

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

Примечания

Ссылки

Навигация

Программирование наборов ответов

История

AnsProlog

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

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

Раскраска графа

Задача о клике

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

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

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

Примечания

Ссылки

Навигация

Поиск