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 \ x2) \ (x1 \ x3) \ (x1 \ x4) \ (x1 \ x5) \ (x1 \ x6) \ (x1 \ x7) \ (x1 \ x8) \ (x1 \ x9)  webertj@18408  30  \ (x2 \ x3) \ (x2 \ x4) \ (x2 \ x5) \ (x2 \ x6) \ (x2 \ x7) \ (x2 \ x8) \ (x2 \ x9)  webertj@18408  31  \ (x3 \ x4) \ (x3 \ x5) \ (x3 \ x6) \ (x3 \ x7) \ (x3 \ x8) \ (x3 \ x9)  webertj@18408  32  \ (x4 \ x5) \ (x4 \ x6) \ (x4 \ x7) \ (x4 \ x8) \ (x4 \ x9)  webertj@18408  33  \ (x5 \ x6) \ (x5 \ x7) \ (x5 \ x8) \ (x5 \ x9)  webertj@18408  34  \ (x6 \ x7) \ (x6 \ x8) \ (x6 \ x9)  webertj@18408  35  \ (x7 \ x8) \ (x7 \ x9)  webertj@18408  36  \ (x8 \ 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  \ valid x21 x22 x23 x24 x25 x26 x27 x28 x29  webertj@18408  60  \ valid x31 x32 x33 x34 x35 x36 x37 x38 x39  webertj@18408  61  \ valid x41 x42 x43 x44 x45 x46 x47 x48 x49  webertj@18408  62  \ valid x51 x52 x53 x54 x55 x56 x57 x58 x59  webertj@18408  63  \ valid x61 x62 x63 x64 x65 x66 x67 x68 x69  webertj@18408  64  \ valid x71 x72 x73 x74 x75 x76 x77 x78 x79  webertj@18408  65  \ valid x81 x82 x83 x84 x85 x86 x87 x88 x89  webertj@18408  66  \ valid x91 x92 x93 x94 x95 x96 x97 x98 x99  webertj@18408  67 webertj@18408  68  \ valid x11 x21 x31 x41 x51 x61 x71 x81 x91  webertj@18408  69  \ valid x12 x22 x32 x42 x52 x62 x72 x82 x92  webertj@18408  70  \ valid x13 x23 x33 x43 x53 x63 x73 x83 x93  webertj@18408  71  \ valid x14 x24 x34 x44 x54 x64 x74 x84 x94  webertj@18408  72  \ valid x15 x25 x35 x45 x55 x65 x75 x85 x95  webertj@18408  73  \ valid x16 x26 x36 x46 x56 x66 x76 x86 x96  webertj@18408  74  \ valid x17 x27 x37 x47 x57 x67 x77 x87 x97  webertj@18408  75  \ valid x18 x28 x38 x48 x58 x68 x78 x88 x98  webertj@18408  76  \ valid x19 x29 x39 x49 x59 x69 x79 x89 x99  webertj@18408  77 webertj@18408  78  \ valid x11 x12 x13 x21 x22 x23 x31 x32 x33  webertj@18408  79  \ valid x14 x15 x16 x24 x25 x26 x34 x35 x36  webertj@18408  80  \ valid x17 x18 x19 x27 x28 x29 x37 x38 x39  webertj@18408  81  \ valid x41 x42 x43 x51 x52 x53 x61 x62 x63  webertj@18408  82  \ valid x44 x45 x46 x54 x55 x56 x64 x65 x66  webertj@18408  83  \ valid x47 x48 x49 x57 x58 x59 x67 x68 x69  webertj@18408  84  \ valid x71 x72 x73 x81 x82 x83 x91 x92 x93  webertj@18408  85  \ valid x74 x75 x76 x84 x85 x86 x94 x95 x96  webertj@18408  86  \ 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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 "\ 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