src/HOL/ex/Sudoku.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 23219 87ad6e8a5f2c
child 28949 610fe33ca358
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (*  Title:      Sudoku.thy
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2005-2007
     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   See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
    18   LPAR'05) for further explanations.
    19 *}
    20 
    21 datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
    22 
    23 constdefs
    24   valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
    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 constdefs
    37   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"
    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 end