Программирование набора ответов - Answer set programming

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

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

История

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

Набор ответов язык программирования AnsProlog

Lparse - это имя программы, которая изначально была создана как инструмент заземления (интерфейс) для смоделей решателя наборов ответов . Язык, который принимает Lparse, теперь обычно называется AnsProlog, сокращение от Answer Set Programming in Logic . В настоящее время используется таким же образом , и во многих другом наборе ответов решателей, включая Assat , застежку , cmodels , GNT , NOMORE ++ и pbmodels . ( dlv является исключением; синтаксис программ ASP, написанных для dlv, несколько отличается.)

Программа AnsProlog состоит из правил вида

<head> :- <body> .

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

Еще одна полезная конструкция, включенная в этот язык, - это выбор . Например, правило выбора

{p,q,r}.

говорит: выберите произвольно, какой из атомов включить в стабильную модель. Программа Lparse, которая содержит это правило выбора и никаких других правил, имеет 8 стабильных моделей - произвольных подмножеств . Определение стабильной модели было обобщено на программы с правилами выбора. Правила выбора можно рассматривать также как аббревиатуры пропозициональных формул в рамках семантики стабильной модели . Например, приведенное выше правило выбора можно рассматривать как сокращение для объединения трех формул " исключенного среднего ": ${\ displaystyle p, q, r}$ ${\ Displaystyle \ {п, д, г \}}$

{\ Displaystyle (п \ лор \ нег р) \ земля (д \ лор \ нег q) \ земля (г \ лор \ нег р).}

Язык Lparse позволяет нам также писать "ограниченные" правила выбора, такие как

1{p,q,r}2.

Это правило гласит: выберите хотя бы 1 из атомов , но не более 2. Смысл этого правила в семантике стабильной модели представлен пропозициональной формулой ${\ displaystyle p, q, r}$

{\ Displaystyle (п \ лор \ нег р) \ земля (д \ лор \ нег q) \ земля (г \ лор \ нег р)}

{\ displaystyle \ land \, (p \ lor q \ lor r) \ land \ neg (p \ land q \ land r).}

Границы мощности также могут использоваться в теле правила, например:

:- 2{p,q,r}.

Добавление этого ограничения в программу Lparse удаляет стабильные модели, содержащие как минимум 2 атома . Смысл этого правила может быть представлен пропозициональной формулой ${\ displaystyle p, q, r}$

