src/HOL/ex/Sudoku.thy
 author blanchet Thu Sep 11 19:32:36 2014 +0200 (2014-09-11) changeset 58310 91ea607a34d8 parent 58183 285fbec02fb0 child 58889 5b7a9633cfa8 permissions -rw-r--r--
updated news
 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@58310  22 datatype 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