Constraint logic programming: Difference between revisions

Revision as of 11:45, 2 March 2006

Revision as of 11:55, 2 March 2006

Line 1:

'''Constraint logic programming''' is a variant of [[logic programming]] that incorporate constraints as used in [[constraint satisfaction]].

A constraint logic programming is a logic program that includes constraints in the body of clauses. 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 the 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 backtraks 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 placing them in a set called ''constraint store'' that is supposed to be satisafiable. This constraint store contains all constraints assumed satisfiable during execution.

If the constraint store becomes unsatisfiable, the interpreter should backtrack, as the lineclause it is followingevaluating tocontains provea theconstraint goalthat iscannot be wrongsatisfied. In practice, some form of local consistency of the constraint store 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:

Line 13:

# labeling literals

During evaluation, a pair <math>\langle G,S \rangle</math> is maintained. The first element initially is the current goal; the second element is the constraint store. Initially, andthe current goal is replacedthe withgoal subgoalsand duringthe executionconstraint store is empty. TheAt secondeach step, the first element of the goal is anremoved initiallyand emptychecked. setThis ofchecking may introduce new literals in the current goal and new constraints, calledin the constraint store. ThisThe setcurrent accumulatesgoal contains the literals the interpreter is trying to prove; the constraint store contains all constraints that the algorithmintrpreter has assumesassumed satisfiable duringso executionfar.

At each step, 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 as the literal is chosen; its body is placed in front of the current goal; equality between the literal and the head of the clause is added to the constraint store. ('''The choice of this clause may be based on an order of the clauses or may be non-deterministic?''').

If the constraint store is unsatisfiable, backtracking should be done. However, checking unsatisfiability at each step would be inefficient. For this reason, some form of local consistency is checked instead.

When the current goal is empty, a regular logic program interpreter stops and output the current substitution. In this condition, a constraint logic program stops,. but onlyIts output withmay be the current domains as reduced via the local consistency conditions on the constraint store. ('''dependsActual onsatisfiability theand interpreter?''').finding Actuala satisfiabilitysolution 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 an assignment to these variables that satisfy all constraints ('''or, finds a complete satisfying assignment and restrict to these variables?''').