Example: Safe

Problem Specification

The code of Professor Smart's safe is a sequence of 9 distinct nonzero digits C₁,..., C₉ such that the following equations and inequations are satisfied:

cC₄ - C₆ = C₇

C₁*C₂*C₃ = C₈ + C₉

C₂ + C₃ + C₆ < C₈

C₉ < C₈

$$\neq \neq$$

Can you determine the code?

Viewpoint and Branching Strategy

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

Script

fun safe space = 
   let
      val letters as #[c1,c2,c3,c4,c5,c6,c7,c8,c9]= 
          FD.intvarVec(space,9,#[(1,9)])
      fun not_equalv vec space = Vector.appi(fn (i,x) => 
                     post(space,FD(x) `<> `i `+ `1,FD.DOM)) vec
   in
      FD.distinct(space,letters,FD.DOM);
      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;
      FD.branch(space,letters,FD.B_SIZE_MIN,FD.B_MIN);
      {c1,c2,c3,c4,c5,c6,c7,c8,c9}
    end

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

Figure 10: Solution of the Safe Puzzle