--- a/src/HOL/Tools/sat_solver.ML Sat May 03 23:15:00 2014 +0200
+++ b/src/HOL/Tools/sat_solver.ML Sun May 04 16:17:53 2014 +0200
@@ -384,130 +384,11 @@
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *)
-(* -- simply enumerates assignments until a satisfying assignment is found *)
-(* ------------------------------------------------------------------------- *)
-
-let
- fun enum_solver fm =
- let
- val indices = Prop_Logic.indices fm
- (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
- fun next_list _ ([]:int list) =
- NONE
- | next_list [] (y::ys) =
- SOME [y]
- | next_list (x::xs) (y::ys) =
- if x=y then
- (* reset the bit, continue *)
- next_list xs ys
- else
- (* set the lowest bit that wasn't set before, keep the higher bits *)
- SOME (y::x::xs)
- fun assignment_from_list xs i =
- member (op =) xs i
- fun solver_loop xs =
- if Prop_Logic.eval (assignment_from_list xs) fm then
- SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
- else
- (case next_list xs indices of
- SOME xs' => solver_loop xs'
- | NONE => SatSolver.UNSATISFIABLE NONE)
- in
- (* start with the "first" assignment (all variables are interpreted as 'false') *)
- solver_loop []
- end
-in
- SatSolver.add_solver ("enumerate", enum_solver)
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a *)
-(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
-(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *)
-(* ------------------------------------------------------------------------- *)
-
-let
- local
- open Prop_Logic
- in
- fun dpll_solver fm =
- let
- (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *)
- (* but that sometimes leads to worse performance due to the *)
- (* introduction of additional variables. *)
- val fm' = Prop_Logic.nnf fm
- val indices = Prop_Logic.indices fm'
- fun partial_var_eval [] i = BoolVar i
- | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
- fun partial_eval xs True = True
- | partial_eval xs False = False
- | partial_eval xs (BoolVar i) = partial_var_eval xs i
- | partial_eval xs (Not fm) = SNot (partial_eval xs fm)
- | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2)
- | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
- fun forced_vars True = []
- | forced_vars False = []
- | forced_vars (BoolVar i) = [i]
- | forced_vars (Not (BoolVar i)) = [~i]
- | forced_vars (Or (fm1, fm2)) = inter (op =) (forced_vars fm1) (forced_vars fm2)
- | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1) (forced_vars fm2)
- (* Above, i *and* ~i may be forced. In this case the first occurrence takes *)
- (* precedence, and the next partial evaluation of the formula returns 'False'. *)
- | forced_vars _ = error "formula is not in negation normal form"
- fun eval_and_force xs fm =
- let
- val fm' = partial_eval xs fm
- val xs' = forced_vars fm'
- in
- if null xs' then
- (xs, fm')
- else
- eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *)
- (* the same effect as 'union_int' *)
- end
- fun fresh_var xs =
- find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
- (* partial assignment 'xs' *)
- fun dpll xs fm =
- let
- val (xs', fm') = eval_and_force xs fm
- in
- case fm' of
- True => SOME xs'
- | False => NONE
- | _ =>
- let
- val x = the (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
- in
- case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *)
- SOME xs'' => SOME xs''
- | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *)
- end
- end
- fun assignment_from_list [] i =
- NONE (* the DPLL procedure didn't provide a value for this variable *)
- | assignment_from_list (x::xs) i =
- if x=i then (SOME true)
- else if x=(~i) then (SOME false)
- else assignment_from_list xs i
- in
- (* initially, no variable is interpreted yet *)
- case dpll [] fm' of
- SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
- | NONE => SatSolver.UNSATISFIABLE NONE
- end
- end (* local *)
-in
- SatSolver.add_solver ("dpll", dpll_solver)
-end;
-
-(* ------------------------------------------------------------------------- *)
(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll_p"' -- *)
-(* a simple, slightly more efficient implementation of the DPLL algorithm *)
-(* (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean Satisfiability *)
-(* Solvers", July 2002, Fig. 2). In contrast to the other two ML solvers *)
-(* above, this solver produces proof traces. *)
+(* a simplified implementation of the conflict-driven clause-learning *)
+(* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean *)
+(* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models *)
+(* and proof traces. *)
(* ------------------------------------------------------------------------- *)
let