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