Проблема удовлетворенности ограничением (CSP) и выполнимость по модулю теории (SMT); с кодой на программировании ограничений

Кто-нибудь осмелится попытаться выяснить, какова связь между этими областями обучения или, возможно, даже дать более конкретный ответ на уровне проблем? Например, включает в себя некоторые общепринятые формулировки. Если я правильно понял, когда вы переходите от SAT к SMT, вы в основном входите в поле CSP; наоборот, если вы ограничиваете CSP булевыми значениями, вы в основном говорите о SAT и, возможно, о некоторых связанных проблемах, таких как #SAT. Я думаю, что это ясно (например, глава Колайтиса и Варди «Логический подход к удовлетворению ограничений» в теории конечных моделей и ее приложениях).Грэделом и др.), но что мне менее ясно, когда ограничения «по модулю теории», а когда нет? Всегда ли SMT подразумевает, что теория использует только равенство, а ограничения неравенства всегда находятся в более широкой области CSP? Насколько я могу судить, вы можете часто вводить слабые переменные , поэтому различие [если оно существует] менее чем очевидно.

Относительно недавний «Справочник по удовлетворенности» (IOP Press 2009) объединяет проблемы как SMT, так и CSP в рамках своего широкого «зонда удовлетворенности», но, учитывая его структуру (главы, написанные различными авторами), на самом деле не помогает мне понять это ,

Я надеюсь, что терминология становится менее запутанной, когда вы говорите о программировании ограничений , которое (по аналогии с термином «математическое программирование»), я надеюсь, предполагает минимизацию / максимизацию некоторой целевой функции. Статья в Википедии, посвященная программированию с ограничениями, увы, настолько расплывчата, что я не могу точно сказать, происходит ли это кадрирование. Фрувирт и Абденнадхер (стр. 56) могут извлечь из « Основы программирования ограничений» то, что «решатель ограничений» обычно предоставляет больше, чем просто средство проверки удовлетворенности, с упрощением и т. Д., Которое важно на практике.

Хотя это вряд ли актуальный вопрос исследования теории CS, я не ожидаю хороших ответов на этот вопрос на сайте бакалавриата CS.SE, учитывая то, что я видел по адресу https://cs.stackexchange.com/questions/14946/distinguish- Решение-процедура-против-smt-решатель-против-теорема-доказатель-против-ограничение-соль (который содержит много слов, но не то, что я бы посчитал реальным ответом, увы).

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

Основываясь на моей дипломной работе по структурной теории CSP , я пришел к выводу, что понятие «структура предложения» необходимо для объединения всех этих парадигм и понимания их различий. Каждое предложение экземпляра SAT представляет собой запрещенное частичное присвоение; предложение типа запрещает частичное присваивание которое одновременно устанавливает для и значение false, а для значение false правда. Структура предложения задачи комбинаторной оптимизации - это ее представление в качестве экземпляра SAT с использованием некоторого подходящего кодирования. Тем не менее, структура предложения включает в себя все$x_1 \lor \overline{x_2} \lor x_3$$\{(x_1,0),(x_2,1),(x_3,0)\}$$x_1$$x_3$$x_2$запрещенные частичные задания, а не только те, которые даны в начале. Следовательно, структура предложения обычно слишком велика, чтобы манипулировать ею напрямую: обычно она имеет по меньшей мере экспоненциальный размер числа переменных и может быть бесконечной. Следовательно, структура предложения должна быть аппроксимирована с ограниченным пространством. SAT / CP / SMT / ASP поддерживает и обновляет более или менее неявное представление базовой структуры предложения. Это возможно, потому что если известно, что одно частичное присвоение находится в структуре предложения, то это подразумевает, что также присутствует много других предложений. Например, приведенное выше предложение SAT также запрещает любое частичное присваивание, которое содержит его в качестве подмножества, поэтому такие предложения, как и$x_1 \lor \overline{x_2} \lor x_3 \lor x_4$$x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$ находятся в структуре предложения этого экземпляра.

Аппроксимация структуры предложения сохраняется для того, чтобы сузить набор решений и помочь определить, является ли этот набор пустым. Во время поиска некоторые частичные назначения могут оказаться не содержащимися в каком-либо решении (даже если они индивидуально удовлетворяют каждому из ограничений в экземпляре). Они известны как nogoods , термин, введенный («Мистер GNU») Столлманом и Суссманом, Следовательно, хорошее предложение входит в структуру предложения и может быть включено в аппроксимацию структуры предложения как компактное представление многих предложений, которые можно исключить из поиска решений. Добавление nogoods в структуру приближенного предложения сохраняет все решения, но лучше приближает эти решения. Таким образом, примерная структура предложения обычно изменяется в процессе поиска. Кроме того, способ моделирования проблемы в одном из подходов комбинаторной оптимизации влияет на структуру предложения, часто весьма существенно. Например, пропозициональные переменные могут представлять интервалы, такие как или точки, такие как$x \le 5$$x = 5$, Следовательно, не существует единой общей структуры предложений, но она связана с каждым выбором представления, в зависимости от того, что представляют синглеты (литералы) структуры предложения.

Зависимое программирование (СР) традиционно было дисциплиной ИИ с упором на планирование, составление графиков и комбинаторные задачи, и поэтому играет центральную роль для переменных, которые могут принимать более двух значений (но обычно только конечное число). CP подчеркнул эффективный поиск и, руководствуясь традиционными приложениями, отводил центральную роль all-differentограничению (инъективности), но также разработал эффективные пропагаторы для многих других видов ограничений. Формальные определения CP существуют примерно с 1974 года, когда Монтанари опубликовал « Сети ограничений».с прекурсорами, возвращающимися еще раньше. Этот вес истории, возможно, способствовал отставанию CP от других подходов в исходной производительности за последнее десятилетие. CP классически поддерживает приближение дополнения к структуре предложения через набор активных областей для переменных. Цель состоит в том, чтобы исключить значения из активных доменов, исследуя структуру предложения, пытаясь назначить значения-кандидаты переменным и возвращая их при необходимости.

