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

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

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

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

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

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

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

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

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

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

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

$\mathbf P(x)$

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

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

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

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

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