Subsections

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

 A hard Sudoku Puzzle 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 i + 1 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

Andreas Rossberg 2006-08-28