|<< Prev||- Up -||Next >>|
example of communicating propagators
Two propagators that share a variable can communicate with each other through the constraint store. To see an example for communicating propagators, suppose we have two propagators imposing the constraints
over a constraint store containing the following information about and :
As is, the first propagator cannot do anything. The second propagator, however, can narrow the domains of both and :
Now the first propagator can narrow the domain of :
Now the second propagator can narrow the domains of both and :
This once more activates the first propagator, which narrows the domain of :
Now the second propagator gets active once more and determines the values of and :
telling a constraint
Given a constraint store storing a constraint and a propagator imposing a constraint , the propagator can tell to the constraint store a basic constraint if the conjunction entails and adds new and consistent information to the store. To tell a constraint to a constraint store storing the constraint means to update the store so that it holds the conjunction .
operational and declarative semantics of propagators
The operational semantics of a propagator determines whether the propagator can tell the store a basic constraint or not. The operational semantics of a propagator must of course respect the declarative semantics of the propagator, which is given by the constraint the propagator imposes.
We require that the constraint store be always consistent; that is, there must always be at least one variable assignment that satisfies all constraints in the constraint store.
We say that a propagator is inconsistent if there is no variable assignment that satisfies both the constraint store and the constraint imposed by the propagator (e.g., over and ). We say that a propagator is failed if its operational semantics realizes that it is inconsistent.
We say that a propagator is entailed if every variable assignment that satisfies the constraint store also satisfies the constraint imposed by the propagator (e.g., over and ). As soon as the operational semantics of a propagator realizes that the propagator is entailed, the propagator ceases to exist.
We require that the operational semantics of a propagator detects inconsistency and entailment at the latest when the store determines all variables of the propagator.
failed, stable, and solved spaces
We say that a space is failed if one of its propagators is failed. We say that a space is stable if all of its propagators are stable. We say that a space is solved if it is not failed and there are no propagators left.
propagation order does not matter
When a space is created, its propagators start to tell basic constraints to the constraint store. This propagation activity continues until the space becomes stable. An important property of constraint propagation as we consider it here is the fact that the order in which the propagators tell information to the store does not matter. When we start a space repeatedly from the same state, it will either always fail or always arrive at the same constraint store (up to logical equivalence).
|<< Prev||- Up -||Next >>|