https://www.glc.us.es/~jalonso/RA2014/index.php?action=history&feed=atom&title=Tema_12e%3A_Sudoku
Tema 12e: Sudoku - Historial de revisiones
2026-07-19T04:13:08Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/RA2014/index.php?title=Tema_12e:_Sudoku&diff=297&oldid=prev
WikiSysop: Texto reemplazado: «"isar"» por «"isabelle"»
2018-07-16T08:17:08Z
<p>Texto reemplazado: «"isar"» por «"isabelle"»</p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 08:17 16 jul 2018</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td>
<td colspan="2" class="diff-lineno">Línea 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><source lang="<del class="diffchange diffchange-inline">isar</del>"></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><source lang="<ins class="diffchange diffchange-inline">isabelle</ins>"></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>(*  Title:      HOL/ex/Sudoku.thy</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>(*  Title:      HOL/ex/Sudoku.thy</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>     Author:    Tjark Weber</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>     Author:    Tjark Weber</div></td></tr>
</table>
WikiSysop
https://www.glc.us.es/~jalonso/RA2014/index.php?title=Tema_12e:_Sudoku&diff=278&oldid=prev
Jalonso: Página creada con '<source lang="isar"> (* Title: HOL/ex/Sudoku.thy Author: Tjark Weber Copyright 2005-2014 *) header {* A SAT-based Sudoku Solver *} theory T12e_Sudoku impor...'
2015-01-29T12:14:36Z
<p>Página creada con '<source lang="isar"> (* Title: HOL/ex/Sudoku.thy Author: Tjark Weber Copyright 2005-2014 *) header {* A SAT-based Sudoku Solver *} theory T12e_Sudoku impor...'</p>
<p><b>Página nueva</b></p><div><source lang="isar"><br />
(* Title: HOL/ex/Sudoku.thy<br />
Author: Tjark Weber<br />
Copyright 2005-2014<br />
*)<br />
<br />
header {* A SAT-based Sudoku Solver *}<br />
<br />
theory T12e_Sudoku<br />
imports Main<br />
begin<br />
<br />
text {*<br />
See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at<br />
LPAR'05) for further explanations. (The paper describes an older <br />
version of this theory that used the model finder refute to find <br />
Sudoku solutions. The refute tool has since been superseded by <br />
nitpick, which is used below.)<br />
*}<br />
<br />
no_notation Groups.one_class.one ("1")<br />
<br />
datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | <br />
F ("6") | G ("7") | H ("8") | I ("9")<br />
<br />
definition valid :: "digit => digit => digit => digit => digit => <br />
digit => digit => digit => digit => bool" where<br />
"valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ≡<br />
(x1≠x2)∧(x1≠x3)∧(x1≠x4)∧(x1≠x5)∧(x1≠x6)∧(x1≠x7)∧(x1≠x8)∧(x1≠x9)<br />
∧(x2≠x3)∧(x2≠x4)∧(x2≠x5)∧(x2≠x6)∧(x2≠x7)∧(x2≠x8)∧(x2≠x9)<br />
∧(x3≠x4)∧(x3≠x5)∧(x3≠x6)∧(x3≠x7)∧(x3≠x8)∧(x3≠x9)<br />
∧(x4≠x5)∧(x4≠x6)∧(x4≠x7)∧(x4≠x8)∧(x4≠x9)<br />
∧(x5≠x6)∧(x5≠x7)∧(x5≠x8)∧(x5≠x9)<br />
∧(x6≠x7)∧(x6≠x8)∧(x6≠x9)<br />
∧(x7≠x8)∧(x7≠x9)<br />
∧(x8≠x9)"<br />
<br />
definition sudoku :: <br />
"digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit =><br />
digit => digit => digit => digit => digit => digit => digit => digit => digit => <br />
bool" where<br />
"sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19<br />
x21 x22 x23 x24 x25 x26 x27 x28 x29<br />
x31 x32 x33 x34 x35 x36 x37 x38 x39<br />
x41 x42 x43 x44 x45 x46 x47 x48 x49<br />
x51 x52 x53 x54 x55 x56 x57 x58 x59<br />
x61 x62 x63 x64 x65 x66 x67 x68 x69<br />
x71 x72 x73 x74 x75 x76 x77 x78 x79<br />
x81 x82 x83 x84 x85 x86 x87 x88 x89<br />
x91 x92 x93 x94 x95 x96 x97 x98 x99 ≡<br />
<br />
valid x11 x12 x13 x14 x15 x16 x17 x18 x19<br />
∧ valid x21 x22 x23 x24 x25 x26 x27 x28 x29<br />
∧ valid x31 x32 x33 x34 x35 x36 x37 x38 x39<br />
∧ valid x41 x42 x43 x44 x45 x46 x47 x48 x49<br />
∧ valid x51 x52 x53 x54 x55 x56 x57 x58 x59<br />
∧ valid x61 x62 x63 x64 x65 x66 x67 x68 x69<br />
∧ valid x71 x72 x73 x74 x75 x76 x77 x78 x79<br />
∧ valid x81 x82 x83 x84 x85 x86 x87 x88 x89<br />
∧ valid x91 x92 x93 x94 x95 x96 x97 x98 x99<br />
<br />
∧ valid x11 x21 x31 x41 x51 x61 x71 x81 x91<br />
∧ valid x12 x22 x32 x42 x52 x62 x72 x82 x92<br />
∧ valid x13 x23 x33 x43 x53 x63 x73 x83 x93<br />
∧ valid x14 x24 x34 x44 x54 x64 x74 x84 x94<br />
∧ valid x15 x25 x35 x45 x55 x65 x75 x85 x95<br />
∧ valid x16 x26 x36 x46 x56 x66 x76 x86 x96<br />
∧ valid x17 x27 x37 x47 x57 x67 x77 x87 x97<br />
∧ valid x18 x28 x38 x48 x58 x68 x78 x88 x98<br />
∧ valid x19 x29 x39 x49 x59 x69 x79 x89 x99<br />
<br />
∧ valid x11 x12 x13 x21 x22 x23 x31 x32 x33<br />
∧ valid x14 x15 x16 x24 x25 x26 x34 x35 x36<br />
∧ valid x17 x18 x19 x27 x28 x29 x37 x38 x39<br />
∧ valid x41 x42 x43 x51 x52 x53 x61 x62 x63<br />
∧ valid x44 x45 x46 x54 x55 x56 x64 x65 x66<br />
∧ valid x47 x48 x49 x57 x58 x59 x67 x68 x69<br />
∧ valid x71 x72 x73 x81 x82 x83 x91 x92 x93<br />
∧ valid x74 x75 x76 x84 x85 x86 x94 x95 x96<br />
∧ valid x77 x78 x79 x87 x88 x89 x97 x98 x99"<br />
<br />
text {*<br />
Just an arbitrary Sudoku grid:<br />
*}<br />
<br />
theorem "¬ sudoku<br />
x11 x12 x13 x14 x15 x16 x17 x18 x19<br />
x21 x22 x23 x24 x25 x26 x27 x28 x29<br />
x31 x32 x33 x34 x35 x36 x37 x38 x39<br />
x41 x42 x43 x44 x45 x46 x47 x48 x49<br />
x51 x52 x53 x54 x55 x56 x57 x58 x59<br />
x61 x62 x63 x64 x65 x66 x67 x68 x69<br />
x71 x72 x73 x74 x75 x76 x77 x78 x79<br />
x81 x82 x83 x84 x85 x86 x87 x88 x89<br />
x91 x92 x93 x94 x95 x96 x97 x98 x99"<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
An ``easy'' Sudoku:<br />
*}<br />
<br />
theorem "¬ sudoku<br />
5 3 x13 x14 7 x16 x17 x18 x19<br />
6 x22 x23 1 9 5 x27 x28 x29<br />
x31 9 8 x34 x35 x36 x37 6 x39<br />
8 x42 x43 x44 6 x46 x47 x48 3 <br />
4 x52 x53 8 x55 3 x57 x58 1 <br />
7 x62 x63 x64 2 x66 x67 x68 6 <br />
x71 6 x73 x74 x75 x76 2 8 x79<br />
x81 x82 x83 4 1 9 x87 x88 5 <br />
x91 x92 x93 x94 8 x96 x97 7 9 "<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
A ``hard'' Sudoku:<br />
*}<br />
<br />
theorem "¬ sudoku<br />
x11 2 x13 x14 x15 x16 x17 x18 x19<br />
x21 x22 x23 6 x25 x26 x27 x28 3 <br />
x31 7 4 x34 8 x36 x37 x38 x39<br />
x41 x42 x43 x44 x45 3 x47 x48 2 <br />
x51 8 x53 x54 4 x56 x57 1 x59<br />
6 x62 x63 5 x65 x66 x67 x68 x69<br />
x71 x72 x73 x74 1 x76 7 8 x79<br />
5 x82 x83 x84 x85 9 x87 x88 x89<br />
x91 x92 x93 x94 x95 x96 x97 4 x99"<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
Some ``exceptionally difficult'' Sudokus, taken from<br />
@{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}<br />
(accessed December~2, 2008).<br />
*}<br />
<br />
text {*<br />
\begin{verbatim}<br />
Rating Program: gsf's sudoku q1 (rating) <br />
Rating: 99408 <br />
Poster: JPF <br />
Label: Easter Monster <br />
1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1 <br />
1 . . | . . . | . . 2 <br />
. 9 . | 4 . . | . 5 . <br />
. . 6 | . . . | 7 . . <br />
------+-------+------ <br />
. 5 . | 9 . 3 | . . . <br />
. . . | . 7 . | . . . <br />
. . . | 8 5 . | . 4 . <br />
------+-------+------ <br />
7 . . | . . . | 6 . . <br />
. 3 . | . . 9 | . 8 . <br />
. . 2 | . . . | . . 1 <br />
\end{verbatim}<br />
*}<br />
<br />
theorem "¬ sudoku<br />
1 x12 x13 x14 x15 x16 x17 x18 2 <br />
x21 9 x23 4 x25 x26 x27 5 x29<br />
x31 x32 6 x34 x35 x36 7 x38 x39<br />
x41 5 x43 9 x45 3 x47 x48 x49<br />
x51 x52 x53 x54 7 x56 x57 x58 x59<br />
x61 x62 x63 8 5 x66 x67 4 x69<br />
7 x72 x73 x74 x75 x76 6 x78 x79<br />
x81 3 x83 x84 x85 9 x87 8 x89<br />
x91 x92 2 x94 x95 x96 x97 x98 1 "<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
\begin{verbatim}<br />
Rating Program: gsf's sudoku q1 (Processing time) <br />
Rating: 4m19s@2 GHz <br />
Poster: tarek <br />
Label: tarek071223170000-052 <br />
..1..4.......6.3.5...9.....8.....7.3.......285...7.6..3...8...6..92......4...1... <br />
. . 1 | . . 4 | . . . <br />
. . . | . 6 . | 3 . 5 <br />
. . . | 9 . . | . . . <br />
------+-------+------ <br />
8 . . | . . . | 7 . 3 <br />
. . . | . . . | . 2 8 <br />
5 . . | . 7 . | 6 . . <br />
------+-------+------ <br />
3 . . | . 8 . | . . 6 <br />
. . 9 | 2 . . | . . . <br />
. 4 . | . . 1 | . . . <br />
\end{verbatim}<br />
*}<br />
<br />
theorem "¬ sudoku<br />
x11 x12 1 x14 x15 4 x17 x18 x19<br />
x21 x22 x23 x24 6 x26 3 x28 5 <br />
x31 x32 x33 9 x35 x36 x37 x38 x39<br />
8 x42 x43 x44 x45 x46 7 x48 3 <br />
x51 x52 x53 x54 x55 x56 x57 2 8 <br />
5 x62 x63 x64 7 x66 6 x68 x69<br />
3 x72 x73 x74 8 x76 x77 x78 6 <br />
x81 x82 9 2 x85 x86 x87 x88 x89<br />
x91 4 x93 x94 x95 1 x97 x98 x99"<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
\begin{verbatim}<br />
Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1 <br />
Rating: 11.9 <br />
Poster: tarek <br />
Label: golden nugget <br />
.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7..... <br />
. . . | . . . | . 3 9 <br />
. . . | . . 1 | . . 5 <br />
. . 3 | . 5 . | 8 . . <br />
------+-------+------ <br />
. . 8 | . 9 . | . . 6 <br />
. 7 . | . . 2 | . . . <br />
1 . . | 4 . . | . . . <br />
------+-------+------ <br />
. . 9 | . 8 . | . 5 . <br />
. 2 . | . . . | 6 . . <br />
4 . . | 7 . . | . . . <br />
\end{verbatim}<br />
*}<br />
<br />
theorem "¬ sudoku<br />
x11 x12 x13 x14 x15 x16 x17 3 9 <br />
x21 x22 x23 x24 x25 1 x27 x28 5 <br />
x31 x32 3 x34 5 x36 8 x38 x39<br />
x41 x42 8 x44 9 x46 x47 x48 6 <br />
x51 7 x53 x54 x55 2 x57 x58 x59<br />
1 x62 x63 4 x65 x66 x67 x68 x69<br />
x71 x72 9 x74 8 x76 x77 5 x79<br />
x81 2 x83 x84 x85 x86 6 x88 x89<br />
4 x92 x93 7 x95 x96 x97 x98 x99"<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
\begin{verbatim}<br />
Rating Program: dukuso's suexrat9 <br />
Rating: 4483 <br />
Poster: coloin <br />
Label: col-02-08-071 <br />
.2.4.37.........32........4.4.2...7.8...5.........1...5.....9...3.9....7..1..86.. <br />
. 2 . | 4 . 3 | 7 . . <br />
. . . | . . . | . 3 2 <br />
. . . | . . . | . . 4 <br />
------+-------+------ <br />
. 4 . | 2 . . | . 7 . <br />
8 . . | . 5 . | . . . <br />
. . . | . . 1 | . . . <br />
------+-------+------ <br />
5 . . | . . . | 9 . . <br />
. 3 . | 9 . . | . . 7 <br />
. . 1 | . . 8 | 6 . . <br />
\end{verbatim}<br />
*}<br />
<br />
theorem "¬ sudoku<br />
x11 2 x13 4 x15 3 7 x18 x19<br />
x21 x22 x23 x24 x25 x26 x27 3 2 <br />
x31 x32 x33 x34 x35 x36 x37 x38 4 <br />
x41 4 x43 2 x45 x46 x47 7 x49<br />
8 x52 x53 x54 5 x56 x57 x58 x59<br />
x61 x62 x63 x64 x65 1 x67 x68 x69<br />
5 x72 x73 x74 x75 x76 9 x78 x79<br />
x81 3 x83 9 x85 x86 x87 x88 7 <br />
x91 x92 1 x94 x95 8 6 x98 x99"<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
text {*<br />
\begin{verbatim}<br />
Rating Program: dukuso's suexratt (10000 2 option) <br />
Rating: 2141 <br />
Poster: tarek <br />
Label: golden nugget <br />
.......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7..... <br />
. . . | . . . | . 3 9 <br />
. . . | . . 1 | . . 5 <br />
. . 3 | . 5 . | 8 . . <br />
------+-------+------ <br />
. . 8 | . 9 . | . . 6 <br />
. 7 . | . . 2 | . . . <br />
1 . . | 4 . . | . . . <br />
------+-------+------ <br />
. . 9 | . 8 . | . 5 . <br />
. 2 . | . . . | 6 . . <br />
4 . . | 7 . . | . . .<br />
\end{verbatim}<br />
*}<br />
<br />
theorem "¬ sudoku<br />
x11 x12 x13 x14 x15 x16 x17 3 9 <br />
x21 x22 x23 x24 x25 1 x27 x28 5 <br />
x31 x32 3 x34 5 x36 8 x38 x39<br />
x41 x42 8 x44 9 x46 x47 x48 6 <br />
x51 7 x53 x54 x55 2 x57 x58 x59<br />
1 x62 x63 4 x65 x66 x67 x68 x69<br />
x71 x72 9 x74 8 x76 x77 5 x79<br />
x81 2 x83 x84 x85 x86 6 x88 x89<br />
4 x92 x93 7 x95 x96 x97 x98 x99"<br />
nitpick [expect=genuine]<br />
oops<br />
<br />
end<br />
</source></div>
Jalonso