Given the following tabular, initially, the lower bound of nb1
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