6 section {* SAT Solver\label{rec:sat} *}

    13   {\bf Solution:} Isabelle contains a general interface for 

    14   a number of external SAT solvers (including ZChaff and Minisat)

    15   and also contains a simple internal SAT solver that

    16   is based on the DPLL algorithm.\smallskip

    17 

    18   The SAT solvers expect a propositional formula as input and produce

    19   a result indicating that the formula is satisfiable, unsatisfiable or

    20   unknown. The type of the propositional formula is  

    21   @{ML_type "PropLogic.prop_formula"} with the usual constructors such 

    22   as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on.

    23 

    24   There is the function  @{ML  PropLogic.prop_formula_of_term}, which

    25   translates an Isabelle term into a propositional formula. Let

    26   us illustrate this function with translating the term @{term "A \<and> \<not>A \<or> B"}. 

    27   Suppose the ML-value

    28 *}

    29 

    30 ML{*val (form, tab) = 

    31        PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}

    32 

    33 text {*

    34   then the resulting propositional formula @{ML form} is 

    35   @{ML "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 

    36   where indices are assigned  for the propositional variables 

    37   @{text "A"} and @{text "B"} respectively. This assignment is recorded 

    38   in the table that is given to the translation function and also returned 

    39   (appropriately updated) in the result. In the case above the

    40   input table is empty and the output table is

    41 

    42   @{ML_response_fake [display,gray]

    43   "Termtab.dest tab"

    44   "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}

    45 

    46   A propositional variable is also introduced whenever the translation

    47   function cannot find an appropriate propositional formula for a term. 

    48   Given the ML-value

    49 *}

    50 

    51 ML{*val (form', tab') = 

    52        PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}

    53 

    54 text {*

    55   @{ML form'} is now the propositional variable @{ML "BoolVar 1" in PropLogic} 

    56   and the table @{ML tab'} is

    57 

    58   @{ML_response_fake [display,gray]

    59   "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest tab')"

    60   "(\<forall>x. P x, 1)"}

    61   

    62   Having produced a propositional formula, you can call the SAT solvers 

    63   with the function @{ML "SatSolver.invoke_solver"}. 

    64   For example

    65 

    66   @{ML_response_fake [display,gray]

    67   "SatSolver.invoke_solver \"dpll\" form"

    68   "SatSolver.SATISFIABLE ass"}

    69 

    70   determines that the formula @{ML form} is satisfiable. If we inspect

    71   the returned function @{text ass}

    72 

    73   @{ML_response [display,gray]

    74 "let

    75   val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form

    76 in 

    77   (ass 1, ass 2, ass 3)

    78 end"

    79   "(SOME true, SOME true, NONE)"}

    80 

    81   we obtain a possible assignment for the variables @{text "A"} and @{text "B"}

    82   that makes the formula satisfiable. 

    83 

    84   If we instead invoke the SAT solver with the string @{text [quotes] "auto"}

    85 

    86   @{ML [display,gray] "SatSolver.invoke_solver \"auto\" form"}

    87 

    88   several external SAT solvers will be tried (if they are installed) and

    89   the default is the internal SAT solver @{text [quotes] "dpll"}.

    90 

    91   There are also two tactics that make use of the SAT solvers. One 

    92   is the tactic @{ML sat_tac in sat}. For example 

    93 *}

    94 

    95 lemma "True"

    96 apply(tactic {* sat.sat_tac 1 *})

    97 done

    98 

    99 text {*

   100   \begin{readmore} 

   101   The interface for the external SAT solvers is implemented

   102   in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple

   103   SAT solver based on the DPLL algorithm. The tactics for SAT solvers are

   104   implemented in @{ML_file "HOL/Tools/sat_funcs.ML"} Functions concerning

   105   propositional formulas are implemented in @{ML_file

   106   "HOL/Tools/prop_logic.ML"}. Tables used in the translation function are

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

   108   \end{readmore}

   109 *}