Программирование логики ограничений - Constraint logic programming

Логическое программирование с ограничениями - это форма программирования с ограничениями , в которой логическое программирование расширяется за счет включения концепций удовлетворения ограничений . Программа логики ограничений - это логическая программа, которая содержит ограничения в теле предложений. Пример пункта , включая ограничение есть . В этом разделе - ограничение; , и являются литералами, как в обычном логическом программировании. В этом пункте указано одно условие, при котором выполняется утверждение : больше нуля и оба и верны. A(X,Y) :- X+Y>0, B(X), C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

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

Обзор

Формально программы с логикой ограничений похожи на обычные логические программы, но тело предложений может содержать ограничения в дополнение к обычным литералам логического программирования. Например, X>0это ограничение, которое включено в последний пункт следующей логической программы ограничения.

B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).

Как и в обычном логическом программировании, оценка цели, например, A(X,1)требует оценки тела последнего предложения с помощью Y=1. Как и в обычном логическом программировании, это, в свою очередь, требует доказательства цели B(X,1). В отличие от обычного логического программирования, это также требует удовлетворения ограничения:, X>0ограничение в теле последнего предложения (в обычном логическом программировании X> 0 не может быть доказано, если X не привязан к полностью основному члену и выполнение программа завершится ошибкой, если это не так).

Не всегда можно определить, удовлетворяется ли ограничение, когда оно встречается. В этом случае, например, значение Xне определяется при оценке последнего предложения. В результате X>0на данном этапе ограничение не выполняется и не нарушается. Вместо того, чтобы продолжать оценку B(X,1)и затем проверять, является ли полученное значение Xположительным, интерпретатор сохраняет ограничение X>0и затем переходит к оценке B(X,1); таким образом, интерпретатор может обнаружить нарушение ограничения X>0во время оценки B(X,1)и немедленно вернуться назад, если это так, вместо того, чтобы ждать завершения оценки B(X,1).

В общем, оценка логической программы ограничений выполняется так же, как и обычная логическая программа. Однако ограничения, обнаруженные во время оценки, помещаются в набор, называемый хранилищем ограничений. Например, оценка цели A(X,1)выполняется путем оценки тела первого предложения с помощью Y=1; эта оценка пополняет X>0запас ограничений и требует B(X,1)подтверждения цели . При попытке доказать эту цель применяется первое предложение, но его оценка добавляется X<0к хранилищу ограничений. Это добавление делает хранилище ограничений неудовлетворительным. Затем интерпретатор возвращается назад, удаляя последнее добавление из хранилища ограничений. Оценка второго предложения добавляет X=1и Y>0к хранилищу ограничений. Поскольку хранилище ограничений выполнимо и не осталось доказательств другого литерала, интерпретатор останавливается на решении X=1, Y=1.

Семантика

Семантика программ логики ограничений может быть определена в терминах виртуального интерпретатора, который поддерживает пару во время выполнения. Первый элемент этой пары называется текущей целью; второй элемент называется хранилищем ограничений. Цель содержит литералы интерпретатор пытается доказать , и может также содержать некоторые ограничения его пытаются удовлетворить; ограничение магазин содержит все ограничения , интерпретатор взятые выполним до сих пор. ${\ displaystyle \ langle G, S \ rangle}$

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

Подробности анализа удаленного от цели литерала заключаются в следующем. После удаления этого литерала с передней части ворот проверяется, является ли он ограничением или литералом. Если это ограничение, оно добавляется в хранилище ограничений. Если это литерал, выбирается предложение, в заголовке которого содержится такой же предикат литерала; предложение переписывается путем замены его переменных новыми переменными (переменные, не входящие в цель): результат называется новым вариантом предложения; затем перед воротами помещается текст нового варианта предложения; равенство каждого аргумента литерала соответствующему аргументу из нового варианта head также помещается перед целью.

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

Интерпретатор доказал цель, когда текущая цель пуста и хранилище ограничений не обнаружено неудовлетворительным. Результат выполнения - текущий набор (упрощенных) ограничений. Этот набор может включать в себя ограничения, такие как принуждение переменных к определенному значению, но также может включать такие ограничения, как только связанные переменные, не давая им определенного значения. ${\ Displaystyle X = 2}$${\ displaystyle X> 2}$

Формально семантика программирования логики ограничений определяется в терминах производных . Замечено, что переход - это пара пар цель / запас . Такая пара заявляет о возможности перехода от штата к штату . Такой переход возможен в трех возможных случаях: ${\ displaystyle \ langle G, S \ rangle \ rightarrow \ langle G ', S' \ rangle}$${\ displaystyle \ langle G, S \ rangle}$${\ Displaystyle \ langle G ', S' \ rangle}$

• элемент G является ограничением C , и ; другими словами, ограничение можно переместить из цели в хранилище ограничений.${\ displaystyle G '= G \ обратная косая черта \ {C \}}$${\ Displaystyle S '= S \ чашка \ {C \}}$
• элемент G является литералом , существует предложение, которое, переписанное с использованием новых переменных, is , is G с замененным на , и ; другими словами, литерал может быть заменен телом нового варианта предложения с тем же предикатом в заголовке, добавив к цели тело нового варианта и указанные выше равенства терминов.${\ Displaystyle L (т_ {1}, \ ldots, т_ {п})}$${\ displaystyle L (t_ {1} ', \ ldots, t_ {n}'): - B}$${\ displaystyle G '}$${\ Displaystyle L (т_ {1}, \ ldots, т_ {п})}$${\ displaystyle t_ {1} = t_ {1} ', \ ldots, t_ {n} = t_ {n}', B}$${\ displaystyle S '= S}$
• S и эквивалентны в соответствии с семантикой конкретных ограничений${\ displaystyle S '}$

Последовательность переходов - это производное. Цель G может быть доказана , если существует вывод из в течение некоторого выполнимой ограничение магазин S . Эта семантика формализует возможные варианты развития интерпретатора, который произвольно выбирает литерал цели для обработки и предложение для замены литералов. Другими словами, цель доказывается в соответствии с этой семантикой, если существует последовательность выбора литералов и предложений, среди возможно многих, которые приводят к пустой цели и выполнимому хранилищу. ${\ Displaystyle \ langle G, \ emptyset \ rangle}$${\ Displaystyle \ langle \ emptyset, S \ rangle}$

Фактические интерпретаторы обрабатывают элементы цели в порядке LIFO : элементы добавляются спереди и обрабатываются спереди. Они также выбирают пункт второго правила в соответствии с порядком, в котором они написаны, и перезаписывают хранилище ограничений при его изменении.

Третий возможный вид перехода - это замена хранилища ограничений эквивалентным. Эта замена ограничена теми, которые выполняются определенными методами, такими как распространение ограничений . Семантика программирования логики ограничений является параметрической не только для типа используемых ограничений, но и для метода переписывания хранилища ограничений. Конкретные методы, используемые на практике, заменяют хранилище ограничений на более простое для решения. Если хранилище ограничений неудовлетворительно, это упрощение может иногда обнаруживать эту неудовлетворенность, но не всегда.

Результат оценки цели по логической программе ограничений определяется, если цель доказана. В этом случае существует переход от исходной пары к паре, где цель пуста. Хранилище ограничений этой второй пары считается результатом оценки. Это связано с тем, что хранилище ограничений содержит все ограничения, которые считаются выполнимыми для подтверждения цели. Другими словами, цель доказана для всех оценок переменных, которые удовлетворяют этим ограничениям.

Попарное равенство членов двух литералов часто компактно обозначают : это сокращение для ограничений . Общий вариант семантики для программирования логики ограничений добавляет непосредственно к хранилищу ограничений, а не к цели. ${\ Displaystyle L (t_ {1}, \ ldots, t_ {n}) = L (t_ {1} ', \ ldots, t_ {n}')}$${\ displaystyle t_ {1} = t_ {1} ', \ ldots, t_ {n} = t_ {n}'}$${\ Displaystyle L (t_ {1}, \ ldots, t_ {n}) = L (t_ {1} ', \ ldots, t_ {n}')}$

Условия и положения

Используются разные определения терминов, порождающие различные виды программирования логики ограничений: над деревьями, вещественными числами или конечными областями. Своеобразным ограничением, которое всегда присутствует, является равенство условий. Такие ограничения необходимы, потому что интерпретатор добавляет t1=t2к цели всякий раз, когда литерал P(...t1...)заменяется телом свежего варианта предложения, голова которого равна P(...t2...).

Термины дерева

Программирование логики ограничений с помощью терминов дерева имитирует программирование обычной логики, сохраняя подстановки как ограничения в хранилище ограничений. Термины - это переменные, константы и функциональные символы, применяемые к другим терминам. Единственные рассматриваемые ограничения - это равенство и неравенство между терминами. Равенство особенно важно, поскольку подобные ограничения t1=t2часто создаются интерпретатором. Ограничения по условиям равенства можно упростить, то есть решить, путем унификации :

Ограничение t1=t2можно упростить, если оба термина являются функциональными символами, применяемыми к другим терминам. Если два функциональных символа совпадают и количество подтермов также совпадает, это ограничение можно заменить попарным равенством подтермов. Если термины состоят из разных функциональных символов или одного и того же функтора, но на разном количестве членов, ограничение невыполнимо.

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

В этой форме удовлетворения ограничений значения переменных являются терминами.

Реалы

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

Если быть точным, термины - это выражения над переменными и действительными константами. Равенство между терминами - это своего рода ограничение, которое всегда присутствует, поскольку интерпретатор генерирует равенство терминов во время выполнения. Например, если первым литералом текущей цели является A(X+1)и интерпретатор выбрал предложение, которое A(Y-1):-Y=1после перезаписи является переменными, к текущей цели добавляются ограничения X+1=Y-1и . Очевидно, что правила упрощения, используемые для функциональных символов, не используются: это не является неудовлетворительным только потому, что первое выражение построено с использованием, а второе - с использованием . ${\ displaystyle Y = 1}$X+1=Y-1+-

Действительные и функциональные символы можно комбинировать, что приводит к появлению терминов, которые являются выражениями, а не вещественными числами, и функциональными символами, применяемыми к другим терминам. Формально переменные и действительные константы являются выражениями, как и любой арифметический оператор над другими выражениями. Переменные, константы (символы функции нулевой арности) и выражения являются терминами, как и любой функциональный символ, применяемый к терминам. Другими словами, термины построены на выражениях, а выражения построены на числах и переменных. В этом случае переменные варьируются от вещественных чисел и терминов . Другими словами, одна переменная может принимать в качестве значения действительное число, а другая - термин.

Равенство двух членов можно упростить, используя правила для терминов дерева, если ни один из двух членов не является действительным выражением. Например, если два термина имеют одинаковый функциональный символ и количество подтермов, их ограничение равенства может быть заменено равенством подтермов.

Конечные домены

Третий класс ограничений, используемых в программировании логики ограничений, - это ограничения конечных областей. Значения переменных в этом случае берутся из конечной области, часто целочисленной . Для каждой переменной может быть указан другой домен: X::[1..5]например, означает, что значение Xнаходится между 1и 5. Область переменной также может быть задана путем перечисления всех значений, которые может принимать переменная; следовательно, указанное выше объявление домена также может быть записано X::[1,2,3,4,5]. Этот второй способ указания домена позволяет использовать домены, не состоящие из целых чисел, например X::[george,mary,john]. Если домен переменной не указан, предполагается, что это набор целых чисел, представимых на языке. Группе переменных можно присвоить один и тот же домен с помощью объявления вида [X,Y,Z]::[1..5].

Домен переменной может быть уменьшен во время выполнения. В самом деле, поскольку интерпретатор добавляет ограничения в хранилище ограничений, он выполняет распространение ограничений, чтобы обеспечить локальную согласованность , и эти операции могут уменьшить область определения переменных. Если домен переменной становится пустым, хранилище ограничений несовместимо, и алгоритм выполняет возврат. Если домен переменной становится одноэлементным , переменной может быть присвоено уникальное значение в ее домене. Формы консистенции , как правило , являются принудительными дугами консистенции , гипер-дуговой консистенция , и оценки консистенции . Текущий домен переменной можно проверить с помощью определенных литералов; например, dom(X,D)определяет текущий домен Dпеременной X.

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

Хранилище ограничений

Хранилище ограничений содержит ограничения, которые в настоящее время считаются выполнимыми. Можно рассмотреть, что в настоящее время заменяет обычное логическое программирование. Когда разрешены только термины дерева, хранилище ограничений содержит ограничения в форме t1=t2; эти ограничения упрощаются за счет унификации, что приводит к ограничениям формы variable=term; такие ограничения эквивалентны замене.

Однако хранилище ограничений также может содержать ограничения в форме t1!=t2, если !=допускается различие между терминами. Когда разрешены ограничения над реальными или конечными доменами, хранилище ограничений может также содержать ограничения, зависящие от домена, например X+2=Y/2, и т. Д.

Хранилище ограничений расширяет концепцию текущей замены двумя способами. Во-первых, он не только содержит ограничения, полученные в результате приравнивания литерала к заголовку нового варианта предложения, но также и ограничения тела предложений. Во-вторых, он содержит не только ограничения формы, variable=valueно и ограничения на рассматриваемый язык ограничений. В то время как результатом успешной оценки обычной логической программы является окончательная подстановка, результатом для программы логики ограничений является окончательное хранилище ограничений, которое может содержать ограничение вида переменная = значение, но в целом может содержать произвольные ограничения.

Ограничения, зависящие от домена, могут поступать в хранилище ограничений как из тела предложений, так и из приравнивания литерала к заголовку предложения: например, если интерпретатор переписывает литерал A(X+2)предложением, заголовок нового варианта которого является заголовком нового варианта A(Y/2), ограничение X+2=Y/2добавляется к хранилище ограничений. Если переменная появляется в реальном или конечном выражении области, она может принимать только значение в действительной или конечной области. Такая переменная не может принимать в качестве значения терм, созданный из функтора, примененного к другим терминам. Хранилище ограничений неудовлетворительно, если переменная обязана принимать как значение конкретной области, так и функтор, применяемый к терминам.

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

В результате этих операций добавление новых ограничений может изменить старые. Важно, чтобы интерпретатор мог отменить эти изменения при возврате. Самый простой метод состоит в том, чтобы интерпретатор сохранял полное состояние хранилища каждый раз, когда он делает выбор (он выбирает предложение, чтобы переписать цель). Существуют более эффективные методы, позволяющие хранилищу ограничений вернуться в предыдущее состояние. В частности, можно просто сохранить изменения в хранилище ограничений, сделанные между двумя точками выбора, включая изменения, внесенные в старые ограничения. Это можно сделать, просто сохранив старое значение измененных ограничений; этот метод называется трейлингом . Более продвинутый метод - сохранить изменения, внесенные в измененные ограничения. Например, линейное ограничение изменяется путем изменения его коэффициента: сохранение разницы между старым и новым коэффициентом позволяет отменить изменение. Этот второй метод называется семантическим отслеживанием с возвратом , потому что сохраняется семантика изменения, а не только старая версия ограничений.

Маркировка

Литералы маркировки используются для переменных в конечных областях, чтобы проверить выполнимость или частичную выполнимость хранилища ограничений и найти удовлетворительное присвоение. Литерал маркировки имеет форму labeling([variables]), где аргумент представляет собой список переменных в конечных областях. Всякий раз, когда интерпретатор вычисляет такой литерал, он выполняет поиск по доменам переменных списка, чтобы найти присвоение, удовлетворяющее всем соответствующим ограничениям. Как правило, это делается путем поиска с возвратом : переменные оцениваются по порядку, пробуя все возможные значения для каждого из них, и выполняя поиск с возвратом при обнаружении несогласованности.

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

Второе использование литерала маркировки состоит в том, чтобы фактически определить оценку переменных, которая удовлетворяет хранилищу ограничений. Без маркировочного литерала переменным присваиваются значения только тогда, когда хранилище ограничений содержит ограничение формы X=valueи когда локальная согласованность уменьшает домен переменной до одного значения. Маркировочный литерал над некоторыми переменными заставляет эти переменные оцениваться. Другими словами, после рассмотрения литерала маркировки всем переменным присваивается значение.

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

solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)

