Example: Sudoku Problem

In section 6.3 and section 11.7 you have already seen how the Sudoku Problem can be realized in Alice. These two models - one with finite domain constraints, the other with finite set constraints - now are put together into one combined model.

New Problem Description

The Sudoku Problem example in section 3.3 can be solved without any search at all. To underline the advantages of a combined model, we need a Problem that is harder to solve. Below you are given a problem that is hard and needs search to be solved.

3 6 1

9 7 5 8

9 2

8 7 4

3 6

1 2 8 9 4

5 1

Viewpoint and Constraints

The viewpoint of the new combined model consists in a set X, the union of the problem variables of the scripts in listing 11 and 35 with their respective domains. Also the constraints of both models are put together. Additionally, you have a set of channeling constraints of the form

grid'[i] = j $\Leftrightarrow$ i + 1 $\in$ numbers[ j-1],

where grid is the vector of problem variables from the first model and numbers the vector of problem variables from the second model. Note, that the channeling constraints are realized with Reified Constraints among other things.

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

val inputlist_hard=[(0,5,3),(0,7,6),(1,7,1),(2,1,9),
                    (2,2,7),(2,3,5),(2,7,8),(3,4,9),
                    (3,6,2),(4,2,8),(4,4,7),(4,6,4),
                    (5,2,3),(5,4,6),(6,1,1),(6,5,2),
                    (6,6,8),(6,7,9),(7,1,4),(8,1,5),
                    (8,3,1)]                 

fun sudoku inputlist space = 
  let
     val grid = Vector.tabulate(9,fn x => 
                         FD.rangeVec(space,9,(1,9)))
     val grid' = Vector.concat(Vector.toList(grid))
     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 domainvecs = 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 flatten([])= []
       | flatten(x::xs)= x@flatten(xs)
     fun box(x,y)= flatten(List.tabulate(3,fn k => 
                            List.tabulate(3,fn z =>(k+x,z+y))))
     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
     List.app(fn(x,y,z) => FD.relI(space,Vector.sub
                          (Vector.sub(grid,x),y),FD.EQ,z))inputlist;
    (* distinct values in rows *)
     Vector.app(fn x => FD.distinct(space,x,FD.DOM))grid;
    (* distinct values in columns *)
     Vector.appi(fn(i,y)=> FD.distinct(space,Vector.map(fn x => 
                                  Vector.sub(x,i))grid,FD.DOM))grid;
    (* distinct values in 3 x 3 boxes *)
     Vector.app(fn(k,l)=> 
       let
          val box' = Vector.map(fn(x,y) => 
                              Vector.sub(Vector.sub(grid,x),y))
                       (Vector.fromList(box(k,l)))
       in
          FD.distinct(space,box',FD.DOM)
      end)(#[(0,0),(0,3),(0,6),(3,0),(3,3),(3,6),(6,0),(6,3),(6,6)]);
     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;   
    (* channeling constraints: grid'[i] = j <=> i+1 in numbers[j-1] *)
     List.app(fn i => 
          List.app(fn j =>
             let
                val bvar = FD.boolvar space
             in  
                FD.Reified.relI(space,Vector.sub(grid',i-1),
                                     FD.EQ,j,bvar);
                FS.domR(space,Vector.sub(numbers,j-1),
                                     FS.SUP,#[(i,i)],bvar)
             end)
             (List.tabulate(9,fn x => x+1)))
         (List.tabulate(81,fn x => x+1));
     FS.setvarbranch(space,numbers,FS.FSB_MIN_CARD,FS.FSB_MIN); 
     numbers
  end

Below, the three realizations of the a hard Sudoku Problem 12.2.1 are compared:

Problem realized with Choices Failures Solutions

finite domain constraints 28 28 1

finite set constraints 12 12 1

combined model 10 10 1