--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/Sat.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,122 @@
+
+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)"}
+  
+  We used some pretty printing scaffolding to see better what the output is.
+ 
+  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 1 *})
+done
+
+text {*
+  However, for proving anything more exciting 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
\ No newline at end of file