# HG changeset patch
# User webertj
# Date 1228312944 0
# Node ID 610fe33ca358f91174c4e65924bc16c161d430e5
# Parent  1860f016886d3fdad5873e2ca985fccbaad50341
more examples

diff -r 1860f016886d -r 610fe33ca358 src/HOL/ex/Sudoku.thy
--- 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