Subsections

## 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 1,..., C9 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}.

### 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 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}.

Andreas Rossberg 2006-08-28