127
|
1 |
|
|
2 |
theory Sat
|
329
|
3 |
imports Main "../FirstSteps"
|
127
|
4 |
begin
|
|
5 |
|
181
|
6 |
section {* SAT Solvers\label{rec:sat} *}
|
180
|
7 |
|
|
8 |
text {*
|
|
9 |
{\bf Problem:}
|
|
10 |
You like to use a SAT solver to find out whether
|
|
11 |
an Isabelle formula is satisfiable or not.\smallskip
|
|
12 |
|
|
13 |
{\bf Solution:} Isabelle contains a general interface for
|
|
14 |
a number of external SAT solvers (including ZChaff and Minisat)
|
|
15 |
and also contains a simple internal SAT solver that
|
|
16 |
is based on the DPLL algorithm.\smallskip
|
|
17 |
|
|
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
|
20 |
unknown. The type of the propositional formula is
|
|
21 |
@{ML_type "PropLogic.prop_formula"} with the usual constructors such
|
|
22 |
as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on.
|
|
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
|
28 |
*}
|
|
29 |
|
184
|
30 |
ML{*val (pform, table) =
|
180
|
31 |
PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*}
|
|
32 |
|
|
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
|
41 |
in the table that is given to the translation function and also returned
|
|
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
|
44 |
|
|
45 |
@{ML_response_fake [display,gray]
|
184
|
46 |
"Termtab.dest table"
|
180
|
47 |
"[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
|
|
48 |
|
184
|
49 |
An index is also produced whenever the translation
|
180
|
50 |
function cannot find an appropriate propositional formula for a term.
|
184
|
51 |
Attempting to translate @{term "\<forall>x::nat. P x"}
|
180
|
52 |
*}
|
|
53 |
|
184
|
54 |
ML{*val (pform', table') =
|
180
|
55 |
PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*}
|
|
56 |
|
|
57 |
text {*
|
184
|
58 |
returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table
|
|
59 |
@{ML table'} is:
|
180
|
60 |
|
|
61 |
@{ML_response_fake [display,gray]
|
329
|
62 |
"map (apfst (string_of_term @{context})) (Termtab.dest table')"
|
180
|
63 |
"(\<forall>x. P x, 1)"}
|
|
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
|
70 |
|
|
71 |
@{ML_response_fake [display,gray]
|
184
|
72 |
"SatSolver.invoke_solver \"dpll\" pform"
|
|
73 |
"SatSolver.SATISFIABLE assg"}
|
180
|
74 |
|
184
|
75 |
determines that the formula @{ML pform} is satisfiable. If we inspect
|
|
76 |
the returned function @{text assg}
|
180
|
77 |
|
|
78 |
@{ML_response [display,gray]
|
|
79 |
"let
|
184
|
80 |
val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform
|
180
|
81 |
in
|
184
|
82 |
(assg 1, assg 2, assg 3)
|
180
|
83 |
end"
|
|
84 |
"(SOME true, SOME true, NONE)"}
|
|
85 |
|
|
86 |
we obtain a possible assignment for the variables @{text "A"} and @{text "B"}
|
|
87 |
that makes the formula satisfiable.
|
|
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
|
92 |
|
184
|
93 |
@{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}
|
180
|
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
|
98 |
|
184
|
99 |
There are also two tactics that make use of SAT solvers. One
|
180
|
100 |
is the tactic @{ML sat_tac in sat}. For example
|
|
101 |
*}
|
|
102 |
|
|
103 |
lemma "True"
|
294
|
104 |
apply(tactic {* sat.sat_tac @{context} 1 *})
|
180
|
105 |
done
|
|
106 |
|
|
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
|
112 |
\begin{readmore}
|
|
113 |
The interface for the external SAT solvers is implemented
|
|
114 |
in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple
|
|
115 |
SAT solver based on the DPLL algorithm. The tactics for SAT solvers are
|
181
|
116 |
implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning
|
180
|
117 |
propositional formulas are implemented in @{ML_file
|
181
|
118 |
"HOL/Tools/prop_logic.ML"}. The tables used in the translation function are
|
180
|
119 |
implemented in @{ML_file "Pure/General/table.ML"}.
|
|
120 |
\end{readmore}
|
|
121 |
*}
|
|
122 |
|
127
|
123 |
|
180
|
124 |
end |