Логическое программирование с ограничениями и задачами об удовлетворимости

Введение

Логическое программирование с удовлетворением ограничений

Программирование с ограничениями — это форма программирования с удовлетворением ограничений, в которой логическое программирование расширяется за счет включения концепций из области удовлетворения ограничений. Логическая программа с ограничениями — это логическая программа, содержащая ограничения в теле клауз. Примером клаузы, включающей ограничение, является: В этой клаузе является ограничением, а 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.

Formally, constraint logic programs are like regular logic programs, but the body of clauses can contain constraints, in addition to the regular logic programming literals. As an example, X>0 is a constraint, and is included in the last clause of the following constraint logic program. B(X,1): X<0. B(X,Y): X=1, Y>0. A(X,Y): X>0, B(X,Y). Like in regular logic programming, evaluating a goal such as A(X,1) requires evaluating the body of the last clause with Y=1. Like in regular logic programming, this in turn requires proving the goal B(X,1). Contrary to regular logic programming, this also requires a constraint to be satisfied: X>0, the constraint in the body of the last clause. (In regular logic programming, X>0 cannot be proved unless X is bound to a fully ground term and execution of the program will fail if that is not the case.) Whether a constraint is satisfied cannot always be determined when the constraint is encountered. In this case, for example, the value of X is not determined when the last clause is evaluated. As a result, the constraint X>0 is neither satisfied nor violated at this point. Rather than proceeding in the evaluation of B(X,1) and then checking whether the resulting value of X is positive afterwards, the interpreter stores the constraint X>0 and then proceeds in the evaluation of B(X,1); this way, the interpreter can detect violation of the constraint X>0 during the evaluation of B(X,1), and backtrack immediately if this is the case, rather than waiting for the evaluation of B(X,1) to conclude. In general, the evaluation of a constraint logic program proceeds as does a regular logic program. However, constraints encountered during evaluation are placed in a set called a constraint store. As an example, the evaluation of the goal A(X,1) proceeds by evaluating the body of the first clause with Y=1; this evaluation adds X>0 to the constraint store and requires the goal B(X,1) to be proven. While trying to prove this goal, the first clause is applied but its evaluation adds X<0 to the constraint store. This addition makes the constraint store unsatisfiable. The interpreter then backtracks, removing the last addition from the constraint store. The evaluation of the second clause adds X=1 and Y>0 to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution X=1, Y=1.

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

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

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

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

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

Реал

Логическое программирование с использованием действительных чисел использует действительные выражения в качестве термов. Когда символы функций не используются, термы являются выражениями над действительными числами, возможно, включая переменные. В этом случае каждая переменная может принимать только действительное число в качестве значения. Точнее говоря, термы – это выражения над переменными и действительными константами. Равенство между термами – это вид ограничения, которое всегда присутствует, поскольку интерпретатор генерирует равенства термов во время выполнения. Например, если первый литерал текущей цели – A(X+1), а интерпретатор выбрал пункт A(Y 1): Y=1 после переписывания переменных, то ограничения, добавленные к текущей цели, будут X+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; эти ограничения упрощаются унификацией, в результате чего получаются ограничения вида переменная=терм; такие ограничения эквивалентны подстановке. Однако хранилище ограничений может также содержать ограничения вида t1!=t2, если допускается неравенство != между термами. Когда разрешены ограничения над вещественными числами или конечными областями, хранилище ограничений может также содержать специфичные для области ограничения, такие как X+2=Y/2 и т.п. Хранилище ограничений расширяет понятие текущей подстановки двумя способами. Во-первых, оно содержит не только ограничения, полученные из отождествления литерала с головой свежей вариации клоза, но и ограничения тела клозов. Во-вторых, оно содержит не только ограничения вида переменная=значение, но и ограничения, относящиеся к рассматриваемому языку ограничений. В то время как результатом успешного вычисления обычной логической программы является окончательная подстановка, результатом для логической программы с ограничениями является окончательное хранилище ограничений, которое может содержать ограничения вида переменная=значение, но в общем случае может содержать произвольные ограничения. Специфичные для области ограничения могут поступать в хранилище ограничений как из тела клозов, так и из отождествления литерала с головой клоза: например, если интерпретатор переписывает литерал A(X+2) с клозом, голова свежей вариации которого A(Y/2), то ограничение X+2=Y/2 добавляется в хранилище ограничений. Если переменная встречается в выражении над вещественными числами или конечной областью, она может принимать только значение из области вещественных чисел или конечной области. Такая переменная не может принимать в качестве значения терм, составленный из функтора, примененного к другим термам. Хранилище ограничений становится невыполнимым, если переменная обязана принимать как значение из конкретной области, так и функтор, примененный к термам. После добавления ограничения в хранилище ограничений над ним выполняются некоторые операции. Какие именно операции выполняются, зависит от рассматриваемой области и ограничений. Например, унификация используется для конечных равенств термов-деревьев, исключение переменных – для полиномиальных уравнений над вещественными числами, распространение ограничений – для обеспечения формы локальной согласованности для конечных областей. Эти операции направлены на упрощение хранилища ограничений для проверки на выполнимость и решения. В результате этих операций добавление новых ограничений может изменить старые. Важно, чтобы интерпретатор мог отменять эти изменения при возврате. Самый простой способ – сохранять полное состояние хранилища каждый раз, когда делается выбор (выбирается клоз для переписывания цели). Существуют более эффективные методы, позволяющие хранилищу ограничений возвращаться в предыдущее состояние. В частности, можно сохранять только изменения, внесенные в хранилище ограничений между двумя точками выбора, включая изменения, внесенные в старые ограничения. Это можно сделать, просто сохраняя старое значение измененных ограничений; этот метод называется трассировкой (trailing). Более продвинутый метод – сохранять изменения, внесенные в измененные ограничения. Например, линейное ограничение изменяется путем изменения его коэффициента: сохранение разницы между старым и новым коэффициентом позволяет отменить изменение. Этот второй метод называется семантической трассировкой (semantic backtracking), поскольку сохраняется семантика изменения, а не только старая версия ограничений.