{\ displaystyle \ neg ((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.

Диапазон имеет вид:

(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 указывает смоделам найти все стабильные модели программы. Например, если файл 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

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

- раскраска из графа является функцией таким образом, что для каждой пары смежных вершин . Мы хотели бы использовать ASP для поиска раскраски данного графа (или определения того, что он не существует). ${\ displaystyle n}$ ${\ displaystyle G = \ left \ langle V, E \ right \ rangle}$ ${\ displaystyle \ mathrm {color}: от V \ to \ {1, \ dots, n \}}$ ${\ Displaystyle \ mathrm {цвет} (х) \ neq \ mathrm {цвет} (у)}$ ${\ displaystyle (x, y) \ in E}$ ${\ displaystyle 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 определяет числа как цвета. Согласно правилу выбора в строке 2, каждой вершине должен быть присвоен уникальный цвет . Ограничение в строке 3 запрещает назначать один и тот же цвет вершинам и при наличии ребра, соединяющего их. ${\ Displaystyle 1, \ точки, п}$ ${\ displaystyle i}$ ${\ displaystyle x}$ ${\ displaystyle x}$ ${\ displaystyle y}$

Если мы объединим этот файл с определением , например, ${\ displaystyle G}$

v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .

и запустите на нем смодели с числовым значением, указанным в командной строке, тогда атомы формы в выводе смоделей будут представлять собой раскраску . ${\ displaystyle n}$ ${\ Displaystyle \ mathrm {цвет} (\ точки, \ точки)}$ ${\ displaystyle n}$ ${\ displaystyle G}$

Программа в этом примере иллюстрирует организацию «генерации и тестирования», которая часто встречается в простых программах ASP. Правило выбора описывает набор «потенциальных решений» - простое надмножество множества решений данной поисковой задачи. За ним следует ограничение, которое устраняет все возможные решения, которые не являются приемлемыми. Однако процесс поиска, используемый смодлами и другими решателями наборов ответов, не основан на методе проб и ошибок .

Большая клика

Клика в графе представляет собой набор попарно смежных вершин. Следующая программа Lparse находит клику размера в заданном графе или определяет, что она не существует: ${\ displaystyle \ 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).

Это еще один пример организации «генерировать и тестировать». Правило выбора в строке 1 «генерирует» все множества, состоящие из вершин. Ограничение в строке 2 «отсеивает» множества, не являющиеся кликами. ${\ displaystyle \ geq n}$

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

Гамильтонов цикл в ориентированном графе представляет собой цикл , который проходит через каждую вершину графа ровно один раз. Следующая программа 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 «генерирует» все подмножества множества ребер. Эти три ограничения «отсеивают» подмножества, не являющиеся гамильтоновыми циклами. Последний из них использует вспомогательный предикат (« достижимо из 0») для запрета вершин, не удовлетворяющих этому условию. Этот предикат рекурсивно определяется в строках 6 и 7. ${\ Displaystyle г (х)}$ ${\ displaystyle x}$

Эта программа является примером более общей организации «генерировать, определять и тестировать»: она включает определение вспомогательного предиката, который помогает нам исключить все «плохие» потенциальные решения.

Разбор зависимостей

В обработке естественного языка , синтаксический анализ зависимостей на основе может быть сформулирован как проблема ASP. Следующий код анализирует латинское предложение «Puella pulchra in villa linguam latinam discit», «красивая девушка изучает латынь на вилле». Синтаксическое дерево выражается предикатами arc, которые представляют зависимости между словами предложения. Вычисляемая структура представляет собой линейно упорядоченное корневое дерево.

% ********** 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, abl, 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, _, _).

Стандартизация языков и конкуренция ASP

Рабочая группа по стандартизации ASP разработала стандартную языковую спецификацию, названную ASP-Core-2, к которой стремятся последние системы ASP. ASP-Core-2 - это эталонный язык для соревнований по программированию набора ответов, на котором решатели ASP периодически проверяются по ряду эталонных задач.

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

Ранние системы, такие как Smodels, использовали откат для поиска решений. По мере развития теории и практики логических решателей SAT , ряд решателей ASP был построен на основе решателей SAT, включая ASSAT и Cmodels. Они преобразовали формулу ASP в предложения SAT, применили решатель SAT, а затем преобразовали решения обратно в форму ASP. Более современные системы, такие как Clasp, используют гибридный подход, используя алгоритмы, основанные на конфликтах, вдохновленные SAT, без полного преобразования в форму логической логики. Эти подходы позволяют значительно улучшить производительность, часто на порядок, по сравнению с более ранними алгоритмами поиска с возвратом.

Проект Potassco выступает в качестве зонтика для многих из перечисленных ниже систем, включая зажимы , системы заземления ( gringo ), инкрементные системы ( iclingo ), решатели ограничений ( clingcon ), язык действий для компиляторов ASP ( coala ), распределенные реализации MPI ( claspar ). , и многие другие.

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

Реализации программирования наборов ответов на основе запросов, такие как система Galliwasp, s (ASP) и s (CASP), вообще избегают заземления за счет использования комбинации разрешения и коиндукции .

Платформа			Функции					Механика
Имя	Операционные системы	Лицензия	Переменные	Функциональные символы	Явные множества	Явные списки	Дизъюнктивная (правила выбора) поддержка
ASPeRiX	Linux	GPL	да				Нет	заземление на лету
АССАТ	Солярис	Бесплатное ПО						На основе SAT-решателя
Застежка Набор Ответов Решатель	Linux , macOS , Windows	Лицензия MIT	Да, в Clingo	да	Нет	Нет	да	инкрементальный, вдохновленный SAT-решателем (неэффективный, управляемый конфликтами)
Cmodels	Linux , Solaris	GPL	Требуется заземление				да	инкрементальный, вдохновленный SAT-решателем (неэффективный, управляемый конфликтами)
diff-SAT	Linux , macOS , Windows ( виртуальная машина Java )	Лицензия MIT	Требуется заземление				да	Вдохновленный SAT-решателем (нет, конфликтный). Поддерживает решение вероятностных задач и выборку наборов ответов
DLV	Linux , macOS , Windows	бесплатно для академического и некоммерческого образовательного использования, а также для некоммерческих организаций	да	да	Нет	Нет	да	не совместим с Lparse
DLV-Комплекс	Linux , macOS , Windows	GPL		да	да	да	да	построен на базе DLV - несовместим с Lparse
GnT	Linux	GPL	Требуется заземление				да	построен на смоделах
nomore ++	Linux	GPL						комбинированный литерал + основанный на правилах
Утконос	Linux , Solaris , Windows	GPL						распределенный, многопоточный nomore ++, смодели
Pbmodels	Linux	?						псевдобулевой решатель на основе
Смоделы	Linux , macOS , Windows	GPL	Требуется заземление	Нет	Нет	Нет	Нет
Смодельс-CC	Linux	?	Требуется заземление					На базе SAT-решателя; смодели с оговорками о конфликте
Как дела	Linux	?						На основе SAT-решателя

Languages

In other projects