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 A(X,Y) :- X+Y>0, B(X), C(Y). In this clause, X+Y>0 is a constraint; A(X,Y), B(X), and C(Y) are literals like in regular logic programming. Intuitively, this clause tells one condition under which the statement A(X,Y) holds: this is the case if X+Y is greater than zero and both B(X) and C(Y) 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 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 backtracks, trying to use other clauses for proving the goal. In practice, satisfiability of the constraint store is checked using a form of local consistency, which does not always detect inconsistency. A complete check for satisfiability can be explicitely forced by using a specific literal.
Overview
Formally, constraint logic programs are like regular logic programs, but the body of clause can contain constraints and labeling literals (described below), 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 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 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 should backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, a form of local consistency is checked instead.
When the current goal is empty, a regular logic program interpreter would stop and output the current substitution. In the same conditions, a constraint logic program also stops, and its output may be the current domains as reduced via the local consistency conditions on the constraint store. Actual satisfiability and finding a solution is enforced via labeling literals. In particular, whenever the interpreter encounters the literal during the evaluation of a clause, it runs a satisfiability checker on the current constraint store to try and find a satisfying assignment.
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 must be present, as the interpreter adds t1=t2 to the goal whenever a literal P(...t1...) is replaced with the body of a clause whose rewritten head is P(...t2...).
Tree terms
In the basic case of constraint logic programming, terms are variables, constants, and functors applied to other terms. In this case, the only considered constraints are equality or disequality between terms. Equality is particularly important, as constraints t1=t2 are often generated by the intepreter.
A constraint t1=t2 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 numbers 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 A(X+1)</math> and the interpreter has chosen a clause that is A(Y-1):-Y=1 after rewriting is variables, the constraints added to the current goal are X+1=Y-1 and . The rules of simplification used for functors are obviously not used: X+1=Y-1 is not unsatisfiable just because the first expression is built using + and the second using -.
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.
Reference
- Dechter, Rina (2003). Constraint processing. Morgan Kaufmann. ISBN 1-55860-890-7
- Apt, Krzysztof (2003). Principles of constraint programming. Cambridge University Press. ISBN 0-521-82583-0
- Marriot, Kim (1998). Programming with constraints: An introduction. MIT Press.
{{cite book}}: Unknown parameter |coauthors= ignored (|author= suggested) (help) ISBN 0-262-13341-5
- Frühwirth, Thom (2003). Essentials of constraint programming. Springer.
{{cite book}}: Unknown parameter |coauthors= ignored (|author= suggested) (help)CS1 maint: multiple names: authors list (link) ISBN 3-540-67623-6