--- a/CookBook/Recipes/Sat.thy	Mon Mar 16 03:02:56 2009 +0100
+++ b/CookBook/Recipes/Sat.thy	Tue Mar 17 01:56:29 2009 +0100
@@ -1,15 +1,112 @@
 
 theory Sat
-imports Main
+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}
+*}
+
 
-section {* SAT Solver *}
-
-
-
-end
-  
-
-
-
+end
\ No newline at end of file