Example: Sukoku Puzzle

The problem description of the Sudoku Puzzle is already given in section 3.3. There are also shown two viewpoints for this problem. Here, we want to realize the first viewpoint in Alice.

Viewpoint

The variables x₁,..., x₈₁ represent all boxes in the grid, and the domain of each variable is the set of integers {1, ..., 9}, i.e. the values every box can have; an assignment x_i = c means that the i-th box has the value c.

In the following example, the domain of the variables x₁, x₄, x₅, x₆, x₉, x₁₁, x₁₂, x₁₄, x₁₆, x₁₇ is unrestricted, i.e. values of the set {1, ..., 9} ( in the first two rows). By contrast, the domain of the variables in the first two rows, that are not already mentioned above, is determined.

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 picks the variable with the smallest lower bound, splits the domain of the selected variable and tries the upper part of the domain first. This strategy leads to a smaller search tree than the standard first-fail strategy, which tries the least possible value of the selected variable first.

Script

The procedure sukoku1 gets as argument a list of triples (a,b,c), where (a,b) is the address of the variable in the grid and c is its value. It first constrains the boxes to the input and then it posts the constraints given in the problem description.

(* the inputlist is a list of triples(a,b,c) where
   (a,b) is the address of the variable in the grid
   and c is its value  *)

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

fun sudoku1 inputlist space =
    let
        val grid = Vector.tabulate(9,fn x => 
                           FD.rangeVec(space,9,(1,9)))
        val grid' = Vector.concat(Vector.toList(grid))
        fun flatten([])= []
              | flatten(x::xs)= x@flatten(xs)
        (* box constructs a list of elements representing
           one 3 x 3 box *)
        fun box(x,y)= flatten(List.tabulate(3,fn k => 
                   List.tabulate(3,fn z =>(k+x,z+y))))
    in 
        (* use next constraint,only when imputlist is used;
           updates the values from inputlist to grid *)
        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)]);
        FD.branch(space,grid',FD.B_MIN_MIN,FD.B_SPLIT_MIN);
        grid
    end

Given this input list, the problem has an unique solution and can be solved without any search at all.