Content deleted Content added
→Finite domains: how a ___domain is specified |
terms and variables + labeling |
||
Line 48:
The ___domain of a variable may be reduced during execution. Indeed, as the interpreter adds constraints to the constraint store, it performs [[constraint propagation]] to enforce a form of [[local consistency]], and these operations may reduce the ___domain of variables. If the ___domain of a variable becomes empty, the constraint store is inconsistent, and the algorrithm backtracks. If the ___domain of a variable becomes a [[Singleton (mathematics)|singleton]], the variable can be assigned the unique value in its ___domain. The forms of consistency typically enforced are [[arc consistency]], [[hyper-arc consistency]], and [[bound consistency]]. The current ___domain of a variable can be inspected using specific literals such as <code>dom(X,D)</code> to find out the current ___domain <code>D</code> of a variable <code>X</code>.
As for domains of reals, functors can be used with domains of integers. In this case, a term can be an expression over integers, a constant, or the application of a functor over other terms. A variable can take an arbitrary term as a value, if its ___domain has not been specified to be a set of integers or constants.
==Labeling==
The labeling literals are used to check satisfiability or partial satisfiability of the constraint store and to find a satisfying assignment. Whenever the interpreter evaluates a literal <code>labeling([variables])</code>, it performs a search over the domains of variables 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 the satisfiability of the constraint store. Indeed, when 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 all variables of the constraint store enforces a complete satisfiability test to be performed.
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.
Typically, constraint logic programs are written in such a way labeling literals are evaluated only after as much constraints as possible have been accumulated in the constraint store. This is because labeling literals enforce search, and search is more efficient if there are more constraints to be satisfied. A [[constraint satisfaction problem]] is typicall solved by a constraint logic program having the following structure:
solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)
When the interpreter evaluates the goal <code>solve(args)</code>, it places the rewritten body of the first clause in the current goal. Since the first goal is <code>constraints(X')</code>, the second clause is evaluated, and this operation moves all constraints in the current goal and eventually in the constraint store. The literal <code>labeling(X')</code> is then evaluated, forcing a search for a solution of the constraint store. Since the constraint store contains exactly the constraints of the original constraint satisfaction problem, this operation searches for a solution of the original problem.
==Reference==
| |||