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