Constraint logic programming: Difference between revisions

Revision as of 12:36, 2 March 2006

Revision as of 12:35, 6 March 2006

Line 15:

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; 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. AtThe eachalgorithm step,proceed by iteratively removing the first element offrom the goal is removed and checkedanalyzing it. This checkinganalysis may result in a failure (backtracking) and may introduce new literals in thefront currentof the goal andor new constraints in the constraint store.

AtMore 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 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.

IfSome checks are done during these operations. In particular, the constraint store is unsatisfiablechecked for consistency every time a new constraint is added to it. In principle, backtrackingwhenever shouldthe beconstraint donestore is unsatisfiable the algorithm should backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, somea 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.