Когда интерпретатор оценивает цель solve(args), он помещает текст нового варианта первого предложения в текущую цель. Поскольку первая цель равна constraints(X'), второе предложение оценивается, и эта операция перемещает все ограничения в текущей цели и, в конечном итоге, в хранилище ограничений. Затем литерал labeling(X')оценивается, вызывая поиск решения хранилища ограничений. Поскольку хранилище ограничений содержит в точности ограничения исходной задачи удовлетворения ограничений, эта операция ищет решение исходной проблемы.

Переформулировки программы

Программу логики данного ограничения можно переформулировать для повышения ее эффективности. Первое правило заключается в том, что маркировочные литералы следует размещать после того, как в хранилище ограничений будет накоплено столько ограничений на помеченные литералы. Хотя теоретически это эквивалентно , поиск, который выполняется, когда интерпретатор встречает литерал маркировки, находится в хранилище ограничений, которое не содержит ограничения . В результате он может генерировать решения, например , которые, как позже выясняется, не удовлетворяют этому ограничению. С другой стороны, во второй формулировке поиск выполняется только тогда, когда ограничение уже находится в хранилище ограничений. В результате поиск возвращает только согласованные с ним решения, используя тот факт, что дополнительные ограничения сокращают пространство поиска. A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

Вторая переформулировка, которая может повысить эффективность, - это поместить ограничения перед литералами в теле предложений. Опять же и в принципе равноценны. Однако для первого может потребоваться больше вычислений. Например, если хранилище ограничений содержит ограничение , интерпретатор рекурсивно выполняет оценку в первом случае; в случае успеха он обнаруживает, что хранилище ограничений несовместимо при добавлении . Во втором случае при оценке этого предложения интерпретатор сначала добавляет в хранилище ограничений, а затем, возможно, выполняет оценку . Поскольку хранилище ограничений после добавления оказывается несовместимым, рекурсивное вычисление не выполняется вообще. A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