Теории удовлетворенности по модулю (SMT) вышли из сообщества верификаторов. Каждая теория в SMT-решателе формирует неявное представление потенциально бесконечного числа SAT-предложений. Теории, используемые с SMT, и ограничения, используемые в CP, отражают их различные исторические применения. Большинство теорий, которые рассматривает SMT, имеют отношение к массивам с целочисленными индексами, реальным замкнутым полям, линейным порядкам и т. П .; они возникают в результате статического анализа программ (при верификации с помощью компьютера) или при формализации математических доказательств (при автоматическом рассуждении). Напротив, при составлении расписаний и расписании ограничение на приемистость является центральным, и хотя стандартный язык SMTLIB имеет ограничения на приемистость с момента его создания в 2003 г. (черезdistinctсимвол), до 2010 года решатели SMT реализовывались только distinctнаивным алгоритмом. На этом этапе метод all-differentпереноса из стандартного пропагатора CP для был перенесен, что дало большой эффект при применении к большим спискам переменных; см . Решатель ограничений Alldifferent в SMT , Банкович и Марич, SMT 2010. Более того, большинство пропагаторов CP предназначены для задач с конечными областями, тогда как стандартные теории SMT имеют дело с бесконечными областями (целыми числами, а в последнее время и действительными) из коробки. SMT использует экземпляр SAT в качестве аппроксимации структуры предложений, извлекая из них полезные предложения, если необходимо. Хороший обзор - « Теория удовлетворенности по модулю: введение и применение » Де Мора и Бьорнер, doi: 10.1145 / 1995376.1995394,

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

Формально SAT - это CSP для булевых доменов, но в SAT основное внимание уделяется изучению предложений, хорошей эвристике для обнаружения конфликтов и быстрым способам возврата назад, что отличается от традиционного подхода CSP к пропагаторам, установлению согласованности и эвристике для переменного порядка. SAT обычно чрезвычайно эффективен, но для многих проблем требуются огромные усилия, чтобы сначала выразить проблему как экземпляр SAT. Использование парадигмы более высокого уровня, такой как CP, может позволить более естественное выражение проблемы, и тогда либо экземпляр CP может быть переведен в SAT вручную, либо инструмент может позаботиться о переводе. Хороший обзор основных моментов SAT - « О современных решениях по удовлетворению условий обучения », авторы Pipatsrisawat и Darwiche, doi: 10.1007 / s10817-009-9156-3 .

Теперь давайте перейдем от общности к сегодняшней специфике.

За последнее десятилетие некоторые люди в CP начали концентрироваться на создании ленивых предложений (LCG). По сути, это способ объединить пропагаторы CP вместе, используя более гибкие SMT-подобные методы, а не довольно жесткую абстракцию активных доменов. Это полезно, потому что существует длинная история опубликованных пропагаторов CP для эффективного представления и решения многих видов проблем. (Конечно, подобный эффект был бы достигнут совместными усилиями по внедрению новых теорий для SMT-решателей.) LCG обладает характеристиками, которые часто конкурируют с SMT, и для некоторых проблем он может быть лучше. Краткий обзор статьи Stuckey CPAIOR 2010 Lazy Clause Generation: объединение возможностей решения SAT и CP (и MIP?) , Doi: 10.1007 / 978-3-642-13520-0_3, Стоит также прочитать документ с изложением позиции Гарсиа де ла Банды, Штуки, Ван Хентенрика и Уоллеса, в котором описывается CP-ориентированное видение « Технологии будущего оптимизации» , doi: 10.1007 / s10601-013-9149-z .

Насколько я могу судить, большая часть недавних исследований SMT, похоже, сместилась к приложениям в формальных методах и формализованной математике. Примером является реконструкция доказательств, найденных SMT-решателями внутри систем доказательств, таких как Изабель / HOL, путем построения тактики Изабель / HOL для отражения правил вывода в следах SMT-доказательств; см. « Быстрая реконструкция в стиле LCF для Z3 » Бёмера и Вебера на ITP 2010.

За последние несколько лет лучшие решения для ASP были разработаны для того, чтобы стать конкурентоспособными с решениями для CP, SMT и SAT. Я лишь смутно знаком с деталями реализации, которые позволили решателям, таким как claspбыть конкурентоспособными, поэтому не может реально сравнить их с SMT и CP, но clasp явно рекламирует свое внимание к изучению nogoods.

Пересечение традиционных границ между этими формализмами является переводом из более абстрактных представлений проблемы в эффективно реализуемые формализмы более низкого уровня. Некоторые из лучших решателей ASP и CP теперь явно переводят свои входные данные в экземпляр SAT, который затем решается с использованием готового решателя SAT. В CP помощник по моделированию ограничений Savile Row использует методы проектирования компилятора для перевода проблем, выраженных на языке Essence среднего уровня, в формализм более низкого уровня, подходящий для ввода в решатели CP, такие как Minion или MiniZinc . Первоначально Savile Row работал с представлением CP в качестве формализма низкого уровня, но в версии 1.6.2 в качестве цели был выбран SAT. Более того, языковая сущность еще более высокого уровнятеперь может быть автоматически переведен в Essence с помощью инструмента Conjure . В то же время низкоуровневые решатели, предназначенные только для SAT, такие как Lingeling, продолжают совершенствоваться каждый год, причем совсем недавно, поочередно на этапах обучения и обработки; см. краткий обзор « Что нового в соревнованиях SAT и ASP» от Heule и Schaub в AAAI 2015.

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