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

  \<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:

  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