64 |
64 |
65 In the print out of the tabel, we used some pretty printing scaffolding |
65 In the print out of the tabel, we used some pretty printing scaffolding |
66 to see better which assignment the table contains. |
66 to see better which assignment the table contains. |
67 |
67 |
68 Having produced a propositional formula, you can now call the SAT solvers |
68 Having produced a propositional formula, you can now call the SAT solvers |
69 with the function @{ML "SatSolver.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 "SatSolver.invoke_solver \"dpll\" pform" |
72 "SAT_Solver.invoke_solver \"minisat\" pform" |
73 "SatSolver.SATISFIABLE assg"} |
73 "SAT_Solver.SATISFIABLE assg"} |
74 |
74 |
75 determines that the formula @{ML pform} is satisfiable. If we inspect |
75 determines that the formula @{ML pform} is satisfiable. If we inspect |
76 the returned function @{text assg} |
76 the returned function @{text assg} |
77 |
77 |
78 @{ML_response [display,gray] |
78 @{ML_response [display,gray] |
79 "let |
79 "let |
80 val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform |
80 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
81 in |
81 in |
82 (assg 1, assg 2, assg 3) |
82 (assg 1, assg 2, assg 3) |
83 end" |
83 end" |
84 "(SOME true, SOME true, NONE)"} |
84 "(SOME true, SOME true, NONE)"} |
85 |
85 |
86 we obtain a possible assignment for the variables @{text "A"} and @{text "B"} |
86 we obtain a possible assignment for the variables @{text "A"} an @{text "B"} |
87 that makes the formula satisfiable. |
87 that makes the formula satisfiable. |
88 |
88 |
89 Note that we invoked the SAT solver with the string @{text [quotes] dpll}. |
89 Note that we invoked the SAT solver with the string @{text [quotes] auto}. |
90 This string specifies which SAT solver is invoked (in this case the internal |
90 This string specifies which specific SAT solver is invoked. If instead |
91 one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"} |
91 called with @{text [quotes] "auto"} |
92 |
|
93 @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"} |
|
94 |
|
95 several external SAT solvers will be tried (assuming they are installed). |
92 several external SAT solvers will be tried (assuming they are installed). |
96 If no external SAT solver is installed, then the default is |
|
97 @{text [quotes] "dpll"}. |
|
98 |
93 |
99 There are also two tactics that make use of SAT solvers. One |
94 There are also two tactics that make use of SAT solvers. One |
100 is the tactic @{ML sat_tac in SAT}. For example |
95 is the tactic @{ML sat_tac in SAT}. For example |
101 *} |
96 *} |
102 |
97 |