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--
     1 (*  Title:      Sudoku.thy

     2     ID:         $Id$

     3     Author:     Tjark Weber

     4     Copyright   2005-2008

     5 *)

     6

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

     8

     9 theory Sudoku

    10 imports Main

    11 begin

    12

    13 text {*

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

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

    16

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

    18   second.

    19

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

    21   LPAR'05) for further explanations.

    22 *}

    23

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

    25

    26 constdefs

    27   valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"

    28

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

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

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

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

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

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

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

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

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

    38

    39 constdefs

    40   sudoku :: "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 =>

    46     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    47     digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    48     digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"

    49

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

    51           x21 x22 x23 x24 x25 x26 x27 x28 x29

    52           x31 x32 x33 x34 x35 x36 x37 x38 x39

    53           x41 x42 x43 x44 x45 x46 x47 x48 x49

    54           x51 x52 x53 x54 x55 x56 x57 x58 x59

    55           x61 x62 x63 x64 x65 x66 x67 x68 x69

    56           x71 x72 x73 x74 x75 x76 x77 x78 x79

    57           x81 x82 x83 x84 x85 x86 x87 x88 x89

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

    59

    60        valid x11 x12 x13 x14 x15 x16 x17 x18 x19

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

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

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

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

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

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

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

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

    69

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

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

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

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

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

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

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

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

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

    79

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

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

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

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

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

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

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

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

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

    89

    90 text {*

    91   Just an arbitrary Sudoku grid:

    92 *}

    93

    94 theorem "\<not> sudoku

    95     x11 x12 x13 x14 x15 x16 x17 x18 x19

    96     x21 x22 x23 x24 x25 x26 x27 x28 x29

    97     x31 x32 x33 x34 x35 x36 x37 x38 x39

    98     x41 x42 x43 x44 x45 x46 x47 x48 x49

    99     x51 x52 x53 x54 x55 x56 x57 x58 x59

   100     x61 x62 x63 x64 x65 x66 x67 x68 x69

   101     x71 x72 x73 x74 x75 x76 x77 x78 x79

   102     x81 x82 x83 x84 x85 x86 x87 x88 x89

   103     x91 x92 x93 x94 x95 x96 x97 x98 x99"

   104   refute

   105 oops

   106

   107 text {*

   108   An "easy" Sudoku:

   109 *}

   110

   111 theorem "\<not> sudoku

   112      5   3  x13 x14  7  x16 x17 x18 x19

   113      6  x22 x23  1   9   5  x27 x28 x29

   114     x31  9   8  x34 x35 x36 x37  6  x39

   115      8  x42 x43 x44  6  x46 x47 x48  3

   116      4  x52 x53  8  x55  3  x57 x58  1

   117      7  x62 x63 x64  2  x66 x67 x68  6

   118     x71  6  x73 x74 x75 x76  2   8  x79

   119     x81 x82 x83  4   1   9  x87 x88  5

   120     x91 x92 x93 x94  8  x96 x97  7   9 "

   121   refute

   122 oops

   123

   124 text {*

   125   A "hard" Sudoku:

   126 *}

   127

   128 theorem "\<not> sudoku

   129     x11  2  x13 x14 x15 x16 x17 x18 x19

   130     x21 x22 x23  6  x25 x26 x27 x28  3

   131     x31  7   4  x34  8  x36 x37 x38 x39

   132     x41 x42 x43 x44 x45  3  x47 x48  2

   133     x51  8  x53 x54  4  x56 x57  1  x59

   134      6  x62 x63  5  x65 x66 x67 x68 x69

   135     x71 x72 x73 x74  1  x76  7   8  x79

   136      5  x82 x83 x84 x85  9  x87 x88 x89

   137     x91 x92 x93 x94 x95 x96 x97  4  x99"

   138   refute

   139 oops

   140

   141 text {*

   142   Some "exceptionally difficult" Sudokus, taken from

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

   144   (accessed December 2, 2008).

   145 *}

   146

   147 text {*

   148 \begin{verbatim}

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

   150 Rating: 99408

   151 Poster: JPF

   152 Label: Easter Monster

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

   154 1 . . | . . . | . . 2

   155 . 9 . | 4 . . | . 5 .

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

   157 ------+-------+------

   158 . 5 . | 9 . 3 | . . .

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

   160 . . . | 8 5 . | . 4 .

   161 ------+-------+------

   162 7 . . | . . . | 6 . .

   163 . 3 . | . . 9 | . 8 .

   164 . . 2 | . . . | . . 1

   165 \end{verbatim}

   166 *}

   167

   168 theorem "\<not> sudoku

   169      1  x12 x13 x14 x15 x16 x17 x18  2

   170     x21  9  x23  4  x25 x26 x27  5  x29

   171     x31 x32  6  x34 x35 x36  7  x38 x39

   172     x41  5  x43  9  x45  3  x47 x48 x49

   173     x51 x52 x53 x54  7  x56 x57 x58 x59

   174     x61 x62 x63  8   5  x66 x67  4  x69

   175      7  x72 x73 x74 x75 x76  6  x78 x79

   176     x81  3  x83 x84 x85  9  x87  8  x89

   177     x91 x92  2  x94 x95 x96 x97 x98  1 "

   178   refute

   179 oops

   180

   181 text {*

   182 \begin{verbatim}

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

   184 Rating: 4m19s@2 GHz

   185 Poster: tarek

   186 Label: tarek071223170000-052

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

   188 . . 1 | . . 4 | . . .

   189 . . . | . 6 . | 3 . 5

   190 . . . | 9 . . | . . .

   191 ------+-------+------

   192 8 . . | . . . | 7 . 3

   193 . . . | . . . | . 2 8

   194 5 . . | . 7 . | 6 . .

   195 ------+-------+------

   196 3 . . | . 8 . | . . 6

   197 . . 9 | 2 . . | . . .

   198 . 4 . | . . 1 | . . .

   199 \end{verbatim}

   200 *}

   201

   202 theorem "\<not> sudoku

   203     x11 x12  1  x14 x15  4  x17 x18 x19

   204     x21 x22 x23 x24  6  x26  3  x28  5

   205     x31 x32 x33  9  x35 x36 x37 x38 x39

   206      8  x42 x43 x44 x45 x46  7  x48  3

   207     x51 x52 x53 x54 x55 x56 x57  2   8

   208      5  x62 x63 x64  7  x66  6  x68 x69

   209      3  x72 x73 x74  8  x76 x77 x78  6

   210     x81 x82  9   2  x85 x86 x87 x88 x89

   211     x91  4  x93 x94 x95  1  x97 x98 x99"

   212   refute

   213 oops

   214

   215 text {*

   216 \begin{verbatim}

   217 Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1

   218 Rating: 11.9

   219 Poster: tarek

   220 Label: golden nugget

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

   222 . . . | . . . | . 3 9

   223 . . . | . . 1 | . . 5

   224 . . 3 | . 5 . | 8 . .

   225 ------+-------+------

   226 . . 8 | . 9 . | . . 6

   227 . 7 . | . . 2 | . . .

   228 1 . . | 4 . . | . . .

   229 ------+-------+------

   230 . . 9 | . 8 . | . 5 .

   231 . 2 . | . . . | 6 . .

   232 4 . . | 7 . . | . . .

   233 \end{verbatim}

   234 *}

   235

   236 theorem "\<not> sudoku

   237     x11 x12 x13 x14 x15 x16 x17  3   9

   238     x21 x22 x23 x24 x25  1  x27 x28  5

   239     x31 x32  3  x34  5  x36  8  x38 x39

   240     x41 x42  8  x44  9  x46 x47 x48  6

   241     x51  7  x53 x54 x55  2  x57 x58 x59

   242      1  x62 x63  4  x65 x66 x67 x68 x69

   243     x71 x72  9  x74  8  x76 x77  5  x79

   244     x81  2  x83 x84 x85 x86  6  x88 x89

   245      4  x92 x93  7  x95 x96 x97 x98 x99"

   246   refute

   247 oops

   248

   249 text {*

   250 \begin{verbatim}

   251 Rating Program: dukuso's suexrat9

   252 Rating: 4483

   253 Poster: coloin

   254 Label: col-02-08-071

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

   256 . 2 . | 4 . 3 | 7 . .

   257 . . . | . . . | . 3 2

   258 . . . | . . . | . . 4

   259 ------+-------+------

   260 . 4 . | 2 . . | . 7 .

   261 8 . . | . 5 . | . . .

   262 . . . | . . 1 | . . .

   263 ------+-------+------

   264 5 . . | . . . | 9 . .

   265 . 3 . | 9 . . | . . 7

   266 . . 1 | . . 8 | 6 . .

   267 \end{verbatim}

   268 *}

   269

   270 theorem "\<not> sudoku

   271     x11  2  x13  4  x15  3   7  x18 x19

   272     x21 x22 x23 x24 x25 x26 x27  3   2

   273     x31 x32 x33 x34 x35 x36 x37 x38  4

   274     x41  4  x43  2  x45 x46 x47  7  x49

   275      8  x52 x53 x54  5  x56 x57 x58 x59

   276     x61 x62 x63 x64 x65  1  x67 x68 x69

   277      5  x72 x73 x74 x75 x76  9  x78 x79

   278     x81  3  x83  9  x85 x86 x87 x88  7

   279     x91 x92  1  x94 x95  8   6  x98 x99"

   280   refute

   281 oops

   282

   283 text {*

   284 \begin{verbatim}

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

   286 Rating: 2141

   287 Poster: tarek

   288 Label: golden nugget

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

   290 . . . | . . . | . 3 9

   291 . . . | . . 1 | . . 5

   292 . . 3 | . 5 . | 8 . .

   293 ------+-------+------

   294 . . 8 | . 9 . | . . 6

   295 . 7 . | . . 2 | . . .

   296 1 . . | 4 . . | . . .

   297 ------+-------+------

   298 . . 9 | . 8 . | . 5 .

   299 . 2 . | . . . | 6 . .

   300 4 . . | 7 . . | . . .

   301 \end{verbatim}

   302 *}

   303

   304 theorem "\<not> sudoku

   305     x11 x12 x13 x14 x15 x16 x17  3   9

   306     x21 x22 x23 x24 x25  1  x27 x28  5

   307     x31 x32  3  x34  5  x36  8  x38 x39

   308     x41 x42  8  x44  9  x46 x47 x48  6

   309     x51  7  x53 x54 x55  2  x57 x58 x59

   310      1  x62 x63  4  x65 x66 x67 x68 x69

   311     x71 x72  9  x74  8  x76 x77  5  x79

   312     x81  2  x83 x84 x85 x86  6  x88 x89

   313      4  x92 x93  7  x95 x96 x97 x98 x99"

   314   refute

   315 oops

   316

   317 end