# HG changeset patch # User boehmes # Date 1399213073 -7200 # Node ID 691da43fbdd49e9ba1c524955cfb36bb5ab18367 # Parent 52e5bf245b2a2bc7162eeac80228f0158e400fed removed obsolete internal SAT solvers diff -r 52e5bf245b2a -r 691da43fbdd4 NEWS --- a/NEWS Sat May 03 23:15:00 2014 +0200 +++ b/NEWS Sun May 04 16:17:53 2014 +0200 @@ -351,6 +351,9 @@ * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy * New internal SAT solver "dpll_p" that produces models and proof traces. + This solver replaces the internal SAT solvers "enumerate" and "dpll". + Applications that explicitly used one of these two SAT solvers should + use "dpll_p" instead. Minor INCOMPATIBILITY. * SMT module: * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 diff -r 52e5bf245b2a -r 691da43fbdd4 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Sat May 03 23:15:00 2014 +0200 +++ b/src/HOL/Library/refute.ML Sun May 04 16:17:53 2014 +0200 @@ -1068,7 +1068,7 @@ val fm_ax = Prop_Logic.all (map toTrue (tl intrs)) val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u] val _ = - (if member (op =) ["dpll_p", "dpll", "enumerate"] satsolver then + (if member (op =) ["dpll_p"] satsolver then warning ("Using SAT solver " ^ quote satsolver ^ "; for better performance, consider installing an \ \external solver.") diff -r 52e5bf245b2a -r 691da43fbdd4 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat May 03 23:15:00 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sun May 04 16:17:53 2014 +0200 @@ -574,7 +574,7 @@ (* use the first ML solver (to avoid startup overhead) *) val (ml_solvers, nonml_solvers) = SatSolver.get_solvers () - |> List.partition (member (op =) ["dptsat", "dpll_p", "dpll"] o fst) + |> List.partition (member (op =) ["dptsat", "dpll_p"] o fst) val res = if null nonml_solvers then TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop diff -r 52e5bf245b2a -r 691da43fbdd4 src/HOL/Tools/sat_solver.ML --- 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 diff -r 52e5bf245b2a -r 691da43fbdd4 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Sat May 03 23:15:00 2014 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Sun May 04 16:17:53 2014 +0200 @@ -20,7 +20,7 @@ refute [expect = genuine] -- {* equivalent to 'refute 1' *} -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *} refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *} -refute [satsolver = "dpll", expect = genuine] 2 +refute [satsolver = "dpll_p", expect = genuine] 2 -- {* ... and specify a subgoal at the same time *} oops