Example: Safe

Problem Specification

The code of Professor Smart's safe is a sequence of 9 distinct nonzero digits C1,..., C9 such that the following equations and inequations are satisfied:
cC4 - C6 = C7  
C1*C2*C3 = C8 + C9  
C2 + C3 + C6 < C8  
C9 < C8  
C1 $\displaystyle \neq$ 1,..., C9 $\displaystyle \neq$ 9      

Can you determine the code?

Viewpoint and Branching Strategy

You should model the problem by choosing a variable for every digit C1,..., C9 and branch over these variables with the standard first-fail strategy. This time, the variables range over {1, ..., 9}.


fun safe space = 
      val letters as #[c1,c2,c3,c4,c5,c6,c7,c8,c9]= 
      fun not_equalv vec space = Vector.appi(fn (i,x) => 
                     post(space,FD(x) `<> `i `+ `1,FD.DOM)) vec
      post(space,FD(c4)`- FD(c6) `= FD(c7),FD.DOM);
      post(space,FD(c1)`* FD(c2)`* FD(c3)`= FD(c8)`+ FD(c9),FD.DOM);        
      post(space,FD(c2)`+ FD(c3)`+ FD(c6)`< FD(c8),FD.DOM);
      post(space,FD(c9)`< FD(c8),FD.DOM);
      not_equalv letters space;

Listing 2 shows a simple script for the Safe Puzzle. First, the script introduces a vector of type intvar, with one finite domain variable for every digit. The script also defines two additional temporary finite domain variables whose use will be explained later and a help function that posts the constraint c.i $ \neq$ i   for every   i = 1,..., 9. In the application part of the let - construct, the first constraint ensures that all digits are distinct. The next six constraints that are posted guarantee that the equations and inequations of the Safe problem are satisfied [*].Finally the branching strategy branches over the vector letters.

The following two figures 9 and 10 show the resulting search-tree of the Safe Puzzle and its unique solution {4 3 1 8 9 2 6 7 5}.

Figure 9: Search-tree of the Safe Puzzle
\includegraphics[scale=1.0, clip]{figs/explorer_safe_expl.eps}
Figure 10: Solution of the Safe Puzzle
\includegraphics[scale=1.0, clip]{figs/solution_safe2.eps}

Andreas Rossberg 2006-08-28