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

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

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

История

Ранним примером программирования наборов ответов был метод планирования , предложенный в 1997 году Димопулосом, Небелем и Кёлером. ^[3]^[4] Их подход основан на связи между планами и стабильными моделями. ^[5] В 1998 году Сойнинен и Ниемеля ^[6] применили то, что сейчас известно как программирование наборов ответов, к проблеме конфигурации продукта . ^[4] В 1999 году термин «программирование наборов ответов» впервые появился в книге «Парадигма логического программирования» как название сборника из двух статей. ^[4] Первая из этих статей определила использование решателей наборов ответов для поиска как новую парадигму программирования . ^[7] В том же году Ниемеля также предложил «логические программы со стабильной семантикой модели» в качестве новой парадигмы. ^[8]

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

Lparse — это название программы, которая изначально была создана как инструмент заземления (front-end) для решателя набора ответов smodels. Язык, который принимает Lparse, теперь обычно называется AnsProlog, ^[9] сокращение от Answer Set Programming in Logic . ^[10] Теперь он используется таким же образом во многих других решателях наборов ответов, включая assat, clasp, cmodels, gNt, nomore++ и pbmodels. (dlv является исключением; синтаксис программ ASP, написанных для dlv, несколько отличается.)

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

< голова >  :-  < тело >  .

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

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

{ п , д , р }.

говорит: выберите произвольно, какой из атомов включить в стабильную модель. Программа Lparse, которая содержит это правило выбора и никаких других правил, имеет 8 стабильных моделей — произвольные подмножества . Определение стабильной модели было обобщено на программы с правилами выбора. ^[11] Правила выбора можно также рассматривать как сокращения для пропозициональных формул в рамках семантики стабильной модели . ^[12] Например, правило выбора выше можно рассматривать как сокращение для конъюнкции трех формул « исключенного третьего »: $p,q,r$ $\{p,q,r\}$

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

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

1 { п , д , р } 2.

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

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

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

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

:-  2 { п , д , г }.

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

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

имеет то же значение, что и

п ( а ).  п ( б ).  п ( в ). кв ( б ).  кв ( в ).

Программа

п ( а ).  п ( б ).  п ( в ). { q ( X ):- п ( X )} 2.

это сокращение от

п ( а ).  п ( б ).  п ( в ). { д ( а ),  д ( б ),  д ( в )} 2.

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

( начало .. конец )

где start и end — константные арифметические выражения. Диапазон — это сокращенная форма записи, которая в основном используется для определения числовых доменов совместимым способом. Например, факт

а ( 1..3 ).

это сокращение для

а ( 1 ).  а ( 2 ).  а ( 3 ).

Диапазоны также можно использовать в текстах правил с той же семантикой.

Условный литерал имеет вид:

р ( Х ) : д ( Х )

Если расширение qесть {q(a1), q(a2), ..., q(aN)}, то указанное выше условие семантически эквивалентно написанию {p(a1), p(a2), ..., p(aN)}на месте условия. Например,

q ( 1..2 ). a  :-  1  { p ( X ) : q ( X )}.

это сокращение от

д ( 1 ).  д ( 2 ). а  :-  1  { п ( 1 ),  п ( 2 )}.

Создание стабильных моделей

Чтобы найти стабильную модель программы Lparse, хранящуюся в файле, ${filename}мы используем команду

% lparse ${ имя_файла } | smodels

Опция 0 предписывает smodels найти все стабильные модели программы. Например, если файл testсодержит правила

1 { p , q , r } 2. s  :-  не  p .

затем команда выдает вывод

% lparse test | smodels 0 Ответ: 1 Стабильная модель: qp Ответ: 2 Стабильная модель: p Ответ: 3 Стабильная модель: rp Ответ: 4 Стабильная модель: qs Ответ: 5 Стабильная модель: rs Ответ: 6 Стабильная модель: rqs

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

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

