14 a number of external SAT solvers (including ZChaff and Minisat) |
14 a number of external SAT solvers (including ZChaff and Minisat) |
15 and also contains a simple internal SAT solver that |
15 and also contains a simple internal SAT solver that |
16 is based on the DPLL algorithm.\smallskip |
16 is based on the DPLL algorithm.\smallskip |
17 |
17 |
18 The SAT solvers expect a propositional formula as input and produce |
18 The SAT solvers expect a propositional formula as input and produce |
19 a result indicating that the formula is satisfiable, unsatisfiable or |
19 a result indicating that the formula is either satisfiable, unsatisfiable or |
20 unknown. The type of the propositional formula is |
20 unknown. The type of the propositional formula is |
21 @{ML_type "PropLogic.prop_formula"} with the usual constructors such |
21 @{ML_type "PropLogic.prop_formula"} with the usual constructors such |
22 as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on. |
22 as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on. |
23 |
23 |
24 There is the function @{ML PropLogic.prop_formula_of_term}, which |
24 The function @{ML PropLogic.prop_formula_of_term} translates an Isabelle |
25 translates an Isabelle term into a propositional formula. Let |
25 term into a propositional formula. Let |
26 us illustrate this function with translating the term @{term "A \<and> \<not>A \<or> B"}. |
26 us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
27 Suppose the ML-value |
27 The function will return a propositional formula and a table. Suppose |
28 *} |
28 *} |
29 |
29 |
30 ML{*val (form, tab) = |
30 ML{*val (pform, table) = |
31 PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
31 PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
32 |
32 |
33 text {* |
33 text {* |
34 then the resulting propositional formula @{ML form} is |
34 then the resulting propositional formula @{ML pform} is |
35 @{ML "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} |
35 |
36 where indices are assigned for the propositional variables |
36 @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} |
37 @{text "A"} and @{text "B"} respectively. This assignment is recorded |
37 |
|
38 |
|
39 where indices are assigned for the variables |
|
40 @{text "A"} and @{text "B"}, respectively. This assignment is recorded |
38 in the table that is given to the translation function and also returned |
41 in the table that is given to the translation function and also returned |
39 (appropriately updated) in the result. In the case above the |
42 (appropriately updated) in the result. In the case above the |
40 input table is empty and the output table is |
43 input table is empty (i.e.~@{ML Termtab.empty}) and the output table is |
41 |
44 |
42 @{ML_response_fake [display,gray] |
45 @{ML_response_fake [display,gray] |
43 "Termtab.dest tab" |
46 "Termtab.dest table" |
44 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
47 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
45 |
48 |
46 A propositional variable is also introduced whenever the translation |
49 An index is also produced whenever the translation |
47 function cannot find an appropriate propositional formula for a term. |
50 function cannot find an appropriate propositional formula for a term. |
48 Given the ML-value |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
49 *} |
52 *} |
50 |
53 |
51 ML{*val (form', tab') = |
54 ML{*val (pform', table') = |
52 PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
55 PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
53 |
56 |
54 text {* |
57 text {* |
55 @{ML form'} is now the propositional variable @{ML "BoolVar 1" in PropLogic} |
58 returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table |
56 and the table @{ML tab'} is |
59 @{ML table'} is: |
57 |
60 |
58 @{ML_response_fake [display,gray] |
61 @{ML_response_fake [display,gray] |
59 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest tab')" |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
60 "(\<forall>x. P x, 1)"} |
63 "(\<forall>x. P x, 1)"} |
61 |
64 |
62 Having produced a propositional formula, you can call the SAT solvers |
65 We used some pretty printing scaffolding to see better what the output is. |
63 with the function @{ML "SatSolver.invoke_solver"}. |
66 |
64 For example |
67 Having produced a propositional formula, you can now call the SAT solvers |
|
68 with the function @{ML "SatSolver.invoke_solver"}. For example |
65 |
69 |
66 @{ML_response_fake [display,gray] |
70 @{ML_response_fake [display,gray] |
67 "SatSolver.invoke_solver \"dpll\" form" |
71 "SatSolver.invoke_solver \"dpll\" pform" |
68 "SatSolver.SATISFIABLE ass"} |
72 "SatSolver.SATISFIABLE assg"} |
69 |
73 |
70 determines that the formula @{ML form} is satisfiable. If we inspect |
74 determines that the formula @{ML pform} is satisfiable. If we inspect |
71 the returned function @{text ass} |
75 the returned function @{text assg} |
72 |
76 |
73 @{ML_response [display,gray] |
77 @{ML_response [display,gray] |
74 "let |
78 "let |
75 val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form |
79 val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform |
76 in |
80 in |
77 (ass 1, ass 2, ass 3) |
81 (assg 1, assg 2, assg 3) |
78 end" |
82 end" |
79 "(SOME true, SOME true, NONE)"} |
83 "(SOME true, SOME true, NONE)"} |
80 |
84 |
81 we obtain a possible assignment for the variables @{text "A"} and @{text "B"} |
85 we obtain a possible assignment for the variables @{text "A"} and @{text "B"} |
82 that makes the formula satisfiable. |
86 that makes the formula satisfiable. |
83 |
87 |
84 If we instead invoke the SAT solver with the string @{text [quotes] "auto"} |
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"} |
85 |
91 |
86 @{ML [display,gray] "SatSolver.invoke_solver \"auto\" form"} |
92 @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"} |
87 |
93 |
88 several external SAT solvers will be tried (if they are installed) and |
94 several external SAT solvers will be tried (assuming they are installed). |
89 the default is the internal SAT solver @{text [quotes] "dpll"}. |
95 If no external SAT solver is installed, then the default is |
|
96 @{text [quotes] "dpll"}. |
90 |
97 |
91 There are also two tactics that make use of the SAT solvers. One |
98 There are also two tactics that make use of SAT solvers. One |
92 is the tactic @{ML sat_tac in sat}. For example |
99 is the tactic @{ML sat_tac in sat}. For example |
93 *} |
100 *} |
94 |
101 |
95 lemma "True" |
102 lemma "True" |
96 apply(tactic {* sat.sat_tac 1 *}) |
103 apply(tactic {* sat.sat_tac 1 *}) |
97 done |
104 done |
98 |
105 |
99 text {* |
106 text {* |
|
107 However, for prove 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 |
100 \begin{readmore} |
110 \begin{readmore} |
101 The interface for the external SAT solvers is implemented |
111 The interface for the external SAT solvers is implemented |
102 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
112 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 |
113 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 |
114 implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning |