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