-Раскраска графа — это функция , такая что для каждой пары смежных вершин . Мы хотели бы использовать ASP, чтобы найти -раскраску заданного графа ( или определить, что она не существует). $n$ $G=\left\langle V,E\right\rangle$ $\mathrm {цвет} :V\to \{1,\точки,n\}$ $\mathrm {color} (x)\neq \mathrm {color} (y)$ $(x,y)\in E$ $n$

Это можно сделать с помощью следующей программы Lparse:

в ( 1. . н ). 1  { цвет ( X , I )  :  c ( I )}  1  :-  v ( X ). :-  цвет ( X , I ),  цвет ( Y , I ),  e ( X , Y ),  c ( I ).

Строка 1 определяет числа, которые будут цветами. Согласно правилу выбора в строке 2, каждой вершине должен быть назначен уникальный цвет . Ограничение в строке 3 запрещает назначать один и тот же цвет вершинам , если есть ребро, соединяющее их. $1,\dots ,n$ $i$ $x$ $x$ $y$

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

v ( 1..100 ).  % 1,...,100 — вершины e ( 1 , 55 ).  % существует ребро из 1 в 55 .  .  .

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

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

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

Клика в графе — это набор попарно смежных вершин. Следующая программа Lparse находит клику размера в заданном ориентированном графе или определяет, что она не существует: $\geq n$

н  { в ( X )  :  v ( X )}.:-  в ( X ),  в ( Y ),  X ! = Y ,  а не  e ( X , Y ).

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

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

Гамильтонов цикл в ориентированном графе — это цикл , который проходит через каждую вершину графа ровно один раз. Следующая программа Lparse может быть использована для поиска гамильтонова цикла в заданном ориентированном графе, если он существует; мы предполагаем, что 0 — одна из вершин.

{ в ( X , Y )}  :-  е ( X , Y ).:-  2  { в ( X , Y )  :  е ( X , Y )},  v ( X ).:-  2  { в ( X , Y )  :  е ( X , Y )},  v ( Y ).r ( X )  :-  in ( 0 , X ),  v ( X ).г ( Y )  :-  г ( X ),  в ( X , Y ),  е ( X , Y ).:-  не  r ( X ),  v ( X ).

Правило выбора в строке 1 «генерирует» все подмножества множества ребер. Три ограничения «отсеивают» подмножества, которые не являются гамильтоновыми циклами. Последнее из них использует вспомогательный предикат (« достижимо из 0»), чтобы запретить вершины, не удовлетворяющие этому условию. Этот предикат определяется рекурсивно в строках 6 и 7. $r(x)$ $x$

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

Анализ зависимостей

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

