+ −
theory Sat+ −
imports "../Appendix" "../First_Steps" + −
begin+ −
+ −
section \<open>SAT Solvers\label{rec:sat}\<close>+ −
+ −
text \<open>+ −
{\bf Problem:}+ −
You like to use a SAT solver to find out whether+ −
an Isabelle formula is satisfiable or not.\smallskip+ −
+ −
{\bf Solution:} Isabelle contains a general interface for + −
a number of external SAT solvers (including ZChaff and Minisat)+ −
and also contains a simple internal SAT solver that+ −
is based on the DPLL algorithm.\smallskip+ −
+ −
The SAT solvers expect a propositional formula as input and produce+ −
a result indicating that the formula is either satisfiable, unsatisfiable or+ −
unknown. The type of the propositional formula is + −
@{ML_type "Prop_Logic.prop_formula"} with the usual constructors such + −
as @{ML And in Prop_Logic}, @{ML Or in Prop_Logic} and so on.+ −
+ −
The function @{ML Prop_Logic.prop_formula_of_term} translates an Isabelle + −
term into a propositional formula. Let+ −
us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. + −
The function will return a propositional formula and a table. Suppose + −
\<close>+ −
+ −
ML %grayML\<open>val (pform, table) = + −
Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty\<close>+ −
+ −
text \<open>+ −
then the resulting propositional formula @{ML pform} is + −
+ −
@{ML [display] \<open>Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)\<close> in Prop_Logic} + −
+ −
+ −
where indices are assigned for the variables + −
\<open>A\<close> and \<open>B\<close>, respectively. This assignment is recorded + −
in the table that is given to the translation function and also returned + −
(appropriately updated) in the result. In the case above the+ −
input table is empty (i.e.~@{ML Termtab.empty}) and the output table is+ −
+ −
@{ML_response [display,gray]+ −
\<open>Termtab.dest table\<close>+ −
\<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>}+ −
+ −
An index is also produced whenever the translation+ −
function cannot find an appropriate propositional formula for a term. + −
Attempting to translate @{term "\<forall>x::nat. P x"}+ −
\<close>+ −
+ −
ML %grayML\<open>val (pform', table') = + −
Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty\<close>+ −
+ −
text \<open>+ −
returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for @{ML pform'} and the table + −
@{ML table'} is:+ −
+ −
@{ML_response [display,gray]+ −
\<open>map (apfst (YXML.content_of o Syntax.string_of_term @{context})) (Termtab.dest table')\<close>+ −
\<open>("\<forall>x. P x", 1)\<close>}+ −
+ −
In the print out of the tabel, we used some pretty printing scaffolding + −
to see better which assignment the table contains.+ −
+ −
Having produced a propositional formula, you can now call the SAT solvers + −
with the function @{ML \<open>SAT_Solver.invoke_solver\<close>}. For example+ −
+ −
@{ML_matchresult_fake [display,gray]+ −
\<open>SAT_Solver.invoke_solver "minisat" pform\<close>+ −
\<open>SAT_Solver.SATISFIABLE assg\<close>}+ −
\<close>+ −
+ −
text \<open>+ −
determines that the formula @{ML pform} is satisfiable. If we inspect+ −
the returned function \<open>assg\<close>+ −
+ −
@{ML_matchresult [display,gray]+ −
\<open>let+ −
val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver "auto" pform+ −
in + −
(assg 1, assg 2, assg 3)+ −
end\<close>+ −
\<open>(NONE, SOME true, NONE)\<close>}+ −
+ −
we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close>+ −
that makes the formula satisfiable. + −
+ −
Note that we invoked the SAT solver with the string @{text [quotes] auto}. + −
This string specifies which specific SAT solver is invoked. If instead + −
called with @{text [quotes] "auto"}+ −
several external SAT solvers will be tried (assuming they are installed). + −
+ −
There are also two tactics that make use of SAT solvers. One + −
is the tactic @{ML sat_tac in SAT}. For example + −
\<close>+ −
+ −
lemma "True"+ −
apply(tactic \<open>SAT.sat_tac @{context} 1\<close>)+ −
done+ −
+ −
text \<open>+ −
However, for proving anything more exciting using @{ML \<open>sat_tac\<close> in SAT} you + −
have to use a SAT solver that can produce a proof. The internal + −
one is not usuable for this. + −
+ −
\begin{readmore} + −
The interface for the external SAT solvers is implemented+ −
in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple+ −
SAT solver based on the DPLL algorithm. The tactics for SAT solvers are+ −
implemented in @{ML_file "HOL/Tools/sat.ML"}. Functions concerning+ −
propositional formulas are implemented in @{ML_file+ −
"HOL/Tools/prop_logic.ML"}. The tables used in the translation function are+ −
implemented in @{ML_file "Pure/General/table.ML"}. + −
\end{readmore}+ −
\<close>+ −
+ −
+ −
end+ −