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