We can apply the idea to spaces. Suppose S is a space
in which at least one variable is not determined.
Then we can choose a constraint C and branch
S with C. Branching yields two spaces, one
obtained by adding a propagator for C, and one obtained
by adding a propagator for *C*.

The combination of constraint propagation and branching
yields a complete solution method
for finite domain problems. Given a problem, we set up a
space whose store contains the basic
constraints and whose propagators impose the nonbasic
constraints of the problem. Then we run
the propagators until they reached a fxpoint. If all
variables are determined, we are done.
Otherwise, we choose a not yet determined variable x
and an integer n such that x = n is consistent
with the constraint store and branch the space
with the constraint x = n. Since we can tell both
x = n and *x* *n* to the constraint store (the store
already knows a domain for x), chances are
that constraint propagation can restart in both spaces.

By proceeding this way we obtain a search tree as shown in figure 2. Each node of the tree corresponds to a space. Each leaf of the tree corresponds to a space that is either solved or failed. The search tree is always finite since there are only finitely many variables all a priori constrained to finite domains.

Andreas Rossberg 2006-08-28