Constraint logic programming: Difference between revisions

Revision as of 14:01, 7 March 2006

Revision as of 12:22, 8 March 2006

Line 1:

'''Constraint logic programming''' is a variant of [[logic programming]] that incorporates constraints asincluding usedconcepts infrom [[constraint satisfaction]]. A constraint logic program is a logic program that includescontains 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. AIntuitively, this clause cantells beone usedcondition tounder provewhich the goalstatement if<code>A(X,Y)</code> itsholds: constraintsthis are satisfied and its literals can be proved. More precisely,is the setcase ofif all constraints of clauses used in a derivation<code>X+Y</code> is supposedgreater tothan bezero satisfiableand inboth order<code>B(X)</code> forand the<code>C(Y)</code> derivation to beare validtrue.

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|backtrack]]s, 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.

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 placed them in a set called ''constraint store''. This constraint store contains all constraints assumed satisfiable during execution. Evaluating a literal may also involve adding constraints to the constraint store.

==Overview==

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.

Formally, constraint logic programs are like regular logic programs, but the body of clause can contain: