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