Открытое или интерактивное удовлетворение ограничений

17

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

Таким образом, мне интересно узнать больше об удовлетворении ограничений, когда ограничения имеют то, что я буду называть внешними переменными , предикатами и функциями , то есть язык ограничений может иметь предикаты, такие как которые могут быть удовлетворены только путем консультации с некоторыми агент, внешний по отношению к решателю, и только тогда, когда х заземлен. Сценарий, в котором это полезно, - это всякий раз, когда P соответствует некоторому внешнему процессу принятия решения, который не может быть включен в решатель ограничений. Такие решатели ограничений можно назвать открытыми (поскольку ограничения не совсем известны) или интерактивнымип(Икс)Иксп (поскольку взаимодействие необходимо для продолжения удовлетворения ограничений).

Я хотел бы знать оба:

  • теоретические исследования, проведенные в этом направлении
  • инструменты или библиотеки, которые реализуют решатели ограничений, которые позволяют взаимодействовать с внешним миром в процессе решения ограничений.
Дэйв Кларк
источник

Ответы:

9

Я не совсем убежден предыдущей работой над открытыми и интерактивными ограничениями.

Попытка изучить вопросы управляемости была:

  • Мартин Дж. Грин и Кристофер Джефферсон, Структурная изменчивость распространенных ограничений , CP 2008. doi: 10.1007 / 978-3-540-85958-1_25

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

Я думаю, что работа над SMT (теорией выполнимости по модулю) также тесно связана с вашим вопросом. Теории SMT часто мотивируются проблемами, связанными с проверкой программного и аппаратного обеспечения, но существуют теории с искусственным интеллектом. Я с нетерпением жду новых приложений, созданных с использованием SMT в качестве основной технологии, и большей работы в условиях ограничений, применяя идеи из SMT.

Андраш Саламон
источник
1
Эта статья, безусловно, выглядит интересно. Я никогда не думал, что SMT решатели делают то, что мне нужно. Это, безусловно, проспект для изучения.
Дейв Кларк
Я смущен последним комментарием. Решатели SMT предназначены для логики и теории, а не для конкретных предикатов. Люди могут вносить новые теории и ориентиры. Я знаю, что разработчики MathSAT изучили проблемы искусственного интеллекта и планирования.
Виджай Д
@Vijay D: вы правы, это предложение излишне предвзято, и я пересмотрю его. Эффективная реализация INJECTIVE как теории SMT была опубликована в 2010 году Банковичем и Маричем ( argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf ).
Андрас Саламон
7

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

Джорджо Камерани
источник
Насколько связана / полезна книга «Исчисление вычислений: процедуры принятия решений с приложениями к проверке» Аарона Р. Брэдли и Зохара Манны? Я знаю, где копия этого находится в нескольких минутах ходьбы.
Дэйв Кларк
@Dave: Отказ от ответственности: Мой личный опыт работы с SMT только начинается ;-) Я только что посмотрел Оглавление этой книги; кажется, что есть большое пересечение между этим и тем, которое я указал. В последнем то, что вы называете здесь внешними функциями , называется там неинтерпретируемыми функциями и широко освещается. Мне не удалось найти неинтерпретируемые функции в содержании процедур принятия решений с приложениями к проверке ; однако, эта книга кажется очень хорошей, и, возможно, она может оказаться полезной.
Джорджио Камерани
@Dave: В эти дни я читаю Процедуры принятия решений - Алгоритмическая точка зрения . Я еще не дошел до главы о неинтерпретированных функциях , но если я не ошибаюсь, формулы с неинтерпретированными функциями преобразуются в формулы в Теории Равенства. Это тот случай, когда теория равенства рассматривается в процедурах принятия решений с приложениями к проверке (глава 9).
Джорджио Камерани
1
Я думаю, что Амазон звонит.
Дэйв Кларк
@Dave: ОК, отлично! ;-)
Джорджио Камерани
7

п(Икс)

Евгений Торстенсен
источник
4

Я немного смущен термином интерактив. Я поделюсь с другими и добавлю, что SMT решатель может быть полезным. В дополнение к комментарию Уолтера Бишопа доступны слайды для книги «Процедуры принятия решений» (Кренинг и Стрихман). Тщательное обращение с Джоном Харрисоном в «Руководстве по практической логике и автоматическому мышлению» также может вас заинтересовать. Пример кода доступен онлайн.

Принцесса Филиппа Рюммера поддерживает арифметику с неинтерпретированными предикатами, которые могут соответствовать тому, что вы подразумеваете под открытым. Он написан на Scala, использует E-match при обработке количественного определения и предоставляет интерполанты.

Виджай Д
источник
0

Что касается инструментов, если вы решите использовать Prolog в качестве языка выбора, я могу предложить несколько подходов к реализации:

  • GNU Prolog with - это библиотека программирования C. Вы можете вызывать функции C из Prolog и Prolog из C. Это открывает вам множество возможностей расширения функциональности. Pro: Gnu Prolog - один из самых быстрых свободно доступных компиляторов Prolog. Примечание: некоторые люди жалуются на отсутствие некоторых встроенных предикатов ... на самом деле большинство из них могут быть реализованы, посмотрите слои совместимости Prolog @ SO
  • SWI-Prolog имеет интересную библиотеку программирования, включая сетевое взаимодействие, поддержку протокольных буферов и т. Д. И довольно популярен.
  • XSB Prolog некоторые люди утверждают, что это наиболее интересный проект с точки зрения взаимодействия - в том числе: интерфейсы баз данных и т. Д.

Prolog - это язык программирования, который подходит для многих видов решателей (и у большинства из них есть конечные доменные решатели).

Гжегож Вежовецкий
источник