1 |
1 |
2 theory Sat |
2 theory Sat |
3 imports "../Appendix" "../First_Steps" |
3 imports "../Appendix" "../First_Steps" |
4 begin |
4 begin |
5 |
5 |
6 section {* SAT Solvers\label{rec:sat} *} |
6 section \<open>SAT Solvers\label{rec:sat}\<close> |
7 |
7 |
8 text {* |
8 text \<open> |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 You like to use a SAT solver to find out whether |
10 You like to use a SAT solver to find out whether |
11 an Isabelle formula is satisfiable or not.\smallskip |
11 an Isabelle formula is satisfiable or not.\smallskip |
12 |
12 |
13 {\bf Solution:} Isabelle contains a general interface for |
13 {\bf Solution:} Isabelle contains a general interface for |
23 |
23 |
24 The function @{ML Prop_Logic.prop_formula_of_term} translates an Isabelle |
24 The function @{ML Prop_Logic.prop_formula_of_term} translates an Isabelle |
25 term into a propositional formula. Let |
25 term into a propositional formula. Let |
26 us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
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 |
27 The function will return a propositional formula and a table. Suppose |
28 *} |
28 \<close> |
29 |
29 |
30 ML %grayML{*val (pform, table) = |
30 ML %grayML\<open>val (pform, table) = |
31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty\<close> |
32 |
32 |
33 text {* |
33 text \<open> |
34 then the resulting propositional formula @{ML pform} is |
34 then the resulting propositional formula @{ML pform} is |
35 |
35 |
36 @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} |
36 @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} |
37 |
37 |
38 |
38 |
39 where indices are assigned for the variables |
39 where indices are assigned for the variables |
40 @{text "A"} and @{text "B"}, respectively. This assignment is recorded |
40 \<open>A\<close> and \<open>B\<close>, respectively. This assignment is recorded |
41 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 |
42 (appropriately updated) in the result. In the case above the |
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 |
43 input table is empty (i.e.~@{ML Termtab.empty}) and the output table is |
44 |
44 |
45 @{ML_response_fake [display,gray] |
45 @{ML_response_fake [display,gray] |
47 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
47 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
48 |
48 |
49 An index is also produced whenever the translation |
49 An index is also produced whenever the translation |
50 function cannot find an appropriate propositional formula for a term. |
50 function cannot find an appropriate propositional formula for a term. |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
52 *} |
52 \<close> |
53 |
53 |
54 ML %grayML{*val (pform', table') = |
54 ML %grayML\<open>val (pform', table') = |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty\<close> |
56 |
56 |
57 text {* |
57 text \<open> |
58 returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table |
58 returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table |
59 @{ML table'} is: |
59 @{ML table'} is: |
60 |
60 |
61 @{ML_response_fake [display,gray] |
61 @{ML_response_fake [display,gray] |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
69 with the function @{ML "SAT_Solver.invoke_solver"}. For example |
69 with the function @{ML "SAT_Solver.invoke_solver"}. For example |
70 |
70 |
71 @{ML_response_fake [display,gray] |
71 @{ML_response_fake [display,gray] |
72 "SAT_Solver.invoke_solver \"minisat\" pform" |
72 "SAT_Solver.invoke_solver \"minisat\" pform" |
73 "SAT_Solver.SATISFIABLE assg"} |
73 "SAT_Solver.SATISFIABLE assg"} |
74 *} |
74 \<close> |
75 |
75 |
76 text {* |
76 text \<open> |
77 determines that the formula @{ML pform} is satisfiable. If we inspect |
77 determines that the formula @{ML pform} is satisfiable. If we inspect |
78 the returned function @{text assg} |
78 the returned function \<open>assg\<close> |
79 |
79 |
80 @{ML_response [display,gray] |
80 @{ML_response [display,gray] |
81 "let |
81 "let |
82 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
82 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
83 in |
83 in |
84 (assg 1, assg 2, assg 3) |
84 (assg 1, assg 2, assg 3) |
85 end" |
85 end" |
86 "(NONE, SOME true, NONE)"} |
86 "(NONE, SOME true, NONE)"} |
87 |
87 |
88 we obtain a possible assignment for the variables @{text "A"} an @{text "B"} |
88 we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close> |
89 that makes the formula satisfiable. |
89 that makes the formula satisfiable. |
90 |
90 |
91 Note that we invoked the SAT solver with the string @{text [quotes] auto}. |
91 Note that we invoked the SAT solver with the string @{text [quotes] auto}. |
92 This string specifies which specific SAT solver is invoked. If instead |
92 This string specifies which specific SAT solver is invoked. If instead |
93 called with @{text [quotes] "auto"} |
93 called with @{text [quotes] "auto"} |
94 several external SAT solvers will be tried (assuming they are installed). |
94 several external SAT solvers will be tried (assuming they are installed). |
95 |
95 |
96 There are also two tactics that make use of SAT solvers. One |
96 There are also two tactics that make use of SAT solvers. One |
97 is the tactic @{ML sat_tac in SAT}. For example |
97 is the tactic @{ML sat_tac in SAT}. For example |
98 *} |
98 \<close> |
99 |
99 |
100 lemma "True" |
100 lemma "True" |
101 apply(tactic {* SAT.sat_tac @{context} 1 *}) |
101 apply(tactic \<open>SAT.sat_tac @{context} 1\<close>) |
102 done |
102 done |
103 |
103 |
104 text {* |
104 text \<open> |
105 However, for proving anything more exciting using @{ML "sat_tac" in SAT} you |
105 However, for proving anything more exciting using @{ML "sat_tac" in SAT} you |
106 have to use a SAT solver that can produce a proof. The internal |
106 have to use a SAT solver that can produce a proof. The internal |
107 one is not usuable for this. |
107 one is not usuable for this. |
108 |
108 |
109 \begin{readmore} |
109 \begin{readmore} |