src/HOL/ex/Sudoku.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 58889 5b7a9633cfa8 child 61343 5b5656a63bd6 permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/ex/Sudoku.thy

     2     Author:     Tjark Weber

     3     Copyright   2005-2014

     4 *)

     5

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

     7

     8 theory Sudoku

     9 imports Main

    10 begin

    11

    12 text {*

    13   See the paper A SAT-based Sudoku Solver'' (Tjark Weber, published at

    14   LPAR'05) for further explanations.  (The paper describes an older version of

    15   this theory that used the model finder @{text refute} to find Sudoku

    16   solutions.  The @{text refute} tool has since been superseded by

    17   @{text nitpick}, which is used below.)

    18 *}

    19

    20 no_notation Groups.one_class.one ("1")

    21

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

    23

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

    25

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

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

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

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

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

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

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

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

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

    35

    36 definition sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>

    37     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 => bool" where

    45

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

    47           x21 x22 x23 x24 x25 x26 x27 x28 x29

    48           x31 x32 x33 x34 x35 x36 x37 x38 x39

    49           x41 x42 x43 x44 x45 x46 x47 x48 x49

    50           x51 x52 x53 x54 x55 x56 x57 x58 x59

    51           x61 x62 x63 x64 x65 x66 x67 x68 x69

    52           x71 x72 x73 x74 x75 x76 x77 x78 x79

    53           x81 x82 x83 x84 x85 x86 x87 x88 x89

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

    55

    56        valid x11 x12 x13 x14 x15 x16 x17 x18 x19

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

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

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

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

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

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

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

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

    65

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

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

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

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

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

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

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

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

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

    75

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

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

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

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

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

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

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

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

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

    85

    86 text {*

    87   Just an arbitrary Sudoku grid:

    88 *}

    89

    90 theorem "\<not> sudoku

    91     x11 x12 x13 x14 x15 x16 x17 x18 x19

    92     x21 x22 x23 x24 x25 x26 x27 x28 x29

    93     x31 x32 x33 x34 x35 x36 x37 x38 x39

    94     x41 x42 x43 x44 x45 x46 x47 x48 x49

    95     x51 x52 x53 x54 x55 x56 x57 x58 x59

    96     x61 x62 x63 x64 x65 x66 x67 x68 x69

    97     x71 x72 x73 x74 x75 x76 x77 x78 x79

    98     x81 x82 x83 x84 x85 x86 x87 x88 x89

    99     x91 x92 x93 x94 x95 x96 x97 x98 x99"

   100   nitpick [expect=genuine]

   101 oops

   102

   103 text {*

   104   An easy'' Sudoku:

   105 *}

   106

   107 theorem "\<not> sudoku

   108      5   3  x13 x14  7  x16 x17 x18 x19

   109      6  x22 x23  1   9   5  x27 x28 x29

   110     x31  9   8  x34 x35 x36 x37  6  x39

   111      8  x42 x43 x44  6  x46 x47 x48  3

   112      4  x52 x53  8  x55  3  x57 x58  1

   113      7  x62 x63 x64  2  x66 x67 x68  6

   114     x71  6  x73 x74 x75 x76  2   8  x79

   115     x81 x82 x83  4   1   9  x87 x88  5

   116     x91 x92 x93 x94  8  x96 x97  7   9 "

   117   nitpick [expect=genuine]

   118 oops

   119

   120 text {*

   121   A hard'' Sudoku:

   122 *}

   123

   124 theorem "\<not> sudoku

   125     x11  2  x13 x14 x15 x16 x17 x18 x19

   126     x21 x22 x23  6  x25 x26 x27 x28  3

   127     x31  7   4  x34  8  x36 x37 x38 x39

   128     x41 x42 x43 x44 x45  3  x47 x48  2

   129     x51  8  x53 x54  4  x56 x57  1  x59

   130      6  x62 x63  5  x65 x66 x67 x68 x69

   131     x71 x72 x73 x74  1  x76  7   8  x79

   132      5  x82 x83 x84 x85  9  x87 x88 x89

   133     x91 x92 x93 x94 x95 x96 x97  4  x99"

   134   nitpick [expect=genuine]

   135 oops

   136

   137 text {*

   138   Some exceptionally difficult'' Sudokus, taken from

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

   140   (accessed December~2, 2008).

   141 *}

   142

   143 text {*

   144 \begin{verbatim}

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

   146 Rating: 99408

   147 Poster: JPF

   148 Label: Easter Monster

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

   150 1 . . | . . . | . . 2

   151 . 9 . | 4 . . | . 5 .

   152 . . 6 | . . . | 7 . .

   153 ------+-------+------

   154 . 5 . | 9 . 3 | . . .

   155 . . . | . 7 . | . . .

   156 . . . | 8 5 . | . 4 .

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

   158 7 . . | . . . | 6 . .

   159 . 3 . | . . 9 | . 8 .

   160 . . 2 | . . . | . . 1

   161 \end{verbatim}

   162 *}

   163

   164 theorem "\<not> sudoku

   165      1  x12 x13 x14 x15 x16 x17 x18  2

   166     x21  9  x23  4  x25 x26 x27  5  x29

   167     x31 x32  6  x34 x35 x36  7  x38 x39

   168     x41  5  x43  9  x45  3  x47 x48 x49

   169     x51 x52 x53 x54  7  x56 x57 x58 x59

   170     x61 x62 x63  8   5  x66 x67  4  x69

   171      7  x72 x73 x74 x75 x76  6  x78 x79

   172     x81  3  x83 x84 x85  9  x87  8  x89

   173     x91 x92  2  x94 x95 x96 x97 x98  1 "

   174   nitpick [expect=genuine]

   175 oops

   176

   177 text {*

   178 \begin{verbatim}

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

   180 Rating: 4m19s@2 GHz

   181 Poster: tarek

   182 Label: tarek071223170000-052

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

   184 . . 1 | . . 4 | . . .

   185 . . . | . 6 . | 3 . 5

   186 . . . | 9 . . | . . .

   187 ------+-------+------

   188 8 . . | . . . | 7 . 3

   189 . . . | . . . | . 2 8

   190 5 . . | . 7 . | 6 . .

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

   192 3 . . | . 8 . | . . 6

   193 . . 9 | 2 . . | . . .

   194 . 4 . | . . 1 | . . .

   195 \end{verbatim}

   196 *}

   197

   198 theorem "\<not> sudoku

   199     x11 x12  1  x14 x15  4  x17 x18 x19

   200     x21 x22 x23 x24  6  x26  3  x28  5

   201     x31 x32 x33  9  x35 x36 x37 x38 x39

   202      8  x42 x43 x44 x45 x46  7  x48  3

   203     x51 x52 x53 x54 x55 x56 x57  2   8

   204      5  x62 x63 x64  7  x66  6  x68 x69

   205      3  x72 x73 x74  8  x76 x77 x78  6

   206     x81 x82  9   2  x85 x86 x87 x88 x89

   207     x91  4  x93 x94 x95  1  x97 x98 x99"

   208   nitpick [expect=genuine]

   209 oops

   210

   211 text {*

   212 \begin{verbatim}

   213 Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1

   214 Rating: 11.9

   215 Poster: tarek

   216 Label: golden nugget

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

   218 . . . | . . . | . 3 9

   219 . . . | . . 1 | . . 5

   220 . . 3 | . 5 . | 8 . .

   221 ------+-------+------

   222 . . 8 | . 9 . | . . 6

   223 . 7 . | . . 2 | . . .

   224 1 . . | 4 . . | . . .

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

   226 . . 9 | . 8 . | . 5 .

   227 . 2 . | . . . | 6 . .

   228 4 . . | 7 . . | . . .

   229 \end{verbatim}

   230 *}

   231

   232 theorem "\<not> sudoku

   233     x11 x12 x13 x14 x15 x16 x17  3   9

   234     x21 x22 x23 x24 x25  1  x27 x28  5

   235     x31 x32  3  x34  5  x36  8  x38 x39

   236     x41 x42  8  x44  9  x46 x47 x48  6

   237     x51  7  x53 x54 x55  2  x57 x58 x59

   238      1  x62 x63  4  x65 x66 x67 x68 x69

   239     x71 x72  9  x74  8  x76 x77  5  x79

   240     x81  2  x83 x84 x85 x86  6  x88 x89

   241      4  x92 x93  7  x95 x96 x97 x98 x99"

   242   nitpick [expect=genuine]

   243 oops

   244

   245 text {*

   246 \begin{verbatim}

   247 Rating Program: dukuso's suexrat9

   248 Rating: 4483

   249 Poster: coloin

   250 Label: col-02-08-071

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

   252 . 2 . | 4 . 3 | 7 . .

   253 . . . | . . . | . 3 2

   254 . . . | . . . | . . 4

   255 ------+-------+------

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

   257 8 . . | . 5 . | . . .

   258 . . . | . . 1 | . . .

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

   260 5 . . | . . . | 9 . .

   261 . 3 . | 9 . . | . . 7

   262 . . 1 | . . 8 | 6 . .

   263 \end{verbatim}

   264 *}

   265

   266 theorem "\<not> sudoku

   267     x11  2  x13  4  x15  3   7  x18 x19

   268     x21 x22 x23 x24 x25 x26 x27  3   2

   269     x31 x32 x33 x34 x35 x36 x37 x38  4

   270     x41  4  x43  2  x45 x46 x47  7  x49

   271      8  x52 x53 x54  5  x56 x57 x58 x59

   272     x61 x62 x63 x64 x65  1  x67 x68 x69

   273      5  x72 x73 x74 x75 x76  9  x78 x79

   274     x81  3  x83  9  x85 x86 x87 x88  7

   275     x91 x92  1  x94 x95  8   6  x98 x99"

   276   nitpick [expect=genuine]

   277 oops

   278

   279 text {*

   280 \begin{verbatim}

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

   282 Rating: 2141

   283 Poster: tarek

   284 Label: golden nugget

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

   286 . . . | . . . | . 3 9

   287 . . . | . . 1 | . . 5

   288 . . 3 | . 5 . | 8 . .

   289 ------+-------+------

   290 . . 8 | . 9 . | . . 6

   291 . 7 . | . . 2 | . . .

   292 1 . . | 4 . . | . . .

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

   294 . . 9 | . 8 . | . 5 .

   295 . 2 . | . . . | 6 . .

   296 4 . . | 7 . . | . . .

   297 \end{verbatim}

   298 *}

   299

   300 theorem "\<not> sudoku

   301     x11 x12 x13 x14 x15 x16 x17  3   9

   302     x21 x22 x23 x24 x25  1  x27 x28  5

   303     x31 x32  3  x34  5  x36  8  x38 x39

   304     x41 x42  8  x44  9  x46 x47 x48  6

   305     x51  7  x53 x54 x55  2  x57 x58 x59

   306      1  x62 x63  4  x65 x66 x67 x68 x69

   307     x71 x72  9  x74  8  x76 x77  5  x79

   308     x81  2  x83 x84 x85 x86  6  x88 x89

   309      4  x92 x93  7  x95 x96 x97 x98 x99"

   310   nitpick [expect=genuine]

   311 oops

   312

   313 end