+
−
theory Sat+
−
imports Main "../Base"+
−
begin+
−
+
−
section {* SAT Solver\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 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.+
−
+
−
  There is the function  @{ML  PropLogic.prop_formula_of_term}, which+
−
  translates an Isabelle term into a propositional formula. Let+
−
  us illustrate this function with translating the term @{term "A \<and> \<not>A \<or> B"}. +
−
  Suppose the ML-value+
−
*}+
−
+
−
ML{*val (form, tab) = +
−
       PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}+
−
+
−
text {*+
−
  then the resulting propositional formula @{ML form} is +
−
  @{ML "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} +
−
  where indices are assigned  for the propositional 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 and the output table is+
−
+
−
  @{ML_response_fake [display,gray]+
−
  "Termtab.dest tab"+
−
  "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}+
−
+
−
  A propositional variable is also introduced whenever the translation+
−
  function cannot find an appropriate propositional formula for a term. +
−
  Given the ML-value+
−
*}+
−
+
−
ML{*val (form', tab') = +
−
       PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}+
−
+
−
text {*+
−
  @{ML form'} is now the propositional variable @{ML "BoolVar 1" in PropLogic} +
−
  and the table @{ML tab'} is+
−
+
−
  @{ML_response_fake [display,gray]+
−
  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest tab')"+
−
  "(\<forall>x. P x, 1)"}+
−
  +
−
  Having produced a propositional formula, you can call the SAT solvers +
−
  with the function @{ML "SatSolver.invoke_solver"}. +
−
  For example+
−
+
−
  @{ML_response_fake [display,gray]+
−
  "SatSolver.invoke_solver \"dpll\" form"+
−
  "SatSolver.SATISFIABLE ass"}+
−
+
−
  determines that the formula @{ML form} is satisfiable. If we inspect+
−
  the returned function @{text ass}+
−
+
−
  @{ML_response [display,gray]+
−
"let+
−
  val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form+
−
in +
−
  (ass 1, ass 2, ass 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. +
−
+
−
  If we instead invoke the SAT solver with the string @{text [quotes] "auto"}+
−
+
−
  @{ML [display,gray] "SatSolver.invoke_solver \"auto\" form"}+
−
+
−
  several external SAT solvers will be tried (if they are installed) and+
−
  the default is the internal SAT solver @{text [quotes] "dpll"}.+
−
+
−
  There are also two tactics that make use of the SAT solvers. One +
−
  is the tactic @{ML sat_tac in sat}. For example +
−
*}+
−
+
−
lemma "True"+
−
apply(tactic {* sat.sat_tac 1 *})+
−
done+
−
+
−
text {*+
−
  \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"}. Tables used in the translation function are+
−
  implemented in @{ML_file "Pure/General/table.ML"}.  +
−
  \end{readmore}+
−
*}+
−
+
−
+
−
end+
−