src/HOL/ex/Sudoku.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28949 610fe33ca358
child 35416 d8d7d1b785af
permissions -rw-r--r--
added lemmas
     1 (*  Title:      Sudoku.thy
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2005-2008
     5 *)
     6 
     7 header {* A SAT-based Sudoku Solver *}
     8 
     9 theory Sudoku
    10 imports Main
    11 begin
    12 
    13 text {*
    14   Please make sure you are using an efficient SAT solver (e.g., zChaff)
    15   when loading this theory.  See Isabelle's settings file for details.
    16 
    17   Using zChaff, each Sudoku in this theory is solved in less than a
    18   second.
    19 
    20   See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
    21   LPAR'05) for further explanations.
    22 *}
    23 
    24 datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
    25 
    26 constdefs
    27   valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
    28 
    29   "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==
    30     (x1 \<noteq> x2) \<and> (x1 \<noteq> x3) \<and> (x1 \<noteq> x4) \<and> (x1 \<noteq> x5) \<and> (x1 \<noteq> x6) \<and> (x1 \<noteq> x7) \<and> (x1 \<noteq> x8) \<and> (x1 \<noteq> x9)
    31     \<and> (x2 \<noteq> x3) \<and> (x2 \<noteq> x4) \<and> (x2 \<noteq> x5) \<and> (x2 \<noteq> x6) \<and> (x2 \<noteq> x7) \<and> (x2 \<noteq> x8) \<and> (x2 \<noteq> x9)
    32     \<and> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9)
    33     \<and> (x4 \<noteq> x5) \<and> (x4 \<noteq> x6) \<and> (x4 \<noteq> x7) \<and> (x4 \<noteq> x8) \<and> (x4 \<noteq> x9)
    34     \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9)
    35     \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9)
    36     \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9)
    37     \<and> (x8 \<noteq> x9)"
    38 
    39 constdefs
    40   sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    41     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    42     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    43     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    44     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    45     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    46     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    47     digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    48     digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
    49 
    50   "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19
    51           x21 x22 x23 x24 x25 x26 x27 x28 x29
    52           x31 x32 x33 x34 x35 x36 x37 x38 x39
    53           x41 x42 x43 x44 x45 x46 x47 x48 x49
    54           x51 x52 x53 x54 x55 x56 x57 x58 x59
    55           x61 x62 x63 x64 x65 x66 x67 x68 x69
    56           x71 x72 x73 x74 x75 x76 x77 x78 x79
    57           x81 x82 x83 x84 x85 x86 x87 x88 x89
    58           x91 x92 x93 x94 x95 x96 x97 x98 x99 ==
    59 
    60        valid x11 x12 x13 x14 x15 x16 x17 x18 x19
    61      \<and> valid x21 x22 x23 x24 x25 x26 x27 x28 x29
    62      \<and> valid x31 x32 x33 x34 x35 x36 x37 x38 x39
    63      \<and> valid x41 x42 x43 x44 x45 x46 x47 x48 x49
    64      \<and> valid x51 x52 x53 x54 x55 x56 x57 x58 x59
    65      \<and> valid x61 x62 x63 x64 x65 x66 x67 x68 x69
    66      \<and> valid x71 x72 x73 x74 x75 x76 x77 x78 x79
    67      \<and> valid x81 x82 x83 x84 x85 x86 x87 x88 x89
    68      \<and> valid x91 x92 x93 x94 x95 x96 x97 x98 x99
    69 
    70      \<and> valid x11 x21 x31 x41 x51 x61 x71 x81 x91
    71      \<and> valid x12 x22 x32 x42 x52 x62 x72 x82 x92
    72      \<and> valid x13 x23 x33 x43 x53 x63 x73 x83 x93
    73      \<and> valid x14 x24 x34 x44 x54 x64 x74 x84 x94
    74      \<and> valid x15 x25 x35 x45 x55 x65 x75 x85 x95
    75      \<and> valid x16 x26 x36 x46 x56 x66 x76 x86 x96
    76      \<and> valid x17 x27 x37 x47 x57 x67 x77 x87 x97
    77      \<and> valid x18 x28 x38 x48 x58 x68 x78 x88 x98
    78      \<and> valid x19 x29 x39 x49 x59 x69 x79 x89 x99
    79 
    80      \<and> valid x11 x12 x13 x21 x22 x23 x31 x32 x33
    81      \<and> valid x14 x15 x16 x24 x25 x26 x34 x35 x36
    82      \<and> valid x17 x18 x19 x27 x28 x29 x37 x38 x39
    83      \<and> valid x41 x42 x43 x51 x52 x53 x61 x62 x63
    84      \<and> valid x44 x45 x46 x54 x55 x56 x64 x65 x66
    85      \<and> valid x47 x48 x49 x57 x58 x59 x67 x68 x69
    86      \<and> valid x71 x72 x73 x81 x82 x83 x91 x92 x93
    87      \<and> valid x74 x75 x76 x84 x85 x86 x94 x95 x96
    88      \<and> valid x77 x78 x79 x87 x88 x89 x97 x98 x99"
    89 
    90 text {*
    91   Just an arbitrary Sudoku grid:
    92 *}
    93 
    94 theorem "\<not> sudoku
    95     x11 x12 x13 x14 x15 x16 x17 x18 x19
    96     x21 x22 x23 x24 x25 x26 x27 x28 x29
    97     x31 x32 x33 x34 x35 x36 x37 x38 x39
    98     x41 x42 x43 x44 x45 x46 x47 x48 x49
    99     x51 x52 x53 x54 x55 x56 x57 x58 x59
   100     x61 x62 x63 x64 x65 x66 x67 x68 x69
   101     x71 x72 x73 x74 x75 x76 x77 x78 x79
   102     x81 x82 x83 x84 x85 x86 x87 x88 x89
   103     x91 x92 x93 x94 x95 x96 x97 x98 x99"
   104   refute
   105 oops
   106 
   107 text {*
   108   An "easy" Sudoku:
   109 *}
   110 
   111 theorem "\<not> sudoku
   112      5   3  x13 x14  7  x16 x17 x18 x19
   113      6  x22 x23  1   9   5  x27 x28 x29
   114     x31  9   8  x34 x35 x36 x37  6  x39
   115      8  x42 x43 x44  6  x46 x47 x48  3 
   116      4  x52 x53  8  x55  3  x57 x58  1 
   117      7  x62 x63 x64  2  x66 x67 x68  6 
   118     x71  6  x73 x74 x75 x76  2   8  x79
   119     x81 x82 x83  4   1   9  x87 x88  5 
   120     x91 x92 x93 x94  8  x96 x97  7   9 "
   121   refute
   122 oops
   123 
   124 text {*
   125   A "hard" Sudoku:
   126 *}
   127 
   128 theorem "\<not> sudoku
   129     x11  2  x13 x14 x15 x16 x17 x18 x19
   130     x21 x22 x23  6  x25 x26 x27 x28  3 
   131     x31  7   4  x34  8  x36 x37 x38 x39
   132     x41 x42 x43 x44 x45  3  x47 x48  2 
   133     x51  8  x53 x54  4  x56 x57  1  x59
   134      6  x62 x63  5  x65 x66 x67 x68 x69
   135     x71 x72 x73 x74  1  x76  7   8  x79
   136      5  x82 x83 x84 x85  9  x87 x88 x89
   137     x91 x92 x93 x94 x95 x96 x97  4  x99"
   138   refute
   139 oops
   140 
   141 text {*
   142   Some "exceptionally difficult" Sudokus, taken from
   143   \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}
   144   (accessed December 2, 2008).
   145 *}
   146 
   147 text {*
   148 \begin{verbatim}
   149 Rating Program: gsf's sudoku q1 (rating) 
   150 Rating: 99408 
   151 Poster: JPF 
   152 Label: Easter Monster 
   153 1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1 
   154 1 . . | . . . | . . 2  
   155 . 9 . | 4 . . | . 5 .  
   156 . . 6 | . . . | 7 . .  
   157 ------+-------+------ 
   158 . 5 . | 9 . 3 | . . .  
   159 . . . | . 7 . | . . .  
   160 . . . | 8 5 . | . 4 .  
   161 ------+-------+------ 
   162 7 . . | . . . | 6 . .  
   163 . 3 . | . . 9 | . 8 .  
   164 . . 2 | . . . | . . 1  
   165 \end{verbatim}
   166 *}
   167 
   168 theorem "\<not> sudoku
   169      1  x12 x13 x14 x15 x16 x17 x18  2 
   170     x21  9  x23  4  x25 x26 x27  5  x29
   171     x31 x32  6  x34 x35 x36  7  x38 x39
   172     x41  5  x43  9  x45  3  x47 x48 x49
   173     x51 x52 x53 x54  7  x56 x57 x58 x59
   174     x61 x62 x63  8   5  x66 x67  4  x69
   175      7  x72 x73 x74 x75 x76  6  x78 x79
   176     x81  3  x83 x84 x85  9  x87  8  x89
   177     x91 x92  2  x94 x95 x96 x97 x98  1 "
   178   refute
   179 oops
   180 
   181 text {*
   182 \begin{verbatim}
   183 Rating Program: gsf's sudoku q1 (Processing time) 
   184 Rating: 4m19s@2 GHz 
   185 Poster: tarek 
   186 Label: tarek071223170000-052 
   187 ..1..4.......6.3.5...9.....8.....7.3.......285...7.6..3...8...6..92......4...1... 
   188 . . 1 | . . 4 | . . .  
   189 . . . | . 6 . | 3 . 5  
   190 . . . | 9 . . | . . .  
   191 ------+-------+------ 
   192 8 . . | . . . | 7 . 3  
   193 . . . | . . . | . 2 8  
   194 5 . . | . 7 . | 6 . .  
   195 ------+-------+------ 
   196 3 . . | . 8 . | . . 6  
   197 . . 9 | 2 . . | . . .  
   198 . 4 . | . . 1 | . . .  
   199 \end{verbatim}
   200 *}
   201 
   202 theorem "\<not> sudoku
   203     x11 x12  1  x14 x15  4  x17 x18 x19
   204     x21 x22 x23 x24  6  x26  3  x28  5 
   205     x31 x32 x33  9  x35 x36 x37 x38 x39
   206      8  x42 x43 x44 x45 x46  7  x48  3 
   207     x51 x52 x53 x54 x55 x56 x57  2   8 
   208      5  x62 x63 x64  7  x66  6  x68 x69
   209      3  x72 x73 x74  8  x76 x77 x78  6 
   210     x81 x82  9   2  x85 x86 x87 x88 x89
   211     x91  4  x93 x94 x95  1  x97 x98 x99"
   212   refute
   213 oops
   214 
   215 text {*
   216 \begin{verbatim}
   217 Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1 
   218 Rating: 11.9 
   219 Poster: tarek 
   220 Label: golden nugget 
   221 .......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7..... 
   222 . . . | . . . | . 3 9  
   223 . . . | . . 1 | . . 5  
   224 . . 3 | . 5 . | 8 . .  
   225 ------+-------+------ 
   226 . . 8 | . 9 . | . . 6  
   227 . 7 . | . . 2 | . . .  
   228 1 . . | 4 . . | . . .  
   229 ------+-------+------ 
   230 . . 9 | . 8 . | . 5 .  
   231 . 2 . | . . . | 6 . .  
   232 4 . . | 7 . . | . . .  
   233 \end{verbatim}
   234 *}
   235 
   236 theorem "\<not> sudoku
   237     x11 x12 x13 x14 x15 x16 x17  3   9 
   238     x21 x22 x23 x24 x25  1  x27 x28  5 
   239     x31 x32  3  x34  5  x36  8  x38 x39
   240     x41 x42  8  x44  9  x46 x47 x48  6 
   241     x51  7  x53 x54 x55  2  x57 x58 x59
   242      1  x62 x63  4  x65 x66 x67 x68 x69
   243     x71 x72  9  x74  8  x76 x77  5  x79
   244     x81  2  x83 x84 x85 x86  6  x88 x89
   245      4  x92 x93  7  x95 x96 x97 x98 x99"
   246   refute
   247 oops
   248 
   249 text {*
   250 \begin{verbatim}
   251 Rating Program: dukuso's suexrat9 
   252 Rating: 4483 
   253 Poster: coloin 
   254 Label: col-02-08-071 
   255 .2.4.37.........32........4.4.2...7.8...5.........1...5.....9...3.9....7..1..86.. 
   256 . 2 . | 4 . 3 | 7 . .  
   257 . . . | . . . | . 3 2  
   258 . . . | . . . | . . 4  
   259 ------+-------+------ 
   260 . 4 . | 2 . . | . 7 .  
   261 8 . . | . 5 . | . . .  
   262 . . . | . . 1 | . . .  
   263 ------+-------+------ 
   264 5 . . | . . . | 9 . .  
   265 . 3 . | 9 . . | . . 7  
   266 . . 1 | . . 8 | 6 . .  
   267 \end{verbatim}
   268 *}
   269 
   270 theorem "\<not> sudoku
   271     x11  2  x13  4  x15  3   7  x18 x19
   272     x21 x22 x23 x24 x25 x26 x27  3   2 
   273     x31 x32 x33 x34 x35 x36 x37 x38  4 
   274     x41  4  x43  2  x45 x46 x47  7  x49
   275      8  x52 x53 x54  5  x56 x57 x58 x59
   276     x61 x62 x63 x64 x65  1  x67 x68 x69
   277      5  x72 x73 x74 x75 x76  9  x78 x79
   278     x81  3  x83  9  x85 x86 x87 x88  7 
   279     x91 x92  1  x94 x95  8   6  x98 x99"
   280   refute
   281 oops
   282 
   283 text {*
   284 \begin{verbatim}
   285 Rating Program: dukuso's suexratt (10000 2 option) 
   286 Rating: 2141 
   287 Poster: tarek 
   288 Label: golden nugget 
   289 .......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7..... 
   290 . . . | . . . | . 3 9  
   291 . . . | . . 1 | . . 5  
   292 . . 3 | . 5 . | 8 . .  
   293 ------+-------+------ 
   294 . . 8 | . 9 . | . . 6  
   295 . 7 . | . . 2 | . . .  
   296 1 . . | 4 . . | . . .  
   297 ------+-------+------ 
   298 . . 9 | . 8 . | . 5 .  
   299 . 2 . | . . . | 6 . .  
   300 4 . . | 7 . . | . . .
   301 \end{verbatim}
   302 *}
   303 
   304 theorem "\<not> sudoku
   305     x11 x12 x13 x14 x15 x16 x17  3   9 
   306     x21 x22 x23 x24 x25  1  x27 x28  5 
   307     x31 x32  3  x34  5  x36  8  x38 x39
   308     x41 x42  8  x44  9  x46 x47 x48  6 
   309     x51  7  x53 x54 x55  2  x57 x58 x59
   310      1  x62 x63  4  x65 x66 x67 x68 x69
   311     x71 x72  9  x74  8  x76 x77  5  x79
   312     x81  2  x83 x84 x85 x86  6  x88 x89
   313      4  x92 x93  7  x95 x96 x97 x98 x99"
   314   refute
   315 oops
   316 
   317 end