Constraint logic programming: Difference between revisions

Revision as of 12:35, 6 March 2006

Revision as of 12:27, 7 March 2006

Line 1:

'''Constraint logic programming''' is a variant of [[logic programming]] that incorporates constraints as used in [[constraint satisfaction]]. A constraint logic program is a logic program that includes constraints in the body of clauses.

AAn example of a clause including a constraint logicis programming<code>A(X,Y) :- X+Y>0, B(X), C(X)</code>. In this clause, <code>X+Y>0</code> is a logicconstraint; program<code>A(X,Y)</code>, that<code>B(X)</code>, includesand constraints<code>C(X)</code> inare theliterals bodylike ofin clausesregular logic programming. A clause can be used to prove the goal if its constraints are satisfied and its literals can be proved. More precisely, the set of all constraints of clauses used in a derivation is supposed to be satisfiable in order for the derivation to be valid.

When the interpreter scans the body of a clause, it [[Backtracking|backtrack]]s if a constraint is not satisfied or a literal cannot be proved. There is a difference in how constrains and literals are handled: literals are proved by recursively evaluating other clauses; constraints are checked by placingplaced them in a set called ''constraint store'' that is supposed to be satisafiable. This constraint store contains all constraints assumed satisfiable during execution. Evaluating a literal may also involve adding constraints to the constraint store.

If the constraint store becomes unsatisfiable, the interpreter should backtrack, as the clause it is evaluating contains a constraint that cannot be satisfied. In practice, some form of [[local consistency]] is used as an approximation of satisfiability. However, the goal is truly proved only if the constraint store is actually satisfiable.

Line 13:

# labeling literals

During evaluation, a pair <math>\langle G,S \rangle</math> is maintained. The first element is the current goal; the second element is the 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 be present 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 algorithminterpreter proceed by iteratively removing the first element from the goal and analyzing it. This analysis may result in a failure, which produces a (backtracking). andThis analysis may also introduce new literals in front of the goal or new constraints in the constraint store.

More precisely, 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, it is treated as in regular logic programming: a clause whose head has the same top-level predicate asof 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 current goal; equalityequalities betweenof arguments of the literal and the head of the rewritten clause ishead addedare toplaced in front of the constraintgoal as storewell.

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 <math>labeling(variables)</math> during the evaluation of a clause, it runs a satisfiability checker on the current constraint store to try and find a satisfying assignment.

Constraint logic programs usually contain constraints from a given language. In the simplest case, the only considered constraints are equality of terms; this corresponds to regular logic programming. Two other languages are also used: constraints over reals and constraints over finite domains, the latter being identified with integers.

==Reference==

Line 40 ⟶ 42:

| 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

[[Category:Logic programming]]