src/HOL/ex/Sudoku.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61933 cf58b5b794b2
child 63680 6e1e8b5abbfa
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Sudoku.thy
     2     Author:     Tjark Weber
     3     Copyright   2005-2014
     4 *)
     5 
     6 section \<open>A SAT-based Sudoku Solver\<close>
     7 
     8 theory Sudoku
     9 imports Main
    10 begin
    11 
    12 text \<open>
    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 \<open>refute\<close> to find Sudoku
    16   solutions.  The \<open>refute\<close> tool has since been superseded by
    17   \<open>nitpick\<close>, which is used below.)
    18 \<close>
    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 \<open>
    87   Just an arbitrary Sudoku grid:
    88 \<close>
    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 \<open>
   104   An ``easy'' Sudoku:
   105 \<close>
   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 \<open>
   121   A ``hard'' Sudoku:
   122 \<close>
   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 \<open>
   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 \<close>
   142 
   143 text \<open>
   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 \<close>
   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 \<open>
   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 \<close>
   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 \<open>
   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 \<close>
   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 \<open>
   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 \<close>
   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 \<open>
   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 \<close>
   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