equal
deleted
inserted
replaced
1 |
1 |
2 theory Sat |
2 theory Sat |
3 imports Main "../Base" |
3 imports Main "../Base" |
4 begin |
4 begin |
5 |
5 |
6 section {* SAT Solver\label{rec:sat} *} |
6 section {* SAT Solvers\label{rec:sat} *} |
7 |
7 |
8 text {* |
8 text {* |
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 |
99 text {* |
99 text {* |
100 \begin{readmore} |
100 \begin{readmore} |
101 The interface for the external SAT solvers is implemented |
101 The interface for the external SAT solvers is implemented |
102 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
102 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 |
103 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 |
104 implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning |
105 propositional formulas are implemented in @{ML_file |
105 propositional formulas are implemented in @{ML_file |
106 "HOL/Tools/prop_logic.ML"}. Tables used in the translation function are |
106 "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are |
107 implemented in @{ML_file "Pure/General/table.ML"}. |
107 implemented in @{ML_file "Pure/General/table.ML"}. |
108 \end{readmore} |
108 \end{readmore} |
109 *} |
109 *} |
110 |
110 |
111 |
111 |