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