src/HOL/ex/Sudoku.thy
author webertj
Wed Dec 14 22:05:22 2005 +0100 (2005-12-14)
changeset 18408 07da804d1119
child 22053 4b713f89f8c7
permissions -rw-r--r--
ex/Sudoku.thy
webertj@18408
     1
(*  Title:      Sudoku.thy
webertj@18408
     2
    ID:         $Id$
webertj@18408
     3
    Author:     Tjark Weber
webertj@18408
     4
    Copyright   2005
webertj@18408
     5
*)
webertj@18408
     6
webertj@18408
     7
header {* A SAT-based Sudoku Solver *}
webertj@18408
     8
webertj@18408
     9
theory Sudoku
webertj@18408
    10
webertj@18408
    11
imports Main
webertj@18408
    12
webertj@18408
    13
begin
webertj@18408
    14
webertj@18408
    15
text {*
webertj@18408
    16
  Please make sure you are using an efficient SAT solver (e.g. zChaff)
webertj@18408
    17
  when loading this theory.  See Isabelle's settings file for details.
webertj@18408
    18
webertj@18408
    19
  See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
webertj@18408
    20
  LPAR'05) for further explanations.
webertj@18408
    21
*}
webertj@18408
    22
webertj@18408
    23
datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
webertj@18408
    24
webertj@18408
    25
constdefs
webertj@18408
    26
  valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
webertj@18408
    27
webertj@18408
    28
  "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==
webertj@18408
    29
    (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)
webertj@18408
    30
    \<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)
webertj@18408
    31
    \<and> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9)
webertj@18408
    32
    \<and> (x4 \<noteq> x5) \<and> (x4 \<noteq> x6) \<and> (x4 \<noteq> x7) \<and> (x4 \<noteq> x8) \<and> (x4 \<noteq> x9)
webertj@18408
    33
    \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9)
webertj@18408
    34
    \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9)
webertj@18408
    35
    \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9)
webertj@18408
    36
    \<and> (x8 \<noteq> x9)"
webertj@18408
    37
webertj@18408
    38
constdefs
webertj@18408
    39
  sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    40
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    41
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    42
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    43
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    44
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    45
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    46
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
webertj@18408
    47
    digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
webertj@18408
    48
webertj@18408
    49
  "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19
webertj@18408
    50
          x21 x22 x23 x24 x25 x26 x27 x28 x29
webertj@18408
    51
          x31 x32 x33 x34 x35 x36 x37 x38 x39
webertj@18408
    52
          x41 x42 x43 x44 x45 x46 x47 x48 x49
webertj@18408
    53
          x51 x52 x53 x54 x55 x56 x57 x58 x59
webertj@18408
    54
          x61 x62 x63 x64 x65 x66 x67 x68 x69
webertj@18408
    55
          x71 x72 x73 x74 x75 x76 x77 x78 x79
webertj@18408
    56
          x81 x82 x83 x84 x85 x86 x87 x88 x89
webertj@18408
    57
          x91 x92 x93 x94 x95 x96 x97 x98 x99 ==
webertj@18408
    58
webertj@18408
    59
       valid x11 x12 x13 x14 x15 x16 x17 x18 x19
webertj@18408
    60
     \<and> valid x21 x22 x23 x24 x25 x26 x27 x28 x29
webertj@18408
    61
     \<and> valid x31 x32 x33 x34 x35 x36 x37 x38 x39
webertj@18408
    62
     \<and> valid x41 x42 x43 x44 x45 x46 x47 x48 x49
webertj@18408
    63
     \<and> valid x51 x52 x53 x54 x55 x56 x57 x58 x59
webertj@18408
    64
     \<and> valid x61 x62 x63 x64 x65 x66 x67 x68 x69
webertj@18408
    65
     \<and> valid x71 x72 x73 x74 x75 x76 x77 x78 x79
webertj@18408
    66
     \<and> valid x81 x82 x83 x84 x85 x86 x87 x88 x89
webertj@18408
    67
     \<and> valid x91 x92 x93 x94 x95 x96 x97 x98 x99
webertj@18408
    68
webertj@18408
    69
     \<and> valid x11 x21 x31 x41 x51 x61 x71 x81 x91
webertj@18408
    70
     \<and> valid x12 x22 x32 x42 x52 x62 x72 x82 x92
webertj@18408
    71
     \<and> valid x13 x23 x33 x43 x53 x63 x73 x83 x93
webertj@18408
    72
     \<and> valid x14 x24 x34 x44 x54 x64 x74 x84 x94
webertj@18408
    73
     \<and> valid x15 x25 x35 x45 x55 x65 x75 x85 x95
webertj@18408
    74
     \<and> valid x16 x26 x36 x46 x56 x66 x76 x86 x96
webertj@18408
    75
     \<and> valid x17 x27 x37 x47 x57 x67 x77 x87 x97
