equal
deleted
inserted
replaced
1 (* Title: Sudoku.thy |
1 (* Title: Sudoku.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tjark Weber |
3 Author: Tjark Weber |
4 Copyright 2005 |
4 Copyright 2005-2007 |
5 *) |
5 *) |
6 |
6 |
7 header {* A SAT-based Sudoku Solver *} |
7 header {* A SAT-based Sudoku Solver *} |
8 |
8 |
9 theory Sudoku |
9 theory Sudoku |
98 x51 x52 x53 x54 x55 x56 x57 x58 x59 |
98 x51 x52 x53 x54 x55 x56 x57 x58 x59 |
99 x61 x62 x63 x64 x65 x66 x67 x68 x69 |
99 x61 x62 x63 x64 x65 x66 x67 x68 x69 |
100 x71 x72 x73 x74 x75 x76 x77 x78 x79 |
100 x71 x72 x73 x74 x75 x76 x77 x78 x79 |
101 x81 x82 x83 x84 x85 x86 x87 x88 x89 |
101 x81 x82 x83 x84 x85 x86 x87 x88 x89 |
102 x91 x92 x93 x94 x95 x96 x97 x98 x99" |
102 x91 x92 x93 x94 x95 x96 x97 x98 x99" |
103 apply (unfold sudoku_def valid_def) |
|
104 refute |
103 refute |
105 oops |
104 oops |
106 |
105 |
107 text {* |
106 text {* |
108 An "easy" Sudoku: |
107 An "easy" Sudoku: |
116 4 x52 x53 8 x55 3 x57 x58 1 |
115 4 x52 x53 8 x55 3 x57 x58 1 |
117 7 x62 x63 x64 2 x66 x67 x68 6 |
116 7 x62 x63 x64 2 x66 x67 x68 6 |
118 x71 6 x73 x74 x75 x76 2 8 x79 |
117 x71 6 x73 x74 x75 x76 2 8 x79 |
119 x81 x82 x83 4 1 9 x87 x88 5 |
118 x81 x82 x83 4 1 9 x87 x88 5 |
120 x91 x92 x93 x94 8 x96 x97 7 9 " |
119 x91 x92 x93 x94 8 x96 x97 7 9 " |
121 apply (unfold sudoku_def valid_def) |
|
122 refute |
120 refute |
123 oops |
121 oops |
124 |
122 |
125 text {* |
123 text {* |
126 A "hard" Sudoku: |
124 A "hard" Sudoku: |
134 x51 8 x53 x54 4 x56 x57 1 x59 |
132 x51 8 x53 x54 4 x56 x57 1 x59 |
135 6 x62 x63 5 x65 x66 x67 x68 x69 |
133 6 x62 x63 5 x65 x66 x67 x68 x69 |
136 x71 x72 x73 x74 1 x76 7 8 x79 |
134 x71 x72 x73 x74 1 x76 7 8 x79 |
137 5 x82 x83 x84 x85 9 x87 x88 x89 |
135 5 x82 x83 x84 x85 9 x87 x88 x89 |
138 x91 x92 x93 x94 x95 x96 x97 4 x99" |
136 x91 x92 x93 x94 x95 x96 x97 4 x99" |
139 apply (unfold sudoku_def valid_def) |
|
140 refute |
137 refute |
141 oops |
138 oops |
142 |
139 |
143 end |
140 end |