The constraint store contains the constraints that are currently assumed satisfiable. It can be considered what the current substitution is for regular logic programming. When only tree terms are allowed, the constraint store contains constraints in the form t1=t2; these constraints are simplified by unification, resulting in constraints of the form variable=term; such constraints are equivalent to a substitution. However, the constraint store may also contain constraints in the form t1!=t2, if the difference != between terms is allowed. When constraints over reals or finite domains are allowed, the constraint store may also contain domain specific constraints like X+2=Y/2, etc. The constraint store extends the concept of current substitution in two ways. First, it does not only contain the constraints derived from equating a literal with the head of a fresh variant of a clause, but also the constraints of the body of clauses. Second, it does not only contain constraints of the form variable=value but also constraints on the considered constraint language. While the result of a successful evaluation of a regular logic program is the final substitution, the result for a constraint logic program is the final constraint store, which may contain constraint of the form variable=value but in general may contain arbitrary constraints. Domain specific constraints may come to the constraint store both from the body of a clauses and from equating a literal with a clause head: for example, if the interpreter rewrites the literal A(X+2) with a clause whose fresh variant head is A(Y/2), the constraint X+2=Y/2 is added to the constraint store. If a variable appears in a real or finite domain expression, it can only take a value in the reals or the finite domain. Such a variable cannot take a term made of a functor applied to other terms as a value. The constraint store is unsatisfiable if a variable is bound to take both a value of the specific domain and a functor applied to terms. After a constraint is added to the constraint store, some operations are performed on the constraint store. Which operations are performed depends on the considered domain and constraints. For example, unification is used for finite tree equalities, variable elimination for polynomial equations over reals, constraint propagation to enforce a form of local consistency for finite domains. These operations are aimed at making the constraint store simpler to be checked for satisfiability and solved. As a result of these operations, the addition of new constraints may change the old ones. It is essential that the interpreter is able to undo these changes when it backtracks. The simplest case method is for the interpreter to save the complete state of the store every time it makes a choice (it chooses a clause to rewrite a goal). More efficient methods for allowing the constraint store to return to a previous state exist. In particular, one may just save the changes to the constraint store made between two points of choice, including the changes made to the old constraints. This can be done by simply saving the old value of the constraints that have been modified; this method is called trailing. A more advanced method is to save the changes that have been done on the modified constraints. For example, a linear constraint is changed by modifying its coefficient: saving the difference between the old and new coefficient allows reverting a change. This second method is called semantic backtracking,
because the semantics of the change is saved rather than the old version of the constraints only.

Маркировка

Литералы маркировки используются для переменных с конечными доменами для проверки выполнимости или частичной выполнимости хранилища ограничений и для поиска выполнимого назначения. Литерал маркировки имеет вид `labeling([переменные])`, где аргументом является список переменных с конечными доменами. Каждый раз, когда интерпретатор вычисляет такой литерал, он выполняет поиск по доменам переменных из списка, чтобы найти назначение, удовлетворяющее всем релевантным ограничениям. Обычно это делается с помощью обратного отслеживания: переменные вычисляются последовательно, перебирая все возможные значения для каждой из них и осуществляя откат при обнаружении противоречия. Первое применение литерала маркировки – это фактическая проверка выполнимости или частичной выполнимости хранилища ограничений. Когда интерпретатор добавляет ограничение в хранилище ограничений, он обеспечивает только форму локальной согласованности. Эта операция может не обнаружить противоречие, даже если хранилище ограничений невыполнимо. Литерал маркировки над набором переменных обеспечивает проверку выполнимости ограничений для этих переменных. Следовательно, использование всех переменных, упомянутых в хранилище ограничений, приводит к проверке выполнимости всего хранилища. Второе применение литерала маркировки – это фактическое определение значения переменных, удовлетворяющего хранилищу ограничений. Без литерала маркировки переменным присваиваются значения только тогда, когда хранилище ограничений содержит ограничение вида `X=значение` и когда локальная согласованность сужает домен переменной до единственного значения. Литерал маркировки над некоторыми переменными заставляет эти переменные быть вычисленными. Иными словами, после рассмотрения литерала маркировки всем переменным присваивается значение. Обычно программы логики ограничений пишутся таким образом, что литералы маркировки вычисляются только после накопления в хранилище ограничений максимально возможного количества ограничений. Это связано с тем, что литералы маркировки обеспечивают поиск, а поиск эффективнее, если существует больше ограничений, которые необходимо удовлетворить. Задача об удовлетворимости ограничений обычно решается программой логики ограничений со следующей структурой:

