95 several external SAT solvers will be tried (assuming they are installed). |
95 several external SAT solvers will be tried (assuming they are installed). |
96 If no external SAT solver is installed, then the default is |
96 If no external SAT solver is installed, then the default is |
97 @{text [quotes] "dpll"}. |
97 @{text [quotes] "dpll"}. |
98 |
98 |
99 There are also two tactics that make use of SAT solvers. One |
99 There are also two tactics that make use of SAT solvers. One |
100 is the tactic @{ML sat_tac in sat}. For example |
100 is the tactic @{ML sat_tac in SAT}. For example |
101 *} |
101 *} |
102 |
102 |
103 lemma "True" |
103 lemma "True" |
104 apply(tactic {* sat.sat_tac @{context} 1 *}) |
104 apply(tactic {* SAT.sat_tac @{context} 1 *}) |
105 done |
105 done |
106 |
106 |
107 text {* |
107 text {* |
108 However, for proving anything more exciting using @{ML "sat_tac" in sat} you |
108 However, for proving anything more exciting using @{ML "sat_tac" in SAT} you |
109 have to use a SAT solver that can produce a proof. The internal |
109 have to use a SAT solver that can produce a proof. The internal |
110 one is not usuable for this. |
110 one is not usuable for this. |
111 |
111 |
112 \begin{readmore} |
112 \begin{readmore} |
113 The interface for the external SAT solvers is implemented |
113 The interface for the external SAT solvers is implemented |
114 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
114 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
115 SAT solver based on the DPLL algorithm. The tactics for SAT solvers are |
115 SAT solver based on the DPLL algorithm. The tactics for SAT solvers are |
116 implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning |
116 implemented in @{ML_file "HOL/Tools/sat.ML"}. Functions concerning |
117 propositional formulas are implemented in @{ML_file |
117 propositional formulas are implemented in @{ML_file |
118 "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are |
118 "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are |
119 implemented in @{ML_file "Pure/General/table.ML"}. |
119 implemented in @{ML_file "Pure/General/table.ML"}. |
120 \end{readmore} |
120 \end{readmore} |
121 *} |
121 *} |