src/HOL/ex/Sudoku.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 41589 bbd861837ebc child 54703 499f92dc6e45 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
     1 (*  Title:      HOL/ex/Sudoku.thy

     2     Author:     Tjark Weber

     3     Copyright   2005-2008

     4 *)

     5

     6 header {* A SAT-based Sudoku Solver *}

     7

     8 theory Sudoku

     9 imports Main

    10 begin

    11

    12 text {*

    13   Please make sure you are using an efficient SAT solver (e.g., zChaff)

    14   when loading this theory.  See Isabelle's settings file for details.

    15

    16   Using zChaff, each Sudoku in this theory is solved in less than a

    17   second.

    18

    19   See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at

    20   LPAR'05) for further explanations.

    21 *}

    22

    23 datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")

    24

    25 definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where

    26

    27   "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==

    28     (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)

    29     \<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)

    30     \<and> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9)

    31     \<and> (x4 \<noteq> x5) \<and> (x4 \<noteq> x6) \<and> (x4 \<noteq> x7) \<and> (x4 \<noteq> x8) \<and> (x4 \<noteq> x9)

    32     \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9)

    33     \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9)

    34     \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9)

    35     \<and> (x8 \<noteq> x9)"

    36

    37 definition sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    38     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    39     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    40     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    41     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    42     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    43     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    44     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    45     digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where

    46

    47   "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19

    48           x21 x22 x23 x24 x25 x26 x27 x28 x29

    49           x31 x32 x33 x34 x35 x36 x37 x38 x39

    50           x41 x42 x43 x44 x45 x46 x47 x48 x49

    51           x51 x52 x53 x54 x55 x56 x57 x58 x59

    52           x61 x62 x63 x64 x65 x66 x67 x68 x69

    53           x71 x72 x73 x74 x75 x76 x77 x78 x79

    54           x81 x82 x83 x84 x85 x86 x87 x88 x89

    55           x91 x92 x93 x94 x95 x96 x97 x98 x99 ==

    56

    57        valid x11 x12 x13 x14 x15 x16 x17 x18 x19

    58      \<and> valid x21 x22 x23 x24 x25 x26 x27 x28 x29

    59      \<and> valid x31 x32 x33 x34 x35 x36 x37 x38 x39

    60      \<and> valid x41 x42 x43 x44 x45 x46 x47 x48 x49

    61      \<and> valid x51 x52 x53 x54 x55 x56 x57 x58 x59

    62      \<and> valid x61 x62 x63 x64 x65 x66 x67 x68 x69

    63      \<and> valid x71 x72 x73 x74 x75 x76 x77 x78 x79

    64      \<and> valid x81 x82 x83 x84 x85 x86 x87 x88 x89

    65      \<and> valid x91 x92 x93 x94 x95 x96 x97 x98 x99

    66

    67      \<and> valid x11 x21 x31 x41 x51 x61 x71 x81 x91

    68      \<and> valid x12 x22 x32 x42 x52 x62 x72 x82 x92

    69      \<and> valid x13 x23 x33 x43 x53 x63 x73 x83 x93

    70      \<and> valid x14 x24 x34 x44 x54 x64 x74 x84 x94

    71      \<and> valid x15 x25 x35 x45 x55 x65 x75 x85 x95

    72      \<and> valid x16 x26 x36 x46 x56 x66 x76 x86 x96

    73      \<and> valid x17 x27 x37 x47 x57 x67 x77 x87 x97

    74      \<and> valid x18 x28 x38 x48 x58 x68 x78 x88 x98

    75      \<and> valid x19 x29 x39 x49 x59 x69 x79 x89 x99

    76

    77      \<and> valid x11 x12 x13 x21 x22 x23 x31 x32 x33

    78      \<and> valid x14 x15 x16 x24 x25 x26 x34 x35 x36

    79      \<and> valid x17 x18 x19 x27 x28 x29 x37 x38 x39

    80      \<and> valid x41 x42 x43 x51 x52 x53 x61 x62 x63

    81      \<and> valid x44 x45 x46 x54 x55 x56 x64 x65 x66

    82      \<and> valid x47 x48 x49 x57 x58 x59 x67 x68 x69

    83      \<and> valid x71 x72 x73 x81 x82 x83 x91 x92 x93

    84      \<and> valid x74 x75 x76 x84 x85 x86 x94 x95 x96

    85      \<and> valid x77 x78 x79 x87 x88 x89 x97 x98 x99"

    86

    87 text {*

    88   Just an arbitrary Sudoku grid:

    89 *}

    90

    91 theorem "\<not> sudoku

    92     x11 x12 x13 x14 x15 x16 x17 x18 x19

    93     x21 x22 x23 x24 x25 x26 x27 x28 x29

    94     x31 x32 x33 x34 x35 x36 x37 x38 x39

    95     x41 x42 x43 x44 x45 x46 x47 x48 x49

    96     x51 x52 x53 x54 x55 x56 x57 x58 x59

    97     x61 x62 x63 x64 x65 x66 x67 x68 x69

    98     x71 x72 x73 x74 x75 x76 x77 x78 x79

    99     x81 x82 x83 x84 x85 x86 x87 x88 x89

   100     x91 x92 x93 x94 x95 x96 x97 x98 x99"

   101   refute

   102 oops

   103

   104 text {*

   105   An "easy" Sudoku:

   106 *}

   107

   108 theorem "\<not> sudoku

   109      5   3  x13 x14  7  x16 x17 x18 x19

   110      6  x22 x23  1   9   5  x27 x28 x29

   111     x31  9   8  x34 x35 x36 x37  6  x39

   112      8  x42 x43 x44  6  x46 x47 x48  3

   113      4  x52 x53  8  x55  3  x57 x58  1

   114      7  x62 x63 x64  2  x66 x67 x68  6

   115     x71  6  x73 x74 x75 x76  2   8  x79

   116     x81 x82 x83  4   1   9  x87 x88  5

   117     x91 x92 x93 x94  8  x96 x97  7   9 "

   118   refute

   119 oops

   120

   121 text {*

   122   A "hard" Sudoku:

   123 *}

   124

   125 theorem "\<not> sudoku

   126     x11  2  x13 x14 x15 x16 x17 x18 x19

   127     x21 x22 x23  6  x25 x26 x27 x28  3

   128     x31  7   4  x34  8  x36 x37 x38 x39

   129     x41 x42 x43 x44 x45  3  x47 x48  2

   130     x51  8  x53 x54  4  x56 x57  1  x59

   131      6  x62 x63  5  x65 x66 x67 x68 x69

   132     x71 x72 x73 x74  1  x76  7   8  x79

   133      5  x82 x83 x84 x85  9  x87 x88 x89

   134     x91 x92 x93 x94 x95 x96 x97  4  x99"

   135   refute

   136 oops

   137

   138 text {*

   139   Some "exceptionally difficult" Sudokus, taken from

   140   \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}

   141   (accessed December 2, 2008).

   142 *}

   143

   144 text {*

   145 \begin{verbatim}

   146 Rating Program: gsf's sudoku q1 (rating)

   147 Rating: 99408

   148 Poster: JPF

   149 Label: Easter Monster

   150 1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1

   151 1 . . | . . . | . . 2

   152 . 9 . | 4 . . | . 5 .

   153 . . 6 | . . . | 7 . .

   154 ------+-------+------

   155 . 5 . | 9 . 3 | . . .

   156 . . . | . 7 . | . . .

   157 . . . | 8 5 . | . 4 .

   158 ------+-------+------

   159 7 . . | . . . | 6 . .

   160 . 3 . | . . 9 | . 8 .

   161 . . 2 | . . . | . . 1

   162 \end{verbatim}

   163 *}

   164

   165 theorem "\<not> sudoku

   166      1  x12 x13 x14 x15 x16 x17 x18  2

   167     x21  9  x23  4  x25 x26 x27  5  x29

   168     x31 x32  6  x34 x35 x36  7  x38 x39

   169     x41  5  x43  9  x45  3  x47 x48 x49

   170     x51 x52 x53 x54  7  x56 x57 x58 x59

   171     x61 x62 x63  8   5  x66 x67  4  x69

   172      7  x72 x73 x74 x75 x76  6  x78 x79

   173     x81  3  x83 x84 x85  9  x87  8  x89

   174     x91 x92  2  x94 x95 x96 x97 x98  1 "

   175   refute

   176 oops

   177

   178 text {*

   179 \begin{verbatim}

   180 Rating Program: gsf's sudoku q1 (Processing time)

   181 Rating: 4m19s@2 GHz

   182 Poster: tarek

   183 Label: tarek071223170000-052

   184 ..1..4.......6.3.5...9.....8.....7.3.......285...7.6..3...8...6..92......4...1...

   185 . . 1 | . . 4 | . . .

   186 . . . | . 6 . | 3 . 5

   187 . . . | 9 . . | . . .

   188 ------+-------+------

   189 8 . . | . . . | 7 . 3

   190 . . . | . . . | . 2 8

   191 5 . . | . 7 . | 6 . .

   192 ------+-------+------

   193 3 . . | . 8 . | . . 6

   194 . . 9 | 2 . . | . . .

   195 . 4 . | . . 1 | . . .

   196 \end{verbatim}

   197 *}

   198

   199 theorem "\<not> sudoku

   200     x11 x12  1  x14 x15  4  x17 x18 x19

   201     x21 x22 x23 x24  6  x26  3  x28  5

   202     x31 x32 x33  9  x35 x36 x37 x38 x39

   203      8  x42 x43 x44 x45 x46  7  x48  3

   204     x51 x52 x53 x54 x55 x56 x57  2   8

   205      5  x62 x63 x64  7  x66  6  x68 x69

   206      3  x72 x73 x74  8  x76 x77 x78  6

   207     x81 x82  9   2  x85 x86 x87 x88 x89

   208     x91  4  x93 x94 x95  1  x97 x98 x99"

   209   refute

   210 oops

   211

   212 text {*

   213 \begin{verbatim}

   214 Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1

   215 Rating: 11.9

   216 Poster: tarek

   217 Label: golden nugget

   218 .......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....

   219 . . . | . . . | . 3 9

   220 . . . | . . 1 | . . 5

   221 . . 3 | . 5 . | 8 . .

   222 ------+-------+------

   223 . . 8 | . 9 . | . . 6

   224 . 7 . | . . 2 | . . .

   225 1 . . | 4 . . | . . .

   226 ------+-------+------

   227 . . 9 | . 8 . | . 5 .

   228 . 2 . | . . . | 6 . .

   229 4 . . | 7 . . | . . .

   230 \end{verbatim}

   231 *}

   232

   233 theorem "\<not> sudoku

   234     x11 x12 x13 x14 x15 x16 x17  3   9

   235     x21 x22 x23 x24 x25  1  x27 x28  5

   236     x31 x32  3  x34  5  x36  8  x38 x39

   237     x41 x42  8  x44  9  x46 x47 x48  6

   238     x51  7  x53 x54 x55  2  x57 x58 x59

   239      1  x62 x63  4  x65 x66 x67 x68 x69

   240     x71 x72  9  x74  8  x76 x77  5  x79

   241     x81  2  x83 x84 x85 x86  6  x88 x89

   242      4  x92 x93  7  x95 x96 x97 x98 x99"

   243   refute

   244 oops

   245

   246 text {*

   247 \begin{verbatim}

   248 Rating Program: dukuso's suexrat9

   249 Rating: 4483

   250 Poster: coloin

   251 Label: col-02-08-071

   252 .2.4.37.........32........4.4.2...7.8...5.........1...5.....9...3.9....7..1..86..

   253 . 2 . | 4 . 3 | 7 . .

   254 . . . | . . . | . 3 2

   255 . . . | . . . | . . 4

   256 ------+-------+------

   257 . 4 . | 2 . . | . 7 .

   258 8 . . | . 5 . | . . .

   259 . . . | . . 1 | . . .

   260 ------+-------+------

   261 5 . . | . . . | 9 . .

   262 . 3 . | 9 . . | . . 7

   263 . . 1 | . . 8 | 6 . .

   264 \end{verbatim}

   265 *}

   266

   267 theorem "\<not> sudoku

   268     x11  2  x13  4  x15  3   7  x18 x19

   269     x21 x22 x23 x24 x25 x26 x27  3   2

   270     x31 x32 x33 x34 x35 x36 x37 x38  4

   271     x41  4  x43  2  x45 x46 x47  7  x49

   272      8  x52 x53 x54  5  x56 x57 x58 x59

   273     x61 x62 x63 x64 x65  1  x67 x68 x69

   274      5  x72 x73 x74 x75 x76  9  x78 x79

   275     x81  3  x83  9  x85 x86 x87 x88  7

   276     x91 x92  1  x94 x95  8   6  x98 x99"

   277   refute

   278 oops

   279

   280 text {*

   281 \begin{verbatim}

   282 Rating Program: dukuso's suexratt (10000 2 option)

   283 Rating: 2141

   284 Poster: tarek

   285 Label: golden nugget

   286 .......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....

   287 . . . | . . . | . 3 9

   288 . . . | . . 1 | . . 5

   289 . . 3 | . 5 . | 8 . .

   290 ------+-------+------

   291 . . 8 | . 9 . | . . 6

   292 . 7 . | . . 2 | . . .

   293 1 . . | 4 . . | . . .

   294 ------+-------+------

   295 . . 9 | . 8 . | . 5 .

   296 . 2 . | . . . | 6 . .

   297 4 . . | 7 . . | . . .

   298 \end{verbatim}

   299 *}

   300

   301 theorem "\<not> sudoku

   302     x11 x12 x13 x14 x15 x16 x17  3   9

   303     x21 x22 x23 x24 x25  1  x27 x28  5

   304     x31 x32  3  x34  5  x36  8  x38 x39

   305     x41 x42  8  x44  9  x46 x47 x48  6

   306     x51  7  x53 x54 x55  2  x57 x58 x59

   307      1  x62 x63  4  x65 x66 x67 x68 x69

   308     x71 x72  9  x74  8  x76 x77  5  x79

   309     x81  2  x83 x84 x85 x86  6  x88 x89

   310      4  x92 x93  7  x95 x96 x97 x98 x99"

   311   refute

   312 oops

   313

   314 end