% ********** введите предложение ********** слово ( 1 ,  puella ).  слово ( 2 ,  пульхра ).  слово ( 3 ,  в ).  слово ( 4 ,  вилла ).  слово ( 5 ,  язык ).  слово ( 6 ,  лат. ).  слово ( 7 ,  дисцит ). % ********** лексикон ********** 1 {  node ( X ,  attr ( pulcher ,  a ,  fem ,  nom ,  sg ));  узел ( X ,  attr ( pulcher ,  a ,  fem ,  abl ,  sg ))  } 1  :-  слово ( X ,  pulchra ). узел ( X ,  attr ( latinus ,  a ,  fem ,  acc ,  sg ))  :  -word ( X ,  latinam ). 1 {  узел ( X ,  attr ( puella ,  n ,  fem ,  nom ,  sg ));  узел ( X ,  атрибут ( puella ,  n ,  fem ,  abl ,  sg ))  } 1  :-  слово ( X ,  puella ). 1 {  узел ( X ,  атрибут ( villa ,  n ,  fem ,  nom ,  sg ));  узел ( X ,  attr ( вилла ,  н ,  жен ,  абл ,  ед ))  } 1  :-  слово ( X,  вилла ). узел ( X ,  атрибут ( linguam ,  n ,  fem ,  acc ,  sg ))  :-  слово ( X ,  linguam ). узел ( X ,  атрибут ( discere ,  v ,  pres ,  3 ,  sg ))  :-  слово ( X ,  discit ). узел ( X ,  атрибут ( in ,  p ))  :-  слово ( X ,  in ). % ********** синтаксические правила ********** 0 {  дуга ( X ,  Y ,  subj )  } 1  :-  узел ( X ,  атрибут ( _ ,  v ,  _ ,  3 ,  sg )),  узел ( Y ,  атрибут ( _ ,  n ,  _ ,  nom ,  sg )). 0 {  дуга ( X ,  Y ,  dobj )  } 1  :-  узел ( X ,  атрибут ( _ ,  v ,  _ ,  3 ,  sg )),  узел ( Y ,  атрибут ( _ ,  n ,  _ ,  acc ,  sg )). 0 {  дуга ( X ,  Y ,  атрибут )  } 1  :-  узел ( X ,  атрибут ( _ ,  n ,  Пол ,  Случай ,  Число )),  узел ( Y ,  атрибут ( _ ,  a ,  Пол ,  Случай,  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 )),  не  leaf ( Y ). % ********** гарантируя древовидность графа ********** 1 {  root ( X ) : node ( X ,  _ )  } 1. :-  arc ( X ,  Z ,  _ ),  arc ( Y ,  Z ,  _ ),  X  ! =  Y . :-  дуга ( X ,  Y ,  L1 ),  дуга ( X ,  Y ,  L2 ),  L1  ! =  L2 . путь ( X ,  Y )  :-  дуга ( X ,  Y ,  _ ). путь ( X ,  Z )  :-  дуга ( X ,  Y ,  _ ),  путь ( Y ,  Z ). :-  путь ( X ,  X ). :-  корень ( X ),  узел ( Y,  _ ),  X  ! =  Y ,  а не  путь ( X ,  Y ). лист ( X )  :-  узел ( X ,  _ ), а  не  дуга ( X ,  _ ,  _ ).

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

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

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

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

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

Большинство систем поддерживают переменные, но только косвенно, принудительно заземляя, используя систему заземления, такую как Lparse или gringo в качестве front-end. Необходимость заземления может вызвать комбинаторный взрыв предложений; таким образом, системы, которые выполняют заземление на лету, могут иметь преимущество. ^[15]

Реализации программирования наборов ответов, основанные на запросах, такие как система Galliwasp ^[16] и s(CASP) ^[17], полностью избегают заземления, используя комбинацию резолюции и коиндукции .

Смотрите также

Ссылки

