--- a/src/HOL/ex/Sudoku.thy Wed Dec 03 09:53:58 2008 +0100
+++ b/src/HOL/ex/Sudoku.thy Wed Dec 03 14:02:24 2008 +0000
@@ -1,7 +1,7 @@
(* Title: Sudoku.thy
ID: $Id$
Author: Tjark Weber
- Copyright 2005-2007
+ Copyright 2005-2008
*)
header {* A SAT-based Sudoku Solver *}
@@ -11,9 +11,12 @@
begin
text {*
- Please make sure you are using an efficient SAT solver (e.g. zChaff)
+ Please make sure you are using an efficient SAT solver (e.g., zChaff)
when loading this theory. See Isabelle's settings file for details.
+ Using zChaff, each Sudoku in this theory is solved in less than a
+ second.
+
See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
LPAR'05) for further explanations.
*}
@@ -135,4 +138,180 @@
refute
oops
+text {*
+ Some "exceptionally difficult" Sudokus, taken from
+ \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}
+ (accessed December 2, 2008).
+*}
+
+text {*
+\begin{verbatim}
+Rating Program: gsf's sudoku q1 (rating)
+Rating: 99408
+Poster: JPF
+Label: Easter Monster
+1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1
+1 . . | . . . | . . 2
+. 9 . | 4 . . | . 5 .
+. . 6 | . . . | 7 . .
+------+-------+------
+. 5 . | 9 . 3 | . . .
+. . . | . 7 . | . . .
+. . . | 8 5 . | . 4 .
+------+-------+------
+7 . . | . . . | 6 . .
+. 3 . | . . 9 | . 8 .
+. . 2 | . . . | . . 1
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ 1 x12 x13 x14 x15 x16 x17 x18 2
+ x21 9 x23 4 x25 x26 x27 5 x29
+ x31 x32 6 x34 x35 x36 7 x38 x39
+ x41 5 x43 9 x45 3 x47 x48 x49
+ x51 x52 x53 x54 7 x56 x57 x58 x59
+ x61 x62 x63 8 5 x66 x67 4 x69
+ 7 x72 x73 x74 x75 x76 6 x78 x79
+ x81 3 x83 x84 x85 9 x87 8 x89
+ x91 x92 2 x94 x95 x96 x97 x98 1 "
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: gsf's sudoku q1 (Processing time)
+Rating: 4m19s@2 GHz
+Poster: tarek
+Label: tarek071223170000-052
+..1..4.......6.3.5...9.....8.....7.3.......285...7.6..3...8...6..92......4...1...
+. . 1 | . . 4 | . . .
+. . . | . 6 . | 3 . 5
+. . . | 9 . . | . . .
+------+-------+------
+8 . . | . . . | 7 . 3
+. . . | . . . | . 2 8
+5 . . | . 7 . | 6 . .
+------+-------+------
+3 . . | . 8 . | . . 6
+. . 9 | 2 . . | . . .
+. 4 . | . . 1 | . . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 x12 1 x14 x15 4 x17 x18 x19
+ x21 x22 x23 x24 6 x26 3 x28 5
+ x31 x32 x33 9 x35 x36 x37 x38 x39
+ 8 x42 x43 x44 x45 x46 7 x48 3
+ x51 x52 x53 x54 x55 x56 x57 2 8
+ 5 x62 x63 x64 7 x66 6 x68 x69
+ 3 x72 x73 x74 8 x76 x77 x78 6
+ x81 x82 9 2 x85 x86 x87 x88 x89
+ x91 4 x93 x94 x95 1 x97 x98 x99"
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1
+Rating: 11.9
+Poster: tarek
+Label: golden nugget
+.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....
+. . . | . . . | . 3 9
+. . . | . . 1 | . . 5
+. . 3 | . 5 . | 8 . .
+------+-------+------
+. . 8 | . 9 . | . . 6
+. 7 . | . . 2 | . . .
+1 . . | 4 . . | . . .
+------+-------+------
+. . 9 | . 8 . | . 5 .
+. 2 . | . . . | 6 . .
+4 . . | 7 . . | . . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 x12 x13 x14 x15 x16 x17 3 9
+ x21 x22 x23 x24 x25 1 x27 x28 5
+ x31 x32 3 x34 5 x36 8 x38 x39
+ x41 x42 8 x44 9 x46 x47 x48 6
+ x51 7 x53 x54 x55 2 x57 x58 x59
+ 1 x62 x63 4 x65 x66 x67 x68 x69
+ x71 x72 9 x74 8 x76 x77 5 x79
+ x81 2 x83 x84 x85 x86 6 x88 x89
+ 4 x92 x93 7 x95 x96 x97 x98 x99"
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: dukuso's suexrat9
+Rating: 4483
+Poster: coloin
+Label: col-02-08-071
+.2.4.37.........32........4.4.2...7.8...5.........1...5.....9...3.9....7..1..86..
+. 2 . | 4 . 3 | 7 . .
+. . . | . . . | . 3 2
+. . . | . . . | . . 4
+------+-------+------
+. 4 . | 2 . . | . 7 .
+8 . . | . 5 . | . . .
+. . . | . . 1 | . . .
+------+-------+------
+5 . . | . . . | 9 . .
+. 3 . | 9 . . | . . 7
+. . 1 | . . 8 | 6 . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 2 x13 4 x15 3 7 x18 x19
+ x21 x22 x23 x24 x25 x26 x27 3 2
+ x31 x32 x33 x34 x35 x36 x37 x38 4
+ x41 4 x43 2 x45 x46 x47 7 x49
+ 8 x52 x53 x54 5 x56 x57 x58 x59
+ x61 x62 x63 x64 x65 1 x67 x68 x69
+ 5 x72 x73 x74 x75 x76 9 x78 x79
+ x81 3 x83 9 x85 x86 x87 x88 7
+ x91 x92 1 x94 x95 8 6 x98 x99"
+ refute
+oops
+
+text {*
+\begin{verbatim}
+Rating Program: dukuso's suexratt (10000 2 option)
+Rating: 2141
+Poster: tarek
+Label: golden nugget
+.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....
+. . . | . . . | . 3 9
+. . . | . . 1 | . . 5
+. . 3 | . 5 . | 8 . .
+------+-------+------
+. . 8 | . 9 . | . . 6
+. 7 . | . . 2 | . . .
+1 . . | 4 . . | . . .
+------+-------+------
+. . 9 | . 8 . | . 5 .
+. 2 . | . . . | 6 . .
+4 . . | 7 . . | . . .
+\end{verbatim}
+*}
+
+theorem "\<not> sudoku
+ x11 x12 x13 x14 x15 x16 x17 3 9
+ x21 x22 x23 x24 x25 1 x27 x28 5
+ x31 x32 3 x34 5 x36 8 x38 x39
+ x41 x42 8 x44 9 x46 x47 x48 6
+ x51 7 x53 x54 x55 2 x57 x58 x59
+ 1 x62 x63 4 x65 x66 x67 x68 x69
+ x71 x72 9 x74 8 x76 x77 5 x79
+ x81 2 x83 x84 x85 x86 6 x88 x89
+ 4 x92 x93 7 x95 x96 x97 x98 x99"
+ refute
+oops
+
end