WikiSort.ru - Программирование

ПОИСК ПО САЙТУ | о проекте

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

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

История

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

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

Lparse —это название программы, которая изначально была создана как инструмент заземлення (англ. Symbol grounding problem) для решателя smodels. Язык, который принимает Lparse, называется AnsProlog. На сегодня, она используется как самостоятельно, так и в множестве других решателей, таких, как 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))$ .

Переменные (в верхнем регистре, как и в Прологе), используются в 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 вершины
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	Linux	GPL	Да				Нет	обоснование «на лету»
ASSAT	Solaris	Бесплатная						основан на SAT-решателе
Clasp Answer Set Solver	Linux, macOS, Windows	GPL	Да	Да	Нет	Нет	Да	основан на SAT-решателе
Cmodels	Linux, Solaris	GPL	Требует обоснования				Да	основан на SAT-решателе
DLV	Linux, macOS, Windows^[4]	Бесплатная для академического и некоммерческого использования	Да	Да	Нет	Нет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-решателе

Ссылки

↑ 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
1 2 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ä, Simons, Soinenen. — Springer, 2000. — Vol. 1730. — P. 317–331. — ISBN 978-3-540-66749-0. as Postscript
↑ Dependency parsing (неопр.) (недоступная ссылка). Проверено 6 апреля 2018. Архивировано 15 апреля 2015 года.
↑ DLV System company page (неопр.). DLVSYSTEM s.r.l.. Проверено 16 ноября 2011.

Ссылки

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .

Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии

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

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

[:3-3] Dependency parsing (неопр.) (недоступная ссылка). Проверено 6 апреля 2018. Архивировано 15 апреля 2015 года.

[dlvsystem.com-4] DLV System company page (неопр.). DLVSYSTEM s.r.l.. Проверено 16 ноября 2011.