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

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

Семантика

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

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

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

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

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

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

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

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

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

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

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

Попарное равенство аргументов двух литералов часто компактно обозначается через $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ : это сокращение для ограничений $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'$ . Распространенный вариант семантики программирования логики ограничений добавляет $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 и $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 но и ограничения на рассматриваемый язык ограничений. В то время как результатом успешной оценки обычной логической программы является окончательная замена, результатом программы логики ограничений является последнее хранилище ограничений, которое может содержать ограничения вида 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>0 эквивалентно A(X):-X>0,labeling(X), поиск, который выполняется, когда интерпретатор встречает литерал маркировки, находится в хранилище ограничений, которое не содержит ограничения X>0. В результате он может генерировать решения, такие как X=-1, которые, как позже выяснилось, не удовлетворяют этому ограничению. С другой стороны, во второй формулировке поиск выполняется только тогда, когда ограничение уже находится в хранилище ограничений. В результате поиск возвращает только соответствующие ему решения, используя тот факт, что дополнительные ограничения уменьшают пространство поиска.

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

Предложения логического программирования в сочетании с правилами обработки ограничений могут использоваться для указания метода установления выполнимости хранилища ограничений. Различные предложения используются для реализации различных вариантов метода; правила обработки ограничений используются для перезаписи хранилища ограничений во время выполнения. Например, таким образом можно реализовать обратный поиск с распространением единиц . Позволять 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. Этот недостаток можно преодолеть путем проверки фактов следствия , которые необходимо добавить к текущему набору последствий. Если новое последствие уже содержится в наборе, оно не добавляется к нему. Поскольку факты хранятся в виде предложений, возможно, с «локальными переменными», следование ограничивается переменными их заголовков.

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

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

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

Приложения

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

История

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

См. также

Ссылки

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

Ссылки

^ Абденнадер, Слим и Ханс Шленкер. « Планирование работы медсестры с использованием программирования логики ограничений ». АААИ /ИААИ. 1999.
^ Михайлов, Спиро и Фрэнк Пфеннинг . « Логическое программирование высшего порядка как программирование логики с ограничениями ». ППКП. Том. 93. 1993.
^ Джаффар, Джоксан и Дж.Л. Лассез. « Программирование логики ограничений ». Материалы 14-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . АКМ, 1987.

[1] Абденнадер, Слим и Ханс Шленкер. « Планирование работы медсестры с использованием программирования логики ограничений ». АААИ /ИААИ. 1999.

[2] Михайлов, Спиро и Фрэнк Пфеннинг . « Логическое программирование высшего порядка как программирование логики с ограничениями ». ППКП. Том. 93. 1993.

[3] Джаффар, Джоксан и Дж.Л. Лассез. « Программирование логики ограничений ». Материалы 14-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . АКМ, 1987.

[1]

[2]

[3]