Subsections


Example: Sudoku Problem - Revisited

In section 3.3 is both given a formulation and a solution to a Sudoku puzzle. There are also shown two different, mutually redundant viewpoints for the problem. In section 6.3 you have already seen a realization of the first viewpoint. Now, you are presented a realization of the second approach.

Viewpoint

The variables nb1,..., nb9 represent the numbers 1, ..., 9, and the domain of every number is the set P{1, ..., 81}, i.e. the boxes a number occurs; an assignment nbi = { c1,..., cn} means that number i occurs in box c1,..., cn and { c1,..., cn} is a subset of {1, ..., 81}.

Given the following tabular, initially, the lower bound of nb1 is { 8, 31, 43, 55} and its upper bound is the set {1, ..., 81}. The variable nb2 has the lower bound {2, 51, 63, 67}, nb3 the lower bound {10, 39, 49, 59, 74}, nb4 the lower bound { 19, 47, 69, 79} and nb5 the lower bound { 23,29,42,53,64} for example. Such as nb1's upper bound, the upper bound of nb2,..., nb5 is {1, ..., 81}.

A Sudoku Puzzle
2 6 8 1
3 7 8 6
4 5 7
5 1 7 9
3 9 5 1
4 3 2 5
1 3 2
5 2 4 9
3 8 4 6

Branching Strategy

We use a strategy that the variable with the minimal cardinality between its lower and upper bound and picks the minimal value of the selected variable first.

Script

In listing 35 the input is a list of tuples (a,b), where a is a 'number' value and b is the list of those numbers positions.
val inputlist2 = [(1,[8,31,43,55]),(2,[2,51,63,67]),
                  (3,[10,39,49,59,74]),(4,[19,47,69,79]),
                  (5,[23,29,42,53,64]),(6,[3,18,80]),
                  (7,[13,27,33]),(8,[7,15,75]),
                  (9,[35,40,72])]

fun sudoku2 inputlist space = 
  let
     val numbers = Vector.tabulate(9,fn x => 
                        FS.upperBound(space,#[(1,81)]))
     val rows = List.tabulate(9,fn x =>(x*9+9-8,x*9+9)) 
     val columns = List.tabulate(9,fn y => 
                       Vector.tabulate(9,fn x =>(x*9+1+y,x*9+1+y)))
     val boxes1 = List.tabulate(3,fn y => 
                   Vector.tabulate(3,fn x =>(x*9+1+y*3,x*9+3+y*3)))
     val boxes2 = List.tabulate(3,fn y => 
                   Vector.tabulate(3,fn x =>(x*9+28+y*3,x*9+30+y*3)))
     val boxes3 = List.tabulate(3,fn y => 
                   Vector.tabulate(3,fn x =>(x*9+55+y*3,x*9+57+y*3)))
     val boxes = List.concat([boxes1,boxes2,boxes3])
     fun constr l = 
       List.app(fn y => 
                 let
                    val tmp1 = FS.Value.make(space,y)
                 in
                    Vector.app(fn x => 
                     let 
                        val tmp2 = FS.setvar space 
                     in
                        FS.relOp(space,x,FS.INTER,tmp1,FS.SEQ,tmp2);
                        FS.cardRange(space,1,1,tmp2)
                     end)numbers
                 end)l
     fun fsDisjoint ([]) = ()
       | fsDisjoint (x::xs) = 
            (List.app(fn y => FS.rel(space,y, FS.DISJ,x))xs;
             fsDisjoint(xs))
  in
    (* use next constraint only, if inputlist is used *)
     List.app(fn(x,y) => 
       List.app(fn z => 
                  let 
                     val tmp = FS.Value.make(space,#[(z,z)])
                  in
                     FS.rel(space,Vector.sub(numbers,x-1),FS.SUP,tmp)
                  end)y)inputlist;
     Vector.app(fn x => FS.cardRange(space,9,9,x))numbers;
    (* the domains of all numbers are pairwise distinct *)
     fsDisjoint(Vector.toList numbers);
    (* distinct numbers in rows *)
     List.app(fn(y,z)=>
       let 
          val tmp1 = FS.Value.make(space,#[(y,z)]) 
       in
          Vector.app(fn x => 
                      let 
                         val tmp2 = FS.setvar space 
                      in
                         FS.relOp(space,x,FS.INTER,tmp1,FS.SEQ,tmp2);
                         FS.cardRange(space,1,1,tmp2)
                      end)numbers
       end)rows;
    (* distinct numbers in columns *)
     constr domainvecs;  
    (* distinct numbers in 3 x 3 boxes *)
     constr boxes;   
     FS.setvarbranch(space,numbers,FS.FSB_MIN_CARD,FS.FSB_MIN); 
     numbers
  end

Andreas Rossberg 2006-08-28