+ −
theory Sat+ −
imports Main "../Base"+ −
begin+ −
+ −
section {* SAT Solvers\label{rec:sat} *}+ −
+ −
text {*+ −
{\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 "PropLogic.prop_formula"} with the usual constructors such + −
as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on.+ −
+ −
The function @{ML PropLogic.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 + −
*}+ −
+ −
ML{*val (pform, table) = + −
PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*}+ −
+ −
text {*+ −
then the resulting propositional formula @{ML pform} is + −
+ −
@{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} + −
+ −
+ −
where indices are assigned for the variables + −
@{text "A"} and @{text "B"}, 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_fake [display,gray]+ −
"Termtab.dest table"+ −
"[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}+ −
+ −
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"}+ −
*}+ −
+ −
ML{*val (pform', table') = + −
PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*}+ −
+ −
text {*+ −
returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table + −
@{ML table'} is:+ −
+ −
@{ML_response_fake [display,gray]+ −
"map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"+ −
"(\<forall>x. P x, 1)"}+ −
+ −
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 "SatSolver.invoke_solver"}. For example+ −
+ −
@{ML_response_fake [display,gray]+ −
"SatSolver.invoke_solver \"dpll\" pform"+ −
"SatSolver.SATISFIABLE assg"}+ −
+ −
determines that the formula @{ML pform} is satisfiable. If we inspect+ −
the returned function @{text assg}+ −
+ −
@{ML_response [display,gray]+ −
"let+ −
val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform+ −
in + −
(assg 1, assg 2, assg 3)+ −
end"+ −
"(SOME true, SOME true, NONE)"}+ −
+ −
we obtain a possible assignment for the variables @{text "A"} and @{text "B"}+ −
that makes the formula satisfiable. + −
+ −
Note that we invoked the SAT solver with the string @{text [quotes] dpll}. + −
This string specifies which SAT solver is invoked (in this case the internal+ −
one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"}+ −
+ −
@{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}+ −
+ −
several external SAT solvers will be tried (assuming they are installed). + −
If no external SAT solver is installed, then the default is + −
@{text [quotes] "dpll"}.+ −
+ −
There are also two tactics that make use of SAT solvers. One + −
is the tactic @{ML sat_tac in sat}. For example + −
*}+ −
+ −
lemma "True"+ −
apply(tactic {* sat.sat_tac @{context} 1 *})+ −
done+ −
+ −
text {*+ −
However, for proving anything more exciting using @{ML "sat_tac" 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_funcs.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}+ −
*}+ −
+ −
+ −
end+ −