Третья переформулировка, которая может повысить эффективность, - это добавление избыточных ограничений. Если программист знает (каким-либо образом), что решение проблемы удовлетворяет определенному ограничению, он может включить это ограничение, чтобы как можно скорее вызвать несогласованность хранилища ограничений. Например, если заранее известно, что оценка B(X)приведет к положительному значению X, программист может добавить X>0перед любым появлением B(X). Например, A(X,Y):-B(X),C(X)не удастся достичь цели A(-2,Z), но это обнаруживается только во время оценки подцели B(X). С другой стороны, если указанное выше предложение заменяется на , интерпретатор выполняет возврат, как только ограничение добавляется в хранилище ограничений, что происходит до начала оценки четности. A(X,Y):-X>0,A(X),B(X)X>0B(X)

Правила обработки ограничений

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

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

Первое правило говорит, что, если B(X)оно вызвано хранилищем, ограничение A(X)можно переписать как C(X). В качестве примера N*X>0можно переписать, как X>0будто магазин подразумевает это N>0. Этот символ <=>в логике напоминает эквивалентность и говорит о том, что первое ограничение эквивалентно второму. На практике это означает, что первое ограничение можно заменить вторым.

Второе правило вместо этого указывает, что последнее ограничение является следствием первого, если ограничение в середине вызвано хранилищем ограничений. В результате, если он A(X)находится в хранилище ограничений и B(X)вызван хранилищем ограничений, то C(X)может быть добавлен в хранилище. В отличие от случая эквивалентности, это дополнение, а не замена: добавляется новое ограничение, но остается старое.

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

