# 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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