author | Christian Urban <urbanc@in.tum.de> |
Sat, 07 Nov 2009 01:03:37 +0100 | |
changeset 375 | 92f7328dc5cc |
parent 346 | 0fea8b7a14a1 |
child 441 | 520127b708e6 |
permissions | -rw-r--r-- |
127
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
|
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Sat |
346
0fea8b7a14a1
tuned the ML-output mechanism; tuned slightly the text
Christian Urban <urbanc@in.tum.de>
parents:
329
diff
changeset
|
3 |
imports "../Appendix" "../FirstSteps" |
127
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
begin |
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
181
5baaabe1ab92
updated to new method_setup
Christian Urban <urbanc@in.tum.de>
parents:
180
diff
changeset
|
6 |
section {* SAT Solvers\label{rec:sat} *} |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
7 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
8 |
text {* |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
9 |
{\bf Problem:} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
10 |
You like to use a SAT solver to find out whether |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
11 |
an Isabelle formula is satisfiable or not.\smallskip |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
12 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
13 |
{\bf Solution:} Isabelle contains a general interface for |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
14 |
a number of external SAT solvers (including ZChaff and Minisat) |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
15 |
and also contains a simple internal SAT solver that |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
16 |
is based on the DPLL algorithm.\smallskip |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
17 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
18 |
The SAT solvers expect a propositional formula as input and produce |
184 | 19 |
a result indicating that the formula is either satisfiable, unsatisfiable or |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
20 |
unknown. The type of the propositional formula is |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
21 |
@{ML_type "PropLogic.prop_formula"} with the usual constructors such |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
22 |
as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on. |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
23 |
|
184 | 24 |
The function @{ML PropLogic.prop_formula_of_term} translates an Isabelle |
25 |
term into a propositional formula. Let |
|
26 |
us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
|
27 |
The function will return a propositional formula and a table. Suppose |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
28 |
*} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
29 |
|
184 | 30 |
ML{*val (pform, table) = |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
31 |
PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
32 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
33 |
text {* |
184 | 34 |
then the resulting propositional formula @{ML pform} is |
35 |
||
36 |
@{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} |
|
37 |
||
38 |
||
39 |
where indices are assigned for the variables |
|
40 |
@{text "A"} and @{text "B"}, respectively. This assignment is recorded |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
41 |
in the table that is given to the translation function and also returned |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
42 |
(appropriately updated) in the result. In the case above the |
184 | 43 |
input table is empty (i.e.~@{ML Termtab.empty}) and the output table is |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
44 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
45 |
@{ML_response_fake [display,gray] |
184 | 46 |
"Termtab.dest table" |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
47 |
"[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
48 |
|
184 | 49 |
An index is also produced whenever the translation |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
50 |
function cannot find an appropriate propositional formula for a term. |
184 | 51 |
Attempting to translate @{term "\<forall>x::nat. P x"} |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
52 |
*} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
53 |
|
184 | 54 |
ML{*val (pform', table') = |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
55 |
PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
56 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
57 |
text {* |
184 | 58 |
returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table |
59 |
@{ML table'} is: |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
60 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
61 |
@{ML_response_fake [display,gray] |
329 | 62 |
"map (apfst (string_of_term @{context})) (Termtab.dest table')" |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
63 |
"(\<forall>x. P x, 1)"} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
64 |
|
191 | 65 |
In the print out of the tabel, we used some pretty printing scaffolding |
66 |
to see better which assignment the table contains. |
|
184 | 67 |
|
68 |
Having produced a propositional formula, you can now call the SAT solvers |
|
69 |
with the function @{ML "SatSolver.invoke_solver"}. For example |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
70 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
71 |
@{ML_response_fake [display,gray] |
184 | 72 |
"SatSolver.invoke_solver \"dpll\" pform" |
73 |
"SatSolver.SATISFIABLE assg"} |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
74 |
|
184 | 75 |
determines that the formula @{ML pform} is satisfiable. If we inspect |
76 |
the returned function @{text assg} |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
77 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
78 |
@{ML_response [display,gray] |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
79 |
"let |
184 | 80 |
val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
81 |
in |
184 | 82 |
(assg 1, assg 2, assg 3) |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
83 |
end" |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
84 |
"(SOME true, SOME true, NONE)"} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
85 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
86 |
we obtain a possible assignment for the variables @{text "A"} and @{text "B"} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
87 |
that makes the formula satisfiable. |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
88 |
|
184 | 89 |
Note that we invoked the SAT solver with the string @{text [quotes] dpll}. |
90 |
This string specifies which SAT solver is invoked (in this case the internal |
|
91 |
one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"} |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
92 |
|
184 | 93 |
@{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"} |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
94 |
|
184 | 95 |
several external SAT solvers will be tried (assuming they are installed). |
96 |
If no external SAT solver is installed, then the default is |
|
97 |
@{text [quotes] "dpll"}. |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
98 |
|
184 | 99 |
There are also two tactics that make use of SAT solvers. One |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
100 |
is the tactic @{ML sat_tac in sat}. For example |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
101 |
*} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
102 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
103 |
lemma "True" |
294
ee9d53fbb56b
made changes for SUBPROOF and sat_tac
Christian Urban <urbanc@in.tum.de>
parents:
191
diff
changeset
|
104 |
apply(tactic {* sat.sat_tac @{context} 1 *}) |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
105 |
done |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
106 |
|
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
107 |
text {* |
191 | 108 |
However, for proving anything more exciting using @{ML "sat_tac" in sat} you |
109 |
have to use a SAT solver that can produce a proof. The internal |
|
110 |
one is not usuable for this. |
|
184 | 111 |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
112 |
\begin{readmore} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
113 |
The interface for the external SAT solvers is implemented |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
114 |
in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
115 |
SAT solver based on the DPLL algorithm. The tactics for SAT solvers are |
181
5baaabe1ab92
updated to new method_setup
Christian Urban <urbanc@in.tum.de>
parents:
180
diff
changeset
|
116 |
implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
117 |
propositional formulas are implemented in @{ML_file |
181
5baaabe1ab92
updated to new method_setup
Christian Urban <urbanc@in.tum.de>
parents:
180
diff
changeset
|
118 |
"HOL/Tools/prop_logic.ML"}. The tables used in the translation function are |
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
119 |
implemented in @{ML_file "Pure/General/table.ML"}. |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
120 |
\end{readmore} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
121 |
*} |
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
122 |
|
127
74846cb0fff9
updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
|
180
9c25418db6f0
added a recipy about SAT solvers
Christian Urban <urbanc@in.tum.de>
parents:
127
diff
changeset
|
124 |
end |