The labeling literals are used on variables over finite domains to check satisfiability or partial satisfiability of the constraint store and to find a satisfying assignment. A labeling literal is of the form labeling([variables]), where the argument is a list of variables over finite domains. Whenever the interpreter evaluates such a literal, it performs a search over the domains of the variables of the list to find an assignment that satisfies all relevant constraints. Typically, this is done by a form of backtracking: variables are evaluated in order, trying all possible values for each of them, and backtracking when inconsistency is detected. The first use of the labeling literal is to actual check satisfiability or partial satisfiability of the constraint store. When the interpreter adds a constraint to the constraint store, it only enforces a form of local consistency on it. This operation may not detect inconsistency even if the constraint store is unsatisfiable. A labeling literal over a set of variables enforces a satisfiability check of the constraints over these variables. As a result, using all variables mentioned in the constraint store results in checking satisfiability of the store. The second use of the labeling literal is to actually determine an evaluation of the variables that satisfies the constraint store. Without the labeling literal, variables are assigned values only when the constraint store contains a constraint of the form X=value and when local consistency reduces the domain of a variable to a single value. A labeling literal over some variables forces these variables to be evaluated. In other words, after the labeling literal has been considered, all variables are assigned a value. Typically, constraint logic programs are written in such a way labeling literals are evaluated only after as many constraints as possible have been accumulated in the constraint store. This is because labeling literals enforce search, and search is more efficient if there are more constraints to be satisfied. A constraint satisfaction problem is typical solved by a constraint logic program having the following structure:

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

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

Данная программа с логикой ограничений может быть переформулирована для повышения ее эффективности. Первое правило заключается в том, что литералы с разметкой (labeling literals) следует размещать после того, как в хранилище ограничений накопится как можно больше ограничений на эти литералы. Хотя в теории эквивалентно , поиск, выполняемый интерпретатором при встрече с литералом разметки, осуществляется в хранилище ограничений, которое не содержит ограничения X>0. В результате он может генерировать решения, такие как X=1, которые впоследствии оказываются не удовлетворяющими этому ограничению. С другой стороны, во второй формулировке поиск выполняется только тогда, когда ограничение уже присутствует в хранилище ограничений. В результате поиск возвращает только решения, согласованные с ним, используя тот факт, что дополнительные ограничения уменьшают пространство поиска. Вторая переформулировка, способная повысить эффективность, заключается в размещении ограничений перед литералами в теле правила. Опять же, и в принципе эквивалентны. Однако первый вариант может потребовать больше вычислений. Например, если хранилище ограничений содержит ограничение 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). С другой стороны, если вышеуказанное правило заменить на , интерпретатор выполнит откат (backtrack) сразу после добавления ограничения X>0 в хранилище ограничений, что происходит до начала вычисления B(X).

A given constraint logic program may be reformulated to improve its efficiency. A first rule is that labeling literals should be placed after as much constraints on the labeled literals are accumulated in the constraint store. While in theory is equivalent to , the search that is performed when the interpreter encounters the labeling literal is on a constraint store that does not contain the constraint X>0. As a result, it may generate solutions, such as X= 1, that are later found out not to satisfy this constraint. On the other hand, in the second formulation the search is performed only when the constraint is already in the constraint store. As a result, search only returns solutions that are consistent with it, taking advantage of the fact that additional constraints reduce the search space. A second reformulation that can increase efficiency is to place constraints before literals in the body of clauses. Again, and are in principle equivalent. However, the first may require more computation. For example, if the constraint store contains the constraint X< 2, the interpreter recursively evaluates B(X) in the first case; if it succeeds, it then finds out that the constraint store is inconsistent when adding X>0. In the second case, when evaluating that clause, the interpreter first adds X>0 to the constraint store and then possibly evaluates B(X). Since the constraint store after the addition of X>0 turns out to be inconsistent, the recursive evaluation of B(X) is not performed at all. A third reformulation that can increase efficiency is the addition of redundant constraints. If the programmer knows (by whatever means) that the solution of a problem satisfies a specific constraint, they can include that constraint to cause inconsistency of the constraint store as soon as possible. For example, if it is known beforehand that the evaluation of B(X) will result in a positive value for X, the programmer may add X>0 before any occurrence of B(X). As an example, A(X,Y): B(X),C(X) will fail on the goal A( 2,Z), but this is only found out during the evaluation of the subgoal B(X). On the other hand, if the above clause is replaced by , the interpreter backtracks as soon as the constraint X>0 is added to the constraint store, which happens before the evaluation of B(X) even starts.

Программирование логики с одновременными ограничениями

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

Приложения

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

История

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