Pi Day Sudoku 2009
Brainfreeze Puzzles has a Pi day Sudoku competition:
Pi Day is a celebration of the number π that occurs every March 14 (3.14...). Math geeks all over the world celebrate their math-geekiness on this day with pie-eating contests, recitations of the digits of pi, and occasionally fundraisers where math faculty get hit in the face with pies. At Brainfreeze Puzzles we celebrate Pi Day - how else? - with a Sudoku puzzle....
Rules: Fill in the grid so that each row, column, and jigsaw region contains 1-9 exactly once and π [Pi] three times.
The puzzle is also here (as a PDF file)
Models
I programmed this puzzle in both Comet (using the constraint programming module) and MiniZinc using different solvers. The models use the same principle of solving the problem: a (homebrewn)all different except 0
constraint and counting exactly 3 occurrences of Pi for each row/column and region.
All the solvers give the same unique answer, which of course may mean that there is some systematic error on my part.
Comet
Comet solves the problem in about 9 seconds with the following statistics, using
exploreall
to make sure that it is a unique solution.
time: 8821
#choices = 9999
#fail = 16231
#propag = 23168886
Somewhat surprisingly selecting j
before i
in the forall
loop, gives an improvment from 15 seconds to 9 seconds. This was the same labeling strategy that was used for improving Nonogram (see Comet: Nonogram improved: solving problem P200 from 1:30 minutes to about 1 second). Here is the labeling:
// reversing i and j gives faster solution
forall(j in 1..n, i in 1..n: !x[i,j].bound()) {
tryall(v in V : x[i,j].memberOf(v)) by(v)
m.label(x[i,j], v);
onFailure
m.diff(x[i,j], v);
}
MiniZinc and Gecode/flatzinc
Interestingly, the same improvement was observed with MiniZinc and the Gecode/flatzinc solver (the interface to Gecode). Here is the labeling function, with the same swapping ofi
and j
(I didn't know that this mattered in MiniZinc).
solve :: int_search([x[i,j] | j, i in 1..n], "input_order", "indomain", "complete") satisfy;
With the swap, the time went from 16 seconds to 10 seconds with the following statistics:
propagators: 9460
propagations: 13461717
failures: 11221
clones: 11221
commits: 31478
peak memory: 5638 KB
mzx.pl sudoku_pi.mzn --num 2 9,41s user 0,72s system 99% cpu 10,139 total
Fzntini, FlatZinc, ECLiPSe and searching for the first solution
MiniZinc's builtin solver flatzinc and fzntini (a SAT solver) only shows one solution and no statistics.* fzntini
solve problem in about 13 seconds
* flatzinc
takes 3 seconds.
The ECLiPSe's MiniZinc solver ic
takes 6.5 seconds using the same labeling as Gecode/flatzinc. No statistics is shown for this solver either.
For comparison both Comet and Gecode/flatzinc shows the first solutions in 2.5 seconds.