Content deleted Content added
→Semantics: clarified that is overview + detail of each step |
|||
| (132 intermediate revisions by 85 users not shown) | |||
Line 1:
{{Short description|Logic programming with constraint satisfaction}}
'''Constraint logic programming''' is a form of [[constraint programming]], in which [[logic programming]] is extended to include concepts from [[constraint satisfaction]]. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is {{code|2=prolog|A(X,Y) :- X+Y>0, B(X), C(Y)}}. In this clause, {{code|2=prolog|X+Y>0}} is a constraint; <code>A(X,Y)</code>, <code>B(X)</code>, and <code>C(Y)</code> are [[Literal (mathematical logic)|literals]] as in regular logic programming. This clause states one condition under which the statement <code>A(X,Y)</code> holds: <code>X+Y</code> is greater than zero and both <code>B(X)</code> and <code>C(Y)</code> are true.
As in regular logic programming, programs are queried about the provability of a goal, which itself may contain constraints in addition to literals. A proof for a goal is composed of clauses whose bodies are satisfiable constraints and literals that can in turn be proved using other clauses. Execution is performed by an interpreter, which starts from the goal and [[Recursion|recursively]] scans the clauses trying to prove the goal. Constraints encountered during this scan are placed in a set called the '''constraint store'''. If this set is found out to be unsatisfiable, the interpreter [[Backtracking|backtracks]], trying to use other clauses for proving the goal. In practice, satisfiability of the constraint store may be checked using an incomplete algorithm, which does not always detect inconsistency.
==Overview==
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, <code>X>0</code> is a constraint, and is included in the last clause of the following constraint logic program.
<syntaxhighlight lang="prolog">
B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).
</syntaxhighlight>
Like in regular logic programming, evaluating a goal such as <code>A(X,1)</code> requires evaluating the body of the last clause with <code>Y=1</code>. Like in regular logic programming, this in turn requires proving the goal <code>B(X,1)</code>. Contrary to regular logic programming, this also requires a constraint to be satisfied: <code>X>0</code>, 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 <code>X</code> is not determined when the last clause is evaluated. As a result, the constraint <code>X>0</code> is neither satisfied nor violated at this point. Rather than proceeding in the evaluation of <code>B(X,1)</code> and then checking whether the resulting value of <code>X</code> is positive afterwards, the interpreter stores the constraint <code>X>0</code> and then proceeds in the evaluation of <code>B(X,1)</code>; this way, the interpreter can detect violation of the constraint <code>X>0</code> during the evaluation of <code>B(X,1)</code>, and backtrack immediately if this is the case, rather than waiting for the evaluation of <code>B(X,1)</code> to conclude.
==Semantics==
The semantics of constraint logic programs can be defined in terms of a virtual interpreter that maintains a pair <math>\langle G,S \rangle</math> during execution. The first element of this pair is called current goal; the second element is called constraint store. The ''current goal'' contains the literals the interpreter is trying to prove
Initially, the current goal is the goal and the constraint store is empty. The interpreter
The details of the analysis of a literal removed from the goal is as follows. After having removed this literal from the front of the goal, it is checked whether it is a constraint or a literal. If it is a constraint, it is added to the constraint store. If it is a literal, a clause whose head has the same predicate
Some checks are done during these operations. In particular, the constraint store is checked for consistency every time a new constraint is added to it. In principle, whenever the constraint store is unsatisfiable the algorithm could backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, an incomplete satisfiability checker may be used instead. In practice, satisfiability is checked using methods that simplify the constraint store, that is, rewrite it into an equivalent but simpler-to-solve form. These methods can sometimes but not always prove unsatisfiability of an unsatisfiable constraint store.
The interpreter has proved the goal when the current goal is empty and the constraint store is not detected unsatisfiable. The result of execution is the current set of (simplified) constraints. This set may include constraints such as <math>X=2</math> that force variables to a specific value, but may also include constraints like <math>X>2</math> that only bound variables without giving them a specific value.
Line 36 ⟶ 33:
Formally, the semantics of constraint logic programming is defined in terms of ''derivations''. A transition is a pair of pairs goal/store, noted <math>\langle G,S \rangle \rightarrow \langle G',S' \rangle</math>. Such a pair states the possibility of going from state <math>\langle G,S \rangle</math> to state <math>\langle G',S' \rangle</math>. Such a transition is possible in three possible cases:
* an element of
* an element of
*
Actual
The third possible kind of transition is a
The result of evaluating a goal against a constraint logic program is defined if the goal is proved. In this case, there exists a derivation from the initial pair to a pair where the goal is empty. The constraint store of this second pair is considered the result of the evaluation. This is because the constraint store contains all constraints assumed satisfiable to prove the goal. In other words, the goal is proved for all variable evaluations that satisfy these constraints.
The pairwise equality of the arguments of two literals is often compactly denoted by <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math>: this is a shorthand for the constraints <math>t_1=t_1',\ldots,t_n=t_n'</math>. A common variant of the semantics for constraint logic programming adds <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> directly to the constraint store rather than to the goal.
==Terms and conditions==
Different definitions of terms are used, generating different kinds of constraint logic programming: over trees, reals, or finite domains. A kind of constraint that is always present is the equality of terms. Such constraints are necessary because the interpreter adds <code>t1=t2</code> to the goal whenever a literal <code>P(...t1...)</code> is replaced with the body of a clause
===Tree terms===
Constraint logic programming with tree terms emulates regular logic programming by storing substitutions as constraints in the constraint store. Terms are variables, constants, and
A constraint <code>t1=t2</code> can be simplified if both terms are
If one of the two terms is a variable, the only allowed value the variable can take is the other term. As a result, the other term can replace the variable in the current goal and constraint store, thus practically removing the variable from consideration. In the particular case of equality of a variable with itself, the constraint can be removed as always satisfied.
Line 66 ⟶ 63:
===Reals===
Constraint logic programming with [[real number]]s uses real expressions as terms. When no
Reals and
Equality of two terms can be simplified using the rules for tree terms if none of the two terms is a real expression. For example, if the two terms have the same
===Finite domains===
{{see also|Constraint satisfaction problem}}
The third class of constraints used in constraint logic programming is that of finite domains. Values of variables are in this case taken from a finite ___domain, often that of [[integer number]]s. For each variable, a different ___domain can be specified: <code>X::[1..5]</code> for example means that the value of <code>X</code> is between <code>1</code> and <code>5</code>. The ___domain of a variable can also be given by enumerating all values a variable can take; therefore, the above ___domain declaration can be also written <code>X::[1,2,3,4,5]</code>. This second way of specifying a ___domain allows for domains that are not composed of integers, such as <code>X::[george,mary,john]</code>. If the ___domain of a variable is not specified, it is assumed to be the set of integers representable in the language. A group of variables can be given the same ___domain using a declaration like <code>[X,Y,Z]::[1..5]</code>.
The ___domain of a variable may be reduced during execution. Indeed, as the interpreter adds constraints to the constraint store, it performs [[constraint propagation]] to enforce a form of [[local consistency]], and these operations may reduce the ___domain of variables. If the ___domain of a variable becomes empty, the constraint store is inconsistent, and the
As for domains of reals, functors can be used with domains of integers. In this case, a term can be an expression over integers, a constant, or the application of a functor over other terms. A variable can take an arbitrary term as a value, if its ___domain has not been specified to be a set of integers or constants.
Line 86 ⟶ 83:
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 <code>t1=t2</code>; these constraints are simplified by unification, resulting in constraints of the form <code>variable=term</code>; such constraints are equivalent to a substitution.
However, the constraint store may also contain constraints in the form <code>t1!=t2</code>, if the difference <code>!=</code> between terms is allowed. When constraints over reals or finite domains are allowed, the constraint store may also contain ___domain-specific constraints like <code>X+2=Y/2</code>, etc.
The constraint store extends the concept of current substitution in two ways
Domain-specific constraints may come to the constraint store both from the body of a clauses and from
After a constraint is added to the constraint store, some operations
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==
Line 100 ⟶ 98:
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 <code>labeling([variables])</code>, 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
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 <code>X=value</code> 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
{{sxhl|
|prolog}}
When the interpreter evaluates the goal <code>solve(args)</code>, it places the
==Program reformulations==
A given constraint logic
A second reformulation that can increase efficiency is to place constraints before literals in the body of clauses. Again,
A third reformulation that can increase efficiency is the addition of redundant
==Constraint handling rules==
[[Constraint handling rules]]
A(X) <
A(X)
The first rule tells that, if <code>B(X)</code> is entailed by the store, the constraint <code>A(X)</code> can be rewritten as <code>C(X)</code>. As an example, <code>N*X>0</code> can be rewritten as <code>X>0</code> if the store implies that <code>N>0</code>. The symbol <code><
The second rule instead specifies that the latter constraint is a consequence of the first, if the constraint in the middle is entailed by the constraint store. As a result, if <code>A(X)</code> is in the constraint store and <code>B(X)</code> is entailed by the constraint store, then <code>C(X)</code> can be added to the store. Differently from the case of equivalence, this is an addition and not a replacement: the new constraint is added but the old one remains.
Equivalence allows for simplifying the constraint store
Logic programming clauses in conjunction with constraint handling rules can be used to specify
example, the choice of value for a variable is implemented using clauses of logic programming; however, it can be encoded in constraint handling rules using an extension called disjunctive constraint handling rules or CHR<sup>∨</sup>.
==Bottom-up evaluation==
The standard strategy of evaluation of logic programs is [[Top-down and bottom-up design#Computer science|top-down]] and [[depth-first]]: from the goal, a number of clauses are identified as being possibly able to prove the goal, and recursion over the literals of their bodies is performed. An alternative strategy is to start from the facts and use clauses to derive new facts; this strategy is called [[Top-down and bottom-up design#Computer science|bottom-up]]. It is considered better than the top-down one when the aim is that of producing all consequences of a given program, rather than proving a single goal. In particular, finding all consequences of a program in the standard top-down and depth-first manner may not terminate while the bottom-up [[evaluation strategy]] terminates.
The bottom-up evaluation strategy maintains the set of facts proved so far during evaluation. This set is initially empty. With each step, new facts are derived by applying a program clause to the existing facts, and are added to the set. For example, the bottom up evaluation of the following program requires two steps:
{{sxhl|2=prolog|1=<nowiki/>
A(q).
B(X):-A(X).
}}
The set of consequences is initially empty. At the first step, <code>A(q)</code> is the only clause whose body can be proved (because it is empty), and <code>A(q)</code> is therefore added to the current set of consequences. At the second step, since <code>A(q)</code> is proved, the second clause can be used and <code>B(q)</code> is added to the consequences. Since no other consequence can be proved from <code>{A(q),B(q)}</code>, execution terminates.
The advantage of the bottom-up evaluation over the top-down one is that cycles of derivations do not produce an [[infinite loop]]. This is because adding a consequence to the current set of consequences that already contains it has no effect. As an example, adding a third clause to the above program generates a cycle of derivations in the top-down evaluation:
{{sxhl|2=prolog|1=<nowiki/>
A(q).
B(X):-A(X).
A(X):-B(X).
}}
For example, while evaluating all answers to the goal <code>A(X)</code>, the top-down strategy would produce the following derivations:
{{sxhl|2=prolog|1=<nowiki/>
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)
}}
In other words, the only consequence <code>A(q)</code> is produced first, but then the algorithm cycles over derivations that do not produce any other answer. More generally, the top-down evaluation strategy may cycle over possible derivations, possibly when other ones exist.
The bottom-up strategy does not have the same drawback, as consequences that were already derived has no effect. On the above program, the bottom-up strategy starts adding <code>A(q)</code> to the set of consequences; in the second step, <code>B(X):-A(X)</code> is used to derive <code>B(q)</code>; in the third step, the only facts that can be derived from the current consequences are <code>A(q)</code> and <code>B(q)</code>, which are however already in the set of consequences. As a result, the algorithm stops.
In the above example, the only used facts were ground literals. In general, every clause that only contains constraints in the body is considered a fact. For example, a clause
As described, the bottom-up approach has the advantage of not considering consequences that have already been derived. However, it still may derive consequences that are entailed by those already derived while not being equal to any of them. As an example, the bottom up evaluation of the following program is infinite:
<syntaxhighlight lang="prolog">
A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).
</syntaxhighlight>
The bottom-up evaluation algorithm first derives that <code>A(X)</code> is true for <code>X=0</code> and <code>X>0</code>. In the second step, the first fact with the third clause allows for the derivation of <code>A(1)</code>. In the third step, <code>A(2)</code> is derived, etc. However, these facts are already entailed by the fact that <code>A(X)</code> is true for any nonnegative <code>X</code>. This drawback can be overcome by checking for [[entailment]] facts that are to be added to the current set of consequences. If the new consequence is already entailed by the set, it is not added to it. Since facts are stored as clauses, possibly with "local variables", entailment is restricted over the variables of their heads.
==Concurrent constraint logic programming==
{{main|Concurrent constraint logic programming}}
The concurrent versions of constraint logic programming are aimed at programming [[concurrent process]]es rather than solving [[constraint satisfaction problem]]s. Goals in constraint logic programming are evaluated concurrently; a concurrent process is therefore programmed as the evaluation of a goal by the [[Interpreter (computing)|interpreter]].
Syntactically, concurrent constraints logic programs are similar to non-concurrent programs, the only exception being that clauses includes ''guards'', which are constraints that may block the applicability of the clause under some conditions. Semantically, concurrent constraint logic programming differs from its non-concurrent versions because a goal evaluation is intended to realize a concurrent process rather than finding a solution to a problem. Most notably, this difference affects how the interpreter behaves when more than one clause is applicable: non-concurrent constraint logic programming [[Recursion|recursively]] tries all clauses; concurrent constraint logic programming chooses only one. This is the most evident effect of an intended ''directionality'' of the interpreter, which never revises a choice it has previously taken. Other effects of this are the semantical possibility of having a goal that cannot be proved while the whole evaluation does not fail, and a particular way for equating a goal and a clause head.
==Applications==
Constraint logic programming has been applied to a number of fields, such as [[Automated planning and scheduling|automated scheduling]],<ref>Abdennadher, Slim, and Hans Schlenker. "[https://www.aaai.org/Papers/IAAI/1999/IAAI99-118.pdf?q=optimal-scheduling-using-constraint-logic-programming Nurse scheduling using constraint logic programming]." [[AAAI]]/IAAI. 1999.</ref> [[type inference]],<ref>Michaylov, Spiro, and [[Frank Pfenning]]. "[http://www.cs.cmu.edu/Groups/fox/people/fp/papers/ppcp93.pdf Higher-Order Logic Programming as Constraint Logic Programming]." PPCP. Vol. 93. 1993.</ref> [[civil engineering]], [[mechanical engineering]], [[digital circuit]] verification, [[air traffic control]], finance, and others.{{citation needed|date=September 2020}}
==History==
Constraint logic programming was introduced by Jaffar and Lassez in 1987.<ref>Jaffar, Joxan, and J-L. Lassez. "[https://dl.acm.org/citation.cfm?id=41635 Constraint logic programming]." Proceedings of the 14th [[ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages]]. ACM, 1987.</ref> They generalized the observation that the term equations and disequations of [[Prolog II]] were a specific form of constraints, and generalized this idea to arbitrary constraint languages. The first implementations of this concept were [[Prolog III]], [[CLP(R)]], and [[CHIP (programming language)|CHIP]].{{citation needed|date=August 2019}}
==See also==
*[[B-Prolog]]
*[[BNR Prolog]] (aka CLP(BNR))
*[[Constraint Handling Rules]]
*[[Ciao (programming language)|Ciao]]
*[[CLP(R)]]
*[[Oz (programming language)|Distributed Oz Mozart]]
*[[ECLiPSe]]
*[[GNU Prolog]]
*[[SWI-Prolog]]
==References==
Line 180 ⟶ 201:
| first=Rina
| last=Dechter
|authorlink = Rina Dechter
| title=Constraint processing
| publisher=Morgan Kaufmann
| year=2003
| url=https://archive.org/details/constraintproces00rina
| url-access=registration
}} {{ISBN|1-55860-890-7}}
*{{cite book
| first=Krzysztof
| last=Apt
| author-link=Krzysztof R. Apt
| title=Principles of constraint programming
| publisher=Cambridge University Press
| year=2003
| url-access=registration
| url=https://archive.org/details/principlesofcons0000aptk
}} {{ISBN|0-521-82583-0}}
*{{cite book
| first=Kim
| last=
|
| title=Programming with constraints: An introduction
| year=1998
| publisher=MIT Press
}} {{ISBN
*{{cite book
| first=Thom
| last=
|
| title=Essentials of constraint programming
| year=2003
| publisher=Springer
}} {{ISBN|3-540-67623-6}}
*{{cite journal
| first=Joxan
| last=Jaffar
|author2=Michael J. Maher
| title=Constraint logic programming: a survey
| journal=[[Journal of Logic Programming]]
| volume=19/20
| pages=503–581
| year=1994
| doi=10.1016/0743-1066(94)90033-7
| doi-access=free
}}
*{{cite journal
| first=Alain
| last = Colmerauer
| title=Opening the Prolog III Universe
| journal=Byte
| volume= August
| year=1987
}}
==
{{reflist}}
{{Programming paradigms navbox}}
{{DEFAULTSORT:Constraint Logic Programming}}
[[Category:Constraint logic programming| ]]
[[Category:Logic programming]]
[[Category:Constraint
| |||