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