--- a/CookBook/Recipes/Sat.thy Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/Recipes/Sat.thy Wed Mar 18 03:03:51 2009 +0100
@@ -16,79 +16,86 @@
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
+ a result indicating that the formula is either 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
+ The function @{ML PropLogic.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
*}
-ML{*val (form, tab) =
+ML{*val (pform, table) =
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
+ then the resulting propositional formula @{ML pform} is
+
+ @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic}
+
+
+ where indices are assigned for the 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
+ input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
@{ML_response_fake [display,gray]
- "Termtab.dest tab"
+ "Termtab.dest table"
"[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
- A propositional variable is also introduced whenever the translation
+ An index is also produced whenever the translation
function cannot find an appropriate propositional formula for a term.
- Given the ML-value
+ Attempting to translate @{term "\<forall>x::nat. P x"}
*}
-ML{*val (form', tab') =
+ML{*val (pform', table') =
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
+ returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table
+ @{ML table'} is:
@{ML_response_fake [display,gray]
- "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest tab')"
+ "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
"(\<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
+ We used some pretty printing scaffolding to see better what the output is.
+
+ Having produced a propositional formula, you can now 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"}
+ "SatSolver.invoke_solver \"dpll\" pform"
+ "SatSolver.SATISFIABLE assg"}
- determines that the formula @{ML form} is satisfiable. If we inspect
- the returned function @{text ass}
+ determines that the formula @{ML pform} is satisfiable. If we inspect
+ the returned function @{text assg}
@{ML_response [display,gray]
"let
- val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form
+ val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform
in
- (ass 1, ass 2, ass 3)
+ (assg 1, assg 2, assg 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"}
+ Note that we invoked the SAT solver with the string @{text [quotes] dpll}.
+ This string specifies which SAT solver is invoked (in this case the internal
+ one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"}
- @{ML [display,gray] "SatSolver.invoke_solver \"auto\" form"}
+ @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}
- several external SAT solvers will be tried (if they are installed) and
- the default is the internal SAT solver @{text [quotes] "dpll"}.
+ several external SAT solvers will be tried (assuming they are installed).
+ If no external SAT solver is installed, then the default is
+ @{text [quotes] "dpll"}.
- There are also two tactics that make use of the SAT solvers. One
+ There are also two tactics that make use of SAT solvers. One
is the tactic @{ML sat_tac in sat}. For example
*}
@@ -97,6 +104,9 @@
done
text {*
+ However, for prove anything more exciting 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