webertj@18408
    76
     \<and> valid x18 x28 x38 x48 x58 x68 x78 x88 x98
webertj@18408
    77
     \<and> valid x19 x29 x39 x49 x59 x69 x79 x89 x99
webertj@18408
    78
webertj@18408
    79
     \<and> valid x11 x12 x13 x21 x22 x23 x31 x32 x33
webertj@18408
    80
     \<and> valid x14 x15 x16 x24 x25 x26 x34 x35 x36
webertj@18408
    81
     \<and> valid x17 x18 x19 x27 x28 x29 x37 x38 x39
webertj@18408
    82
     \<and> valid x41 x42 x43 x51 x52 x53 x61 x62 x63
webertj@18408
    83
     \<and> valid x44 x45 x46 x54 x55 x56 x64 x65 x66
webertj@18408
    84
     \<and> valid x47 x48 x49 x57 x58 x59 x67 x68 x69
webertj@18408
    85
     \<and> valid x71 x72 x73 x81 x82 x83 x91 x92 x93
webertj@18408
    86
     \<and> valid x74 x75 x76 x84 x85 x86 x94 x95 x96
webertj@18408
    87
     \<and> valid x77 x78 x79 x87 x88 x89 x97 x98 x99"
webertj@18408
    88
webertj@18408
    89
text {*
webertj@18408
    90
  Just an arbitrary Sudoku grid:
webertj@18408
    91
*}
webertj@18408
    92
webertj@18408
    93
theorem "\<not> sudoku
webertj@18408
    94
    x11 x12 x13 x14 x15 x16 x17 x18 x19
webertj@18408
    95
    x21 x22 x23 x24 x25 x26 x27 x28 x29
webertj@18408
    96
    x31 x32 x33 x34 x35 x36 x37 x38 x39
webertj@18408
    97
    x41 x42 x43 x44 x45 x46 x47 x48 x49
webertj@18408
    98
    x51 x52 x53 x54 x55 x56 x57 x58 x59
webertj@18408
    99
    x61 x62 x63 x64 x65 x66 x67 x68 x69
webertj@18408
   100
    x71 x72 x73 x74 x75 x76 x77 x78 x79
webertj@18408
   101
    x81 x82 x83 x84 x85 x86 x87 x88 x89
webertj@18408
   102
    x91 x92 x93 x94 x95 x96 x97 x98 x99"
webertj@18408
   103
  apply (unfold sudoku_def valid_def)
webertj@18408
   104
  refute
webertj@18408
   105
oops
webertj@18408
   106
webertj@18408
   107
text {*
webertj@18408
   108
  An "easy" Sudoku:
webertj@18408
   109
*}
webertj@18408
   110
webertj@18408
   111
theorem "\<not> sudoku
webertj@18408
   112
     5   3  x13 x14  7  x16 x17 x18 x19
webertj@18408
   113
     6  x22 x23  1   9   5  x27 x28 x29
webertj@18408
   114
    x31  9   8  x34 x35 x36 x37  6  x39
webertj@18408
   115
     8  x42 x43 x44  6  x46 x47 x48  3 
webertj@18408
   116
     4  x52 x53  8  x55  3  x57 x58  1 
webertj@18408
   117
     7  x62 x63 x64  2  x66 x67 x68  6 
webertj@18408
   118
    x71  6  x73 x74 x75 x76  2   8  x79
webertj@18408
   119
    x81 x82 x83  4   1   9  x87 x88  5 
webertj@18408
   120
    x91 x92 x93 x94  8  x96 x97  7   9 "
webertj@18408
   121
  apply (unfold sudoku_def valid_def)
webertj@18408
   122
  refute
webertj@18408
   123
oops
webertj@18408
   124
webertj@18408
   125
text {*
webertj@18408
   126
  A "hard" Sudoku:
webertj@18408
   127
*}
webertj@18408
   128
webertj@18408
   129
theorem "\<not> sudoku
webertj@18408
   130
    x11  2  x13 x14 x15 x16 x17 x18 x19
webertj@18408
   131
    x21 x22 x23  6  x25 x26 x27 x28  3 
webertj@18408
   132
    x31  7   4  x34  8  x36 x37 x38 x39
webertj@18408
   133
    x41 x42 x43 x44 x45  3  x47 x48  2 
webertj@18408
   134
    x51  8  x53 x54  4  x56 x57  1  x59
webertj@18408
   135
     6  x62 x63  5  x65 x66 x67 x68 x69
webertj@18408
   136
    x71 x72 x73 x74  1  x76  7   8  x79
webertj@18408
   137
     5  x82 x83 x84 x85  9  x87 x88 x89
webertj@18408
   138
    x91 x92 x93 x94 x95 x96 x97  4  x99"
webertj@18408
   139
  apply (unfold sudoku_def valid_def)
webertj@18408
   140
  refute
webertj@18408
   141
oops
webertj@18408
   142
webertj@18408
   143
end