theory Sat

imports Main "../Base"

begin

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

  propositional formulas are implemented in @{ML_file

  implemented in @{ML_file "Pure/General/table.ML"}.  

  \end{readmore}

*}

end