--- a/src/HOL/IsaMakefile Wed Dec 14 18:01:50 2005 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 14 22:05:22 2005 +0100
@@ -602,8 +602,8 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \
- ex/Classical.thy ex/Chinese.thy Library/Commutative_Ring.thy \
- ex/Commutative_RingEx.thy \
+ ex/Classical.thy ex/Chinese.thy Library/Commutative_Ring.thy \
+ ex/Commutative_RingEx.thy \
ex/Commutative_Ring_Complete.thy ex/Hebrew.thy \
ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
@@ -612,8 +612,9 @@
ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML \
ex/Recdefs.thy ex/Records.thy ex/Reflected_Presburger.thy \
- ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
- ex/StringEx.thy ex/Tarski.thy ex/document/root.bib \
+ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/Sudoku.thy \
+ ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
+ ex/StringEx.thy ex/Tarski.thy ex/document/root.bib \
ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/set.thy \
ex/svc_funcs.ML ex/svc_test.ML ex/svc_test.thy
@$(ISATOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/ex/ROOT.ML Wed Dec 14 18:01:50 2005 +0100
+++ b/src/HOL/ex/ROOT.ML Wed Dec 14 22:05:22 2005 +0100
@@ -47,6 +47,12 @@
(* requires zChaff with proof generation to be installed: *)
time_use_thy "SAT_Examples" handle ERROR => ();
+(* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
+if getenv "ZCHAFF_HOME" <> "" then
+ time_use_thy "Sudoku"
+else
+ ();
+
time_use_thy "Refute_Examples";
time_use_thy "Quickcheck_Examples";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Sudoku.thy Wed Dec 14 22:05:22 2005 +0100
@@ -0,0 +1,143 @@
+(* Title: Sudoku.thy
+ ID: $Id$
+ Author: Tjark Weber
+ Copyright 2005
+*)
+
+header {* A SAT-based Sudoku Solver *}
+
+theory Sudoku
+
+imports Main
+
+begin
+
+text {*
+ Please make sure you are using an efficient SAT solver (e.g. zChaff)
+ when loading this theory. See Isabelle's settings file for details.
+
+ See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
+ LPAR'05) for further explanations.
+*}
+
+datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
+
+constdefs
+ valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
+
+ "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==
+ (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)
+ \<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)
+ \<and> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9)
+ \<and> (x4 \<noteq> x5) \<and> (x4 \<noteq> x6) \<and> (x4 \<noteq> x7) \<and> (x4 \<noteq> x8) \<and> (x4 \<noteq> x9)
+ \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9)
+ \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9)
+ \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9)
+ \<and> (x8 \<noteq> x9)"
+
+constdefs
+ sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit =>
+ digit => digit => digit => digit => digit => digit => digit => digit => digit => bool"
+
+ "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19
+ x21 x22 x23 x24 x25 x26 x27 x28 x29
+ x31 x32 x33 x34 x35 x36 x37 x38 x39
+ x41 x42 x43 x44 x45 x46 x47 x48 x49
+ x51 x52 x53 x54 x55 x56 x57 x58 x59
+ x61 x62 x63 x64 x65 x66 x67 x68 x69
+ x71 x72 x73 x74 x75 x76 x77 x78 x79
+ x81 x82 x83 x84 x85 x86 x87 x88 x89
+ x91 x92 x93 x94 x95 x96 x97 x98 x99 ==
+
+ valid x11 x12 x13 x14 x15 x16 x17 x18 x19
+ \<and> valid x21 x22 x23 x24 x25 x26 x27 x28 x29
+ \<and> valid x31 x32 x33 x34 x35 x36 x37 x38 x39
+ \<and> valid x41 x42 x43 x44 x45 x46 x47 x48 x49
+ \<and> valid x51 x52 x53 x54 x55 x56 x57 x58 x59
+ \<and> valid x61 x62 x63 x64 x65 x66 x67 x68 x69
+ \<and> valid x71 x72 x73 x74 x75 x76 x77 x78 x79
+ \<and> valid x81 x82 x83 x84 x85 x86 x87 x88 x89
+ \<and> valid x91 x92 x93 x94 x95 x96 x97 x98 x99
+
+ \<and> valid x11 x21 x31 x41 x51 x61 x71 x81 x91
+ \<and> valid x12 x22 x32 x42 x52 x62 x72 x82 x92
+ \<and> valid x13 x23 x33 x43 x53 x63 x73 x83 x93
+ \<and> valid x14 x24 x34 x44 x54 x64 x74 x84 x94
+ \<and> valid x15 x25 x35 x45 x55 x65 x75 x85 x95
+ \<and> valid x16 x26 x36 x46 x56 x66 x76 x86 x96
+ \<and> valid x17 x27 x37 x47 x57 x67 x77 x87 x97
+ \<and> valid x18 x28 x38 x48 x58 x68 x78 x88 x98
+ \<and> valid x19 x29 x39 x49 x59 x69 x79 x89 x99
+
+ \<and> valid x11 x12 x13 x21 x22 x23 x31 x32 x33
+ \<and> valid x14 x15 x16 x24 x25 x26 x34 x35 x36
+ \<and> valid x17 x18 x19 x27 x28 x29 x37 x38 x39
+ \<and> valid x41 x42 x43 x51 x52 x53 x61 x62 x63
+ \<and> valid x44 x45 x46 x54 x55 x56 x64 x65 x66
+ \<and> valid x47 x48 x49 x57 x58 x59 x67 x68 x69
+ \<and> valid x71 x72 x73 x81 x82 x83 x91 x92 x93
+ \<and> valid x74 x75 x76 x84 x85 x86 x94 x95 x96
+ \<and> valid x77 x78 x79 x87 x88 x89 x97 x98 x99"
+
+text {*
+ Just an arbitrary Sudoku grid:
+*}
+
+theorem "\<not> sudoku
+ x11 x12 x13 x14 x15 x16 x17 x18 x19
+ x21 x22 x23 x24 x25 x26 x27 x28 x29
+ x31 x32 x33 x34 x35 x36 x37 x38 x39
+ x41 x42 x43 x44 x45 x46 x47 x48 x49
+ x51 x52 x53 x54 x55 x56 x57 x58 x59
+ x61 x62 x63 x64 x65 x66 x67 x68 x69
+ x71 x72 x73 x74 x75 x76 x77 x78 x79
+ x81 x82 x83 x84 x85 x86 x87 x88 x89
+ x91 x92 x93 x94 x95 x96 x97 x98 x99"
+ apply (unfold sudoku_def valid_def)
+ refute
+oops
+
+text {*
+ An "easy" Sudoku:
+*}
+
+theorem "\<not> sudoku
+ 5 3 x13 x14 7 x16 x17 x18 x19
+ 6 x22 x23 1 9 5 x27 x28 x29
+ x31 9 8 x34 x35 x36 x37 6 x39
+ 8 x42 x43 x44 6 x46 x47 x48 3
+ 4 x52 x53 8 x55 3 x57 x58 1
+ 7 x62 x63 x64 2 x66 x67 x68 6
+ x71 6 x73 x74 x75 x76 2 8 x79
+ x81 x82 x83 4 1 9 x87 x88 5
+ x91 x92 x93 x94 8 x96 x97 7 9 "
+ apply (unfold sudoku_def valid_def)
+ refute
+oops
+
+text {*
+ A "hard" Sudoku:
+*}
+
+theorem "\<not> sudoku
+ x11 2 x13 x14 x15 x16 x17 x18 x19
+ x21 x22 x23 6 x25 x26 x27 x28 3
+ x31 7 4 x34 8 x36 x37 x38 x39
+ x41 x42 x43 x44 x45 3 x47 x48 2
+ x51 8 x53 x54 4 x56 x57 1 x59
+ 6 x62 x63 5 x65 x66 x67 x68 x69
+ x71 x72 x73 x74 1 x76 7 8 x79
+ 5 x82 x83 x84 x85 9 x87 x88 x89
+ x91 x92 x93 x94 x95 x96 x97 4 x99"
+ apply (unfold sudoku_def valid_def)
+ refute
+oops
+
+end