1 

     2 theory Sat

     3 imports Main "../Base"

     4 begin

     5 

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

     7 

     8 text {*

     9   {\bf Problem:}

    10   You like to use a SAT solver to find out whether

    11   an Isabelle formula is satisfiable or not.\smallskip

    12 

    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 either 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   The function  @{ML  PropLogic.prop_formula_of_term} translates an Isabelle 

    25   term into a propositional formula. Let

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

    27   The function will return a propositional formula and a table. Suppose 

    28 *}

    29 

    30 ML{*val (pform, table) = 

    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 pform} is 

    35   

    36   @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 

    37   

    38 

    39   where indices are assigned for the variables 

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

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

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

    43   input table is empty (i.e.~@{ML Termtab.empty}) and the output table is

    44 

    45   @{ML_response_fake [display,gray]

    46   "Termtab.dest table"

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

    48 

    49   An index is also produced whenever the translation

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

    51   Attempting to translate @{term "\<forall>x::nat. P x"}

    52 *}

    53 

    54 ML{*val (pform', table') = 

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

    56 

    57 text {*

    58   returns @{ML "BoolVar 1" in PropLogic} for  @{ML pform'} and the table 

    59   @{ML table'} is:

    60 

    61   @{ML_response_fake [display,gray]

    62   "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"

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

    64   

    65   We used some pretty printing scaffolding to see better what the output is.

    66  

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

    68   with the function @{ML "SatSolver.invoke_solver"}. For example

    69 

    70   @{ML_response_fake [display,gray]

    71   "SatSolver.invoke_solver \"dpll\" pform"

    72   "SatSolver.SATISFIABLE assg"}

    73 

    74   determines that the formula @{ML pform} is satisfiable. If we inspect

    75   the returned function @{text assg}

    76 

    77   @{ML_response [display,gray]

    78 "let

    79   val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform

    80 in 

    81   (assg 1, assg 2, assg 3)

    82 end"

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

    84 

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

    86   that makes the formula satisfiable. 

    87 

    88   Note that we invoked the SAT solver with the string @{text [quotes] dpll}. 

    89   This string specifies which SAT solver is invoked (in this case the internal

    90   one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"}

    91 

    92   @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}

    93 

    94   several external SAT solvers will be tried (assuming they are installed). 

    95   If no external SAT solver is installed, then the default is 

    96   @{text [quotes] "dpll"}.

    97 

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

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

   100 *}

   101 

   102 lemma "True"

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

   104 done

   105 

   106 text {*

   107   However, for proving anything more exciting you have to use a SAT solver

   108   that can produce a proof. The internal one is not usuable for this. 

   109 

   110   \begin{readmore} 

   111   The interface for the external SAT solvers is implemented

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

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

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

   115   propositional formulas are implemented in @{ML_file

   116   "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are

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

   118   \end{readmore}

   119 *}

   120 

   121 

   122 end