Constraint logic programming: Difference between revisions

Revision as of 12:40, 15 March 2006

Revision as of 10:34, 16 March 2006

Line 77:

==Labeling==

The labeling literals are used on variables over finite domains to check satisfiability or partial satisfiability of the constraint store and to find a satisfying assignment. A labeling literal is of the form <code>labeling([variables])</code>, where the argument is a list of variables over finite domains. Whenever the interpreter evaluates such a literal, it performs a search over the domains of the variables of the list to find an assignment that satisfies all relevant constraints. Typically, this is done by a form of [[backtracking]]: variables are evaluated in order, trying all possible values for each of them, and backtracking when inconsistency is detected.

The first use of the labeling literal is to actual check thesatisfiability or partial satisfiability of the constraint store. Indeed, whenWhen the interpreter adds a constraint to the constraint store, it only checks or enforces a form of local consistency on it. This operation may not detect inconsistency even if the constraint store is unsatisfiable. A labeling literal over alla set of variables enforces a satisfiability check of the constraints over these variables. As a result, using all variables mentioned in the constraint store enforcesresults ain completechecking satisfiability testof to bethe performedstore.

The second use of the labeling literal is to actually determine an evaluation of the variables that satisfies the constraint store. Without the labeling literal, variables are assigned values only when the constraint store contains a constraint of the form <code>X=value</code> and when local consistency reduces the ___domain of a variable to a single value. A labeling literal over some variables forces these variables to be evaluated. In other words, after the labeling literal has been considered, all variables are assigned a value.