Content deleted Content added
m <source lang="prolog"> |
|||
| (33 intermediate revisions by 23 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==
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>
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
==Semantics==
Line 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 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 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 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. 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 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 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 <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 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:
{{sxhl|
|prolog}}
When the interpreter evaluates the goal <code>solve(args)</code>, it places the body of a fresh variant of the first clause in the current goal. Since the first goal is <code>constraints(X')</code>, the second clause is evaluated, and this operation moves all constraints in the current goal and eventually in the constraint store. The literal <code>labeling(X')</code> is then evaluated, forcing a search for a solution of the constraint store. Since the constraint store contains exactly the constraints of the original constraint satisfaction problem, this operation searches for a solution of the original problem.
Line 115:
A second reformulation that can increase efficiency is to place constraints before literals in the body of clauses. Again, {{code|2=prolog|A(X):-B(X),X>0}} and {{code|2=prolog|A(X):-X>0,B(X)}} are in principle equivalent. However, the first may require more computation. For example, if the constraint store contains the constraint <code>X<-2</code>, the interpreter recursively evaluates <code>B(X)</code> in the first case; if it succeeds, it then finds out that the constraint store is inconsistent when adding <code>X>0</code>. In the second case, when evaluating that clause, the interpreter first adds <code>X>0</code> to the constraint store and then possibly evaluates <code>B(X)</code>. Since the constraint store after the addition of <code>X>0</code> turns out to be inconsistent, the recursive evaluation of <code>B(X)</code> is not performed at all.
A third reformulation that can increase efficiency is the addition of redundant
==Constraint handling rules==
Line 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:
<
</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.
Line 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 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==
*[[
*[[BNR Prolog]] (aka CLP(BNR))
*[[Constraint Handling Rules]]
*[[Ciao (programming language)|Ciao]]
*[[CLP(R)]]
*[[Oz (programming language)|Distributed Oz Mozart]]
*[[ECLiPSe]]
Line 198 ⟶ 201:
| first=Rina
| last=Dechter
|authorlink = Rina Dechter
| title=Constraint processing
| publisher=Morgan Kaufmann
| year=2003
| url=https://archive.org/details/constraintproces00rina
| isbn=1-55860-890-7
| url-access=registration
}} {{ISBN
*{{cite book
| first=Krzysztof
| last=Apt
| author-link=Krzysztof R. Apt
| title=Principles of constraint programming
| publisher=Cambridge University Press
| year=2003
| isbn=0-521-82583-0
| url-access=registration
}} ISBN 0-521-82583-0▼
| url=https://archive.org/details/principlesofcons0000aptk
*{{cite book
| first=Kim
Line 219 ⟶ 227:
| year=1998
| publisher=MIT Press
}} {{ISBN
*{{cite book
| first=Thom
Line 228 ⟶ 236:
| publisher=Springer
| isbn=3-540-67623-6
}} {{ISBN
*{{cite journal
| first=Joxan
Line 234 ⟶ 242:
|author2=Michael J. Maher
| title=Constraint logic programming: a survey
| journal=[[Journal of
| volume=19/20
| pages=503–581
| year=1994
| doi=10.1016/0743-1066(94)90033-7
| doi-access=free
}}
*{{cite journal
Line 249 ⟶ 258:
}}
==References==
{{reflist}}
▲{{Programming paradigms navbox}}
{{DEFAULTSORT:Constraint Logic Programming}}
[[Category:Constraint logic programming| ]]▼
[[Category:Logic programming]]
[[Category:Constraint programming]]
▲[[Category:Constraint logic programming]]
| |||