Content deleted Content added
→Bottom-up evaluation: extended definition of facts |
re-added bottom up evaluation |
||
Line 1:
'''Constraint logic programming''' is a variant of [[logic programming]] including 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>A(X,Y) :- X+Y>0, B(X), C(Y)</code>. In this clause, <code>X+Y>0</code> is a constraint; <code>A(X,Y)</code>, <code>B(X)</code>, and <code>C(Y)</code> are literals like in regular logic programming. Intuitively, this clause tells one condition under which the statement <code>A(X,Y)</code> holds: this is the case if <code>X+Y</code> is greater than zero and both <code>B(X)</code> and <code>C(Y)</code> are true.
Like in regular logic programming, programs are queried about the provability of a goal. A proof for a goal is composed of clauses whose constraints are satisfied and whose literals can in turn be proved using other clauses. Execution is done 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 '''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 clause can contain constraints, in addition to the regular logic programming literals.
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; constraints and equality of terms are considered literals, so they can occur in the goal; the ''constraint store'' contains all constraints the interpreter has assumed satisfiable so far.
Initially, the current goal is the goal and the constraint store is empty. The interpreter proceed by removing the first element from the current goal and analyzing it. This analysis may end up in a [[Recursion|recursive call]] or a failure; the interpreter backtracks in the second case. It may also generate an addition of new literals to the current goal and an addition of new constraint to the constraint store. The interpreter stops when the current goal is empty and the constraint store is satisfiable.
Each step of the algorithm is as follows. The first literal of the goal is considered and removed from the current goal. 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 of the literal is chosen; the clause is rewritten by replacing its variables with new variables (what is important is that these new variables do not already occur in the goal); the body of the clause is then placed in front of the goal; the equality of each argument of the literal with the corresponding one of the rewritten clause head is placed in front of the goal as well.
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.
The interpreter stops when the current goal is empty and the constraint store is not detected unsatisfiable.
The constraints of constraints logic programming are typically of three classes: constraints over terms, constraints over reals, and constraints over finite domains, which are usually interpreted as sets of integers.
==Terms and constraints==
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 whose rewritten head is <code>P(...t2...)</code>.
===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 functors applied to other terms. The only considered constraints are equalities and disequalities between terms. Equality is particularly important, as constraints link <code>t1=t2</code> are often generated by the intepreter.
A constraint <code>t1=t2</code> can be simplified if both terms are functors applied to other terms. If the two functors are the same and the number of subterms is also the same, this constraint can be replaced with the pairwise equality of subterms. If the terms are composed of different functors or the same functor but on different number of terms, the constraint is unsatisfiable.
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.
In this form of constraint satisfaction, variable values are terms.
===Reals===
Constraint logic programming with [[real number]]s uses real expressions as terms. When no functors are used, terms are expressions over reals, possibly including variables. In this case, each variable can only take a real number as a value.
Precisely, terms are expressions over variables and real constants. Equality between terms is a kind of constraint that is always present, as the interpreter generates equality of terms during execution. As an example, if the first literal of the current goal is <code>A(X+1)</math> and the interpreter has chosen a clause that is <code>A(Y-1):-Y=1</code> after rewriting is variables, the constraints added to the current goal are <code>X+1=Y-1</code> and <math>Y=1</math>. The rules of simplification used for functors are obviously not used: <code>X+1=Y-1</code> is not unsatisfiable just because the first expression is built using <code>+</code> and the second using <code>-</code>.
Reals and functors can be combined, leading to terms that are expressions over reals and functors applied to other terms. Formally, variables and real constants are expressions, as any arithmetic operator over other expressions. Variables, constants (zero-arity-functors), and expressions are terms, as any functor applied to terms. In other words, terms are built over expressions, while expressions are built over numbers and variables. In this case, variables ranges over real numbers ''and terms''. In other words, a variable can take a real number as a value, while another takes a term.
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 functor and number of subterms, their equality constraint can be replaced with the equality of subterms.
===Finite domains===
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 algorrithm backtracks. If the ___domain of a variable becomes a [[Singleton (mathematics)|singleton]], the variable can be assigned the unique value in its ___domain. The forms of consistency typically enforced are [[arc consistency]], [[hyper-arc consistency]], and [[bound consistency]]. The current ___domain of a variable can be inspected using specific literals; for example, <code>dom(X,D)</code> finds out the current ___domain <code>D</code> of a variable <code>X</code>.
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.
==The constraint store==
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 does not only contains the constraints derived from equating a literal with the head of a rewritten clause, but also the constraints of the body of clauses; second, it does not only contains constraints of the form <code>variable=value</code> but also constraints on reals or a finite ___domain, depending on the considered ___domain.
Domain-specific constraints may come to the constraint store both from the body of a clauses and from matching of a literals with a clause head: for example, if the interpreter rewrites the literal <code>A(X+2)</code> with a clause whose rewritten 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.
After a constraint is added to the constraint store, some operations may be performed on the constraint store. Depending on the ___domain, these may be arithmetic simplifications for reals or [[constraint propagation]] to enforce a form of [[local consistency]] for finite domains.
As a result, 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==
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 variables 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 the satisfiability of the constraint store. Indeed, when the interpreter adds a constraint to the constraint store, it only checks or 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 all variables of the constraint store enforces a complete satisfiability test to be performed.
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 much 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 typicall solved by a constraint logic program having the following structure:
solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)
When the interpreter evaluates the goal <code>solve(args)</code>, it places the rewritten body 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.
==Program reformulations==
A given constraint logic progam 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 <code>A(X):-labeling(X),X>0</code> is equivalent to <code>A(X):-X>0,labeling(X)</code>, the search that is performed when the interpreter encounters the labeling literal is on a constraint store that does not contain the constraint <code>X>0</code>. As a result, it may generate solutions, such as <code>X=-1</code>, 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, <code>A(X):-B(X),X>0</code> and <code>A(X):-X>0,B(X)</code> 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 evaluting 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 constrains. 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 beforehands that the evaluation of <code>B(X)</code> will result in a positive value for <code>X</code>, the programmer may add <code>X>0</code> before any occurrence of <code>B(X)</code>. As an example, <code>A(X,Y):-B(X),C(X)</code> will fail on the goal <code>A(-2,Z)</code>, but this is only found out during the evaluation of the subgoal <code>B(X)</code>. On the other hand, if the above clause is replaced by <code>A(X,Y):-X>0,A(X),B(X)</code>, the interpreter backtracks as soon as the constraint <code>X>0</code> is added to the constraint store, which happens before the evalation of <code>B(X)</code> even starts.
==Bottom-up evaluation==
Line 27 ⟶ 116:
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 <code>A(X):-X>0,X<10</code> is considered a fact as well. For this extended definition of facts, some facts may be equivalent while not syntactically equal. For example, <code>A(q)</code> is equivalent to <code>A(X):-X=q</code> and both are equivalent to <code>A(X):-X=Y, Y=a</code>. To solve this problem, facts are translated into a normal form in which the head contains a tuple of all-different variables; two facts are then equivalent if their bodies are equivalent on the variables of the head, that is, their sets of solutions are the same when restricted to these variables.
==History==
Constraint logic programming was introduced by Jaffar and Lassez in 1987. 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]].
==References==
*{{cite book
| first=Rina
| last=Dechter
| title=Constraint processing
| publisher=Morgan Kaufmann
| year=2003
| url=http://www.ics.uci.edu/~dechter/books/index.html
}} ISBN 1-55860-890-7
*{{cite book
| first=Krzysztof
| last=Apt
| title=Principles of constraint programming
| publisher=Cambridge University Press
| year=2003
}} ISBN 0-521-82583-0
*{{cite book
| first=Kim
| last=Marriot
| coauthors=Peter J. Stuckey
| title=Programming with constraints: An introduction
| year=1998
| publisher=MIT Press
}} ISBN 0-262-13341-5
*{{cite book
| first=Thom
| last=Frühwirth
| coauthors=Slim Abdennadher
| title=Essentials of constraint programming
| year=2003
| publisher=Springer
}} ISBN 3-540-67623-6
==See also==
*[[GNU Prolog]]
[[Category:Logic programming]]
[[Category:Constraint satisfaction]]
| |||