^ Барал, Читта (2003). Представление знаний, рассуждения и декларативное решение проблем . Cambridge University Press. ISBN 978-0-521-81802-5.
^ Гельфонд, Майкл (2008). «Наборы ответов». В ван Хармелен, Франк; Лифшиц, Владимир; Портер, Брюс (ред.). Справочник по представлению знаний . Elsevier. стр. 285–316. ISBN 978-0-08-055702-1.в формате PDF Архивировано 2016-03-03 на Wayback Machine
^ Dimopoulos, Y.; Nebel, B .; Köhler, J. (1997). «Кодирование проблем планирования в немонотонных логических программах». В Steel, Sam; Alami, Rachid (ред.). Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, France, September 24–26, 1997, Proceedings. Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence. Vol. 1348. Springer. pp. 273–285. ISBN 978-3-540-63912-1.как постскриптум
^ abc Лифшиц, Владимир (13 июля 2008 г.). «Что такое программирование набора ответов?» (PDF) . Труды 23-й Национальной конференции по искусственному интеллекту . 3. AAAI Press: 1594–1597.
^ Субраманян, В.С.; Заниоло, К. (1995). «Связь стабильных моделей и областей планирования ИИ». В Sterling, Leon (ред.). Логическое программирование: Труды Двенадцатой международной конференции по логическому программированию . MIT Press. стр. 233–247. ISBN 978-0-262-69177-2.как постскриптум
^ Сойнинен, Т.; Ниемеля, И. (1998), Формализация знаний о конфигурации с использованием правил с выбором (Postscript) , Лаборатория науки обработки информации, Хельсинкский технологический университет
^ Марек, В.; Трушчинский, М. (20 мая 1999 г.). «Стабильные модели и альтернативная парадигма логического программирования». В Apt, Кшиштоф Р. (ред.). Парадигма логического программирования: 25-летняя перспектива (PDF) . Springer. стр. 169–181. arXiv : cs/9809032 . ISBN 978-3-540-65463-6.
^ Ниемеля, И. (ноябрь 1999 г.). «Логические программы со стабильной семантикой модели как парадигма программирования ограничений» (Postscript, gzip) . Annals of Mathematics and Artificial Intelligence . 25 (3/4): 241–273. doi :10.1023/A:1018930122475. S2CID 14465318.
^ Крик, Том (2009). Супероптимизация: доказуемо оптимальная генерация кода с использованием программирования набора ответов (PDF) (Ph.D.). Университет Бата. Доктет 20352. Архивировано из оригинала (PDF) 2016-03-04 . Получено 2011-05-27 .
^ Рохелио Давила. «АнсПролог, обзор» (PowerPoint) .
^ Ниемеля, И.; Саймонс, П.; Сойненен, Т. (2000). "Семантика стабильной модели правил ограничения веса". В Гельфонд, Майкл; Леоне, Николь; Пфайфер, Джеральд (ред.). Логическое программирование и немонотонные рассуждения: 5-я международная конференция, LPNMR '99, Эль-Пасо, Техас, США, 2–4 декабря 1999 г. Труды . Конспект лекций по информатике: Конспект лекций по искусственному интеллекту. Том 1730. Springer. С. 317–331. ISBN 978-3-540-66749-0.как постскриптум
^ Феррарис, П.; Лифшиц, В. (январь 2005 г.). «Ограничения веса как вложенные выражения». Теория и практика логического программирования . 5 (1–2): 45–74. arXiv : cs/0312045 . doi :10.1017/S1471068403001923. S2CID 5051610.как постскриптум
^ "Разбор зависимостей". Архивировано из оригинала 2015-04-15 . Получено 2015-04-15 .
^ "Спецификация языка ввода ASP-Core-2" (PDF) . Получено 14 мая 2018 г.
^ Лефевр, Клэр; Беатрикс, Кристофер; Стефан, Игорь; Гарсия, Лоран (май 2017 г.). «ASPeRiX, подход прямого построения цепочек первого порядка для вычисления множества ответов*». Теория и практика логического программирования . 17 (3): 266–310. arXiv : 1503.07717 . doi :10.1017/S1471068416000569. ISSN 1471-0684. S2CID 2371655.
^ Марпл, Кайл.; Гупта, Гопал. (2012). «Galliwasp: Целенаправленный решатель множества ответов». В Альберт, Эльвира (ред.). Логико-ориентированный синтез программ и преобразование, 22-й международный симпозиум, LOPSTR 2012, Лёвен, Бельгия, 18–20 сентября 2012 г., пересмотренные избранные статьи . Springer. стр. 122–136.
^ Ариас, Дж.; Карро, М.; Салазар, Э.; Марпл, К.; Гупта, Г. (2018). «Программирование набора ответов с ограничениями без заземления». Теория и практика логического программирования . 18 (3–4): 337–354. arXiv : 1804.11162 . doi : 10.1017/S1471068418000285 . S2CID 13754645.
^ ab "Страница компании DLV System". DLVSYSTEM srl . Получено 16 ноября 2011 г. .

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

Спецификация языка ввода ASP-Core-2 2.03c
Первый конкурс систем ASP
Второй конкурс ASP
Третий конкурс ASP
Четвертый конкурс ASP
Утконос
Различные решатели наборов ответов, упакованные для Debian / Ubuntu
Застежка Ответ Набор Решатель