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

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

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

История

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

AnsProlog

Lparse — программа, изначально была создана, как инструмент формирования базовых высказываний ( англ. ) для вычисления логических высказываний 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\}$ . Определение стабильных моделей было ограничено до программ с выбором правил . Выбор правил также может использоваться для сокращения формул логики.

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

(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 . Следующий код анализирует латинскую фразу 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	Linux	GPL	Да				Нет	обоснование «на лету»
ASSAT	Solaris	Бесплатная						основан на SAT-решателе
Clasp Answer Set Solver	Linux , macOS , Windows	GPL	Да	Да	Нет	Нет	Да	основан на SAT-решателе
Cmodels	Linux , Solaris	GPL	Требует обоснования				Да	основан на SAT-решателе
	Linux , macOS , Windows	Бесплатная для академического и некоммерческого использования	Да	Да	Нет	Нетs	Да	не Lparse-совместимый
DLV-Complex	Linux , macOS , Windows	GPL		Да	Да	Да	Да	основан на — несовместимый c 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-решателе

Примечания

Ferraris, P.; Lifschitz, V. (неопр.) // Theory and Practice of Logic Programming. — 2005. — January ( т. 5 , № 1—2 ). — С. 45—74 . — doi : . от 22 сентября 2017 на Wayback Machine
↑ Niemelä, I.; Simons, P.; Soinenen, T. // 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 . от 15 октября 2008 на Wayback Machine
. Дата обращения: 6 апреля 2018. Архивировано из 15 апреля 2015 года.
. Дата обращения: 6 апреля 2018. 8 ноября 2016 года.
. Дата обращения: 6 апреля 2018. 16 ноября 2018 года.
. Дата обращения: 6 апреля 2018. 2 декабря 2005 года.
. DLVSYSTEM s.r.l.. Дата обращения: 16 ноября 2011. 2 января 2012 года.
. Дата обращения: 6 апреля 2018. 1 июля 2017 года.
. Дата обращения: 6 апреля 2018. 25 декабря 2017 года.
. Дата обращения: 6 апреля 2018. 4 февраля 2019 года.
. Дата обращения: 6 апреля 2018. 8 апреля 2018 года.
. Дата обращения: 6 апреля 2018. 7 марта 2017 года.
. Дата обращения: 6 апреля 2018. 24 марта 2018 года.
. Дата обращения: 6 апреля 2018. 15 ноября 2015 года.
. Дата обращения: 6 апреля 2018. 30 марта 2018 года.

Ссылки

Беляев С.А., Родионов С.В. Программирование наборов ответов: учебно-методическое пособие. СПб.: Изд-во СПбГЭТУ «ЛЭТИ», 2020. 31 с. ISBN 978-5-7629-2660-7