Content deleted Content added
DavidGries (talk | contribs) →References: added author-link for "Krzysztof R. Apt" |
|||
| (5 intermediate revisions by 4 users not shown) | |||
Line 1:
{{Short description|Logic programming with constraint satisfaction}}
{{Programming paradigms}}▼
'''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==
Line 14 ⟶ 13:
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. (
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
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 <code>A(X,1)</code> proceeds by evaluating the body of the first clause with <code>Y=1</code>; this evaluation adds <code>X>0</code> to the constraint store and requires the goal <code>B(X,1)</code> to be proven. While trying to prove this goal, the first clause is applied but its evaluation adds <code>X<0</code> 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 <code>X=1</code> and <code>Y>0</code> to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution <code>X=1, Y=1</code>.
Line 26 ⟶ 25:
Initially, the current goal is the goal and the constraint store is empty. The interpreter proceeds by removing the first element from the current goal and analyzing it. The details of this analysis are explained below, but in the end this analysis may produce a successful termination or a failure. This analysis may involve [[Recursion|recursive call]]s and addition of new literals to the current goal and new constraint to the constraint store. The interpreter backtracks if a failure is generated. A successful termination is generated when the current goal is empty and the constraint store is satisfiable.
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.
Line 34 ⟶ 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 {{mvar|G}} is a constraint {{mvar|C}}, and we have <math>G'=G \backslash \{C\}</math> and <math>S'=S \cup \{C\}</math>; in other words, a constraint can be moved from the goal to the constraint store
* an element of {{mvar|G}} is a literal <math>L(t_1,\ldots,t_n)</math>, there exists a clause that, rewritten using new variables, is <math>L(t_1',\ldots,t_n') \mathrel{{:}{-}} B</math>, the set <math>G'</math> is {{mvar|G}} with <math>L(t_1,\ldots,t_n)</math> replaced by <math>t_1=t_1',\ldots,t_n=t_n',B</math>, and <math>S'=S</math>; in other words, a literal can be replaced by the body of a fresh variant of a clause having the same predicate in the head, adding the body of the fresh variant and the above equalities of
* {{mvar|S}} and <math>S'</math> are equivalent according to the specific constraint semantics
Actual interpreters process the goal elements in a [[LIFO (computing)|LIFO]] order: elements are added in the front and processed from the front. They also choose the clause of the second rule according to the order in which they are written, and rewrite the constraint store when it is modified.
Line 46 ⟶ 45:
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
==Terms and conditions==
Line 86 ⟶ 85:
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. First, it
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 <code>A(X+2)</code> with a clause whose fresh variant head is <code>A(Y/2)</code>, the constraint <code>X+2=Y/2</code> 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.
Line 139 ⟶ 138:
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:
Line 180 ⟶ 179:
==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
==See also==
*[[
*[[BNR Prolog]] (aka CLP(BNR))
*[[Constraint Handling Rules]]
Line 202 ⟶ 201:
| first=Rina
| last=Dechter
|authorlink = Rina Dechter
| title=Constraint processing
| publisher=Morgan Kaufmann
Line 242:
|author2=Michael J. Maher
| title=Constraint logic programming: a survey
| journal=[[Journal of Logic Programming]]
| volume=19/20
| pages=503–581
Line 260:
==References==
{{reflist}}
▲{{Programming paradigms navbox}}
{{DEFAULTSORT:Constraint Logic Programming}}
| |||