Пункты логического программирования в сочетании с правилами обработки ограничений могут использоваться для определения метода для установления выполнимости хранилища ограничений. Различные предложения используются для реализации различных вариантов выбора метода; правила обработки ограничений используются для перезаписи хранилища ограничений во время выполнения. Например, таким образом можно реализовать отслеживание с возвратом с распространением единиц . Let holds(L)представляет пропозициональное предложение, в котором литералы в списке Lнаходятся в том же порядке, в котором они оцениваются. Алгоритм может быть реализован с использованием предложений для выбора присвоения литералу значения true или false и правил обработки ограничений для определения распространения. В этих правилах указано, что holds([l|L])может быть удалено, если это l=trueследует из хранилища, и может быть переписано, как holds(L)если бы это l=falseследует из хранилища. Аналогично holds([l])можно заменить на l=true. В этом примере выбор значения переменной реализован с помощью предложений логического программирования; однако его можно закодировать в правилах обработки ограничений, используя расширение, называемое правилами обработки дизъюнктивных ограничений или CHR ^∨ .

Оценка снизу вверх

Стандартная стратегия оценки логических программ - сверху вниз и сначала в глубину : от цели определяется ряд предложений, которые, возможно, могут доказать цель, и выполняется рекурсия по литералам их тел. Альтернативная стратегия - начать с фактов и использовать предложения для получения новых фактов; эта стратегия называется восходящей . Он считается лучшим, чем метод «сверху вниз», когда цель состоит в том, чтобы произвести все последствия данной программы, а не доказать единственную цель. В частности, обнаружение всех последствий программы стандартным методом «сверху вниз» и «сначала в глубину» может не завершиться, пока не завершится стратегия оценки снизу вверх .

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

A(q).
B(X):-A(X).

Набор последствий изначально пуст. На первом этапе A(q)это единственное предложение, тело которого может быть доказано (поскольку оно пусто), и A(q)поэтому оно добавляется к текущему набору последствий. На втором этапе, поскольку A(q)доказано, можно использовать второе предложение и B(q)добавить его к следствиям. Поскольку никакие другие последствия не могут быть доказаны {A(q),B(q)}, выполнение прекращается.

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

A(q).
B(X):-A(X).
A(X):-B(X).

Например, при оценке всех ответов на цель A(X)стратегия сверху вниз приведет к следующим выводам:

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

Другими словами, A(q)сначала создается единственное следствие , но затем алгоритм циклически перебирает выводы, которые не дают другого ответа. В более общем плане стратегия оценки сверху вниз может циклически перебирать возможные производные, возможно, когда существуют другие.

Стратегия «снизу вверх» не имеет того же недостатка, поскольку уже выведенные последствия не имеют никакого эффекта. В вышеупомянутой программе восходящая стратегия начинает добавлять A(q)к набору последствий; на втором этапе B(X):-A(X)используется для получения B(q); на третьем этапе единственными фактами, которые могут быть выведены из текущих последствий, являются A(q)и B(q), которые, однако, уже входят в набор последствий. В результате алгоритм останавливается.

В приведенном выше примере единственными использованными фактами были наземные литералы. В общем, каждое предложение, которое содержит только ограничения в теле, считается фактом. Например, оговорка A(X):-X>0,X<10тоже считается фактом. Для этого расширенного определения фактов некоторые факты могут быть эквивалентными, но не синтаксически равными. Например, A(q)эквивалентно, A(X):-X=qи оба они эквивалентны A(X):-X=Y, Y=q. Чтобы решить эту проблему, факты переводятся в нормальную форму, в которой заголовок содержит кортеж всех различных переменных; тогда два факта эквивалентны, если их тела эквивалентны по переменным головы, то есть их наборы решений одинаковы при ограничении этими переменными.

Как описано, восходящий подход имеет то преимущество, что не учитывает уже выведенные последствия. Тем не менее, он все еще может иметь последствия, которые влечет за собой уже полученные, хотя и не равны ни одному из них. Например, оценка следующей программы снизу вверх бесконечна:

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

Алгоритм восходящей оценки сначала выводит, что A(X)верно для X=0и X>0. На втором этапе первый факт с третьим предложением позволяет получить A(1). На третьем этапе A(2)выводится и т. Д. Однако эти факты уже вытекают из того факта, что A(X)верно для любого неотрицательного X. Этот недостаток может быть преодолен путем проверки фактов следствия , которые должны быть добавлены к текущему набору последствий. Если новое последствие уже влечет за собой множество, оно не добавляется к нему. Поскольку факты хранятся в виде предложений, возможно, с «локальными переменными», вывод ограничен по переменным их заголовков.

Программирование параллельной логики ограничений

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

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

Приложения

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

История

Программирование с логикой ограничений было введено Яффаром и Лассезом в 1987 году. Они обобщили наблюдение, что термины «уравнения» и «неравенства» в Prolog II были особой формой ограничений, и обобщили эту идею на произвольные языки ограничений. Первыми реализациями этой концепции были Prolog III , CLP (R) и CHIP .

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

• BProlog
• BNR Prolog (также известный как CLP (BNR))
• Чао
• CLP (R)
• Распространенный Оз Моцарт
• Затмение
• GNU Prolog
• SWI-Prolog

использованная литература

• Дехтер, Рина (2003). Обработка ограничений . Морган Кауфманн. ISBN 1-55860-890-7. ISBN  1-55860-890-7
• Апт, Кшиштоф (2003). Принципы программирования ограничений . Издательство Кембриджского университета. ISBN 0-521-82583-0. ISBN  0-521-82583-0
• Marriott, Ким; Питер Дж. Стаки (1998). Программирование с ограничениями: введение . MIT Press. ISBN  0-262-13341-5
• Фрювирт, Том; Слим Абденнадхер (2003). Основы программирования ограничений . Springer. ISBN 3-540-67623-6. ISBN  3-540-67623-6
• Джаффар, Джоксан; Майкл Дж. Махер (1994). «Программирование с ограничениями логики: обзор» . Журнал логического программирования . 19/20: 503–581. DOI : 10.1016 / 0743-1066 (94) 90033-7 .
• Колмерауэр, Ален (1987). «Открытие вселенной Пролога III». Байт . Август.

использованная литература