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 nb₁,..., nb₉ 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 nb_i = { c₁,..., c_n} means that number i occurs in box c₁,..., c_n and { c₁,..., c_n} is a subset of {1, ..., 81}.

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

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