# HG changeset patch # User webertj # Date 1078946898 -3600 # Node ID 3397a69dfa4e5bed0f276f0a7ca8d9bbbe0295c3 # Parent c24d90dbf0c9d8328ae47a6d4fba9a4ac56719e8 Internal and external SAT solvers diff -r c24d90dbf0c9 -r 3397a69dfa4e src/HOL/Tools/sat_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/sat_solver.ML Wed Mar 10 20:28:18 2004 +0100 @@ -0,0 +1,439 @@ +(* Title: HOL/Tools/sat_solver.ML + ID: $Id$ + Author: Tjark Weber + Copyright 2004 + +Interface to external SAT solvers, and (simple) built-in SAT solvers. +*) + +signature SAT_SOLVER = +sig + type solver (* PropLogic.prop_formula -> (int -> bool) option *) + + (* external SAT solvers *) + val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit + val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit + val parse_std_result_file : Path.T -> string -> (int -> bool) option + val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option) -> solver + + (* generic interface *) + val solvers : (solver Symtab.table) ref + val add_solver : string * solver -> unit (* exception DUP *) + val invoke_solver : string -> solver (* exception OPTION *) + val preferred : string ref +end; + +structure SatSolver : SAT_SOLVER = +struct + + open PropLogic; + +(* ------------------------------------------------------------------------- *) +(* Type of SAT solvers: given a propositional formula, a satisfying *) +(* assignment may be returned *) +(* ------------------------------------------------------------------------- *) + + type solver = prop_formula -> (int -> bool) option; + +(* ------------------------------------------------------------------------- *) +(* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) +(* to a file in DIMACS CNF format (see "Satisfiability Suggested *) +(* Format", May 8 1993, Section 2.1) *) +(* Note: 'fm' must not contain a variable index less than 1. *) +(* Note: 'fm' is converted into (definitional) CNF. *) +(* ------------------------------------------------------------------------- *) + + (* Path.T -> prop_formula -> unit *) + + fun write_dimacs_cnf_file path fm = + let + (* prop_formula -> prop_formula *) + fun cnf_True_False_elim True = + Or (BoolVar 1, Not (BoolVar 1)) + | cnf_True_False_elim False = + And (BoolVar 1, Not (BoolVar 1)) + | cnf_True_False_elim fm = + fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) + (* prop_formula -> int *) + fun cnf_number_of_clauses (And (fm1,fm2)) = + (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) + | cnf_number_of_clauses _ = + 1 + (* prop_formula -> string *) + fun cnf_string True = + error "formula is not in CNF" + | cnf_string False = + error "formula is not in CNF" + | cnf_string (BoolVar i) = + (assert (i>=1) "formula contains a variable index less than 1"; + string_of_int i) + | cnf_string (Not fm) = + "-" ^ (cnf_string fm) + | cnf_string (Or (fm1,fm2)) = + (cnf_string fm1) ^ " " ^ (cnf_string fm2) + | cnf_string (And (fm1,fm2)) = + (cnf_string fm1) ^ " 0\n" ^ (cnf_string fm2) + in + File.write path + (let + val cnf = (cnf_True_False_elim o defcnf) fm (* conversion into def. CNF *) + val number_of_vars = maxidx cnf + val number_of_clauses = cnf_number_of_clauses cnf + in + "c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ + "c (c) Tjark Weber\n" ^ + "p cnf " ^ (string_of_int number_of_vars) ^ " " ^ (string_of_int number_of_clauses) ^ "\n" ^ + (cnf_string cnf) ^ "\n" + end) + end; + +(* ------------------------------------------------------------------------- *) +(* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) +(* to a file in DIMACS SAT format (see "Satisfiability Suggested *) +(* Format", May 8 1993, Section 2.2) *) +(* Note: 'fm' must not contain a variable index less than 1. *) +(* ------------------------------------------------------------------------- *) + + (* Path.T -> prop_formula -> unit *) + + fun write_dimacs_sat_file path fm = + let + (* prop_formula -> string *) + fun sat_string True = + "*()" + | sat_string False = + "+()" + | sat_string (BoolVar i) = + (assert (i>=1) "formula contains a variable index less than 1"; + string_of_int i) + | sat_string (Not fm) = + "-(" ^ (sat_string fm) ^ ")" + | sat_string (Or (fm1,fm2)) = + "+(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")" + | sat_string (And (fm1,fm2)) = + "*(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")" + in + File.write path + (let + val number_of_vars = Int.max (maxidx fm, 1) + in + "c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ + "c (c) Tjark Weber\n" ^ + "p sat " ^ (string_of_int number_of_vars) ^ "\n" ^ + "(" ^ (sat_string fm) ^ ")\n" + end) + end; + +(* ------------------------------------------------------------------------- *) +(* parse_std_result_file: scans a SAT solver's output file for a satisfying *) +(* variable assignment. Returns the assignment, or 'None' if the SAT *) +(* solver did not find one. The file format must be as follows: *) +(* ,----- *) +(* | 0 or more lines not containing 'success' *) +(* | A line containing 'success' as a substring *) +(* | A line ASSIGNMENT containing integers, separated by " " *) +(* | 0 or more lines *) +(* `----- *) +(* If variable i is contained in ASSIGNMENT, then i is interpreted as *) +(* 'true'. If ~i is contained in ASSIGNMENT, then i is interpreted as *) +(* 'false'. *) +(* ------------------------------------------------------------------------- *) + + (* Path.T -> string -> (int -> bool) option *) + + fun parse_std_result_file path success = + let + (* 'a option -> 'a Library.option *) + fun option (SOME a) = + Some a + | option NONE = + None + (* string -> int list *) + fun int_list_from_string s = + mapfilter (option o Int.fromString) (space_explode " " s) + (* int list -> int -> bool *) + fun assignment_from_list [] i = + false (* could be 'true' just as well; the SAT solver didn't provide a value for this variable *) + | assignment_from_list (x::xs) i = + if x=i then true + else if x=(~i) then false + else assignment_from_list xs i + (* string -> string -> bool *) + fun is_substring needle haystack = + let + val length1 = String.size needle + val length2 = String.size haystack + in + if length2 < length1 then + false + else if needle = String.substring (haystack, 0, length1) then + true + else is_substring needle (String.substring (haystack, 1, length2-1)) + end + (* string list -> int list option *) + fun parse_lines [] = + None + | parse_lines (line::lines) = + if is_substring success line then + (* the next line must be a list of integers *) + (Some o assignment_from_list o int_list_from_string o hd) lines + else + parse_lines lines + in + (parse_lines o split_lines o File.read) path + end; + +(* ------------------------------------------------------------------------- *) +(* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) +(* ------------------------------------------------------------------------- *) + + (* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> solver *) + + fun make_external_solver cmd writefn readfn fm = + (writefn fm; + assert ((system cmd)=0) ("system command " ^ quote cmd ^ " failed (make sure the SAT solver is installed)"); + readfn ()); + +(* ------------------------------------------------------------------------- *) +(* solvers: a (reference to a) table of all registered SAT solvers *) +(* ------------------------------------------------------------------------- *) + + val solvers = ref Symtab.empty; + +(* ------------------------------------------------------------------------- *) +(* add_solver: updates 'solvers' by adding a new solver *) +(* Note: No two solvers may have the same 'name'; otherwise exception 'DUP' *) +(* will be raised. *) +(* ------------------------------------------------------------------------- *) + + (* string * solver -> unit *) + + fun add_solver (name, new_solver) = + solvers := Symtab.update_new ((name, new_solver), !solvers); + +(* ------------------------------------------------------------------------- *) +(* invoke_solver: returns the solver associated with the given 'name' *) +(* Note: If no solver is associated with 'name', exception 'OPTION' will be *) +(* raised. *) +(* ------------------------------------------------------------------------- *) + + (* string -> solver *) + + fun invoke_solver name = + (the o Symtab.lookup) (!solvers, name); + +(* ------------------------------------------------------------------------- *) +(* preferred: the name of the preferred SAT solver *) +(* ------------------------------------------------------------------------- *) + + val preferred = ref ""; + +end; (* SatSolver *) + + +(* ------------------------------------------------------------------------- *) +(* Predefined SAT solvers *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* Internal SAT solver, available as 'SatSolver.solve "enumerate"' -- simply *) +(* enumerates assignments until a satisfying assignment is found *) +(* ------------------------------------------------------------------------- *) + +let + fun enum_solver fm = + let + (* int list *) + val indices = PropLogic.indices fm + (* int list -> int list -> int list option *) + (* 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) + (* int list -> int -> bool *) + fun assignment_from_list xs i = + i mem xs + (* int list -> (int -> bool) option *) + fun solver_loop xs = + if PropLogic.eval (assignment_from_list xs) fm then + Some (assignment_from_list xs) + else + (case next_list xs indices of + Some xs' => solver_loop xs' + | None => 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.solve "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 PropLogic + in + fun dpll_solver fm = + let + (* prop_formula *) + val defcnf = PropLogic.defcnf fm + (* int list *) + val indices = PropLogic.indices defcnf + (* int list -> int -> prop_formula *) + 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 + (* int list -> prop_formula -> prop_formula *) + 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) + (* prop_formula -> int list *) + fun forced_vars True = [] + | forced_vars False = [] + | forced_vars (BoolVar i) = [i] + | forced_vars (Not (BoolVar i)) = [~i] + | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) + | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (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 _ = raise ERROR (* formula is not in negation normal form *) + (* int list -> prop_formula -> (int list * prop_formula) *) + 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 + (* int list -> int option *) + fun fresh_var xs = + Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices + (* int list -> prop_formula -> int list option *) + (* 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 + (* int list -> int -> bool *) + fun assignment_from_list [] i = + false (* could be 'true' just as well; the DPLL procedure didn't provide a value for this variable *) + | assignment_from_list (x::xs) i = + if x=i then true + else if x=(~i) then false + else assignment_from_list xs i + in + (* initially, no variable is interpreted yet *) + apsome assignment_from_list (dpll [] defcnf) + end + end (* local *) +in + SatSolver.add_solver ("dpll", dpll_solver); + SatSolver.preferred := "dpll" +end; + +(* ------------------------------------------------------------------------- *) +(* Internal SAT solver, available as 'SatSolver.solve "auto"': uses the *) +(* preferred solver, or "dpll" if the preferred solver isn't present *) +(* ------------------------------------------------------------------------- *) + +let + fun auto_solver fm = + let + val preferred = !SatSolver.preferred + val fallback = "dpll" + in + if preferred="auto" then (* prevent infinite recursion *) + (warning ("Preferred SAT solver \"auto\": using solver " ^ quote fallback ^ " instead."); + SatSolver.invoke_solver fallback fm) + else if preferred=fallback then + (warning ("Preferred SAT solver is " ^ quote fallback ^ "; for better performance, consider using an external solver."); + SatSolver.invoke_solver fallback fm) + else + (SatSolver.invoke_solver preferred fm + handle OPTION => + (warning ("Preferred SAT solver " ^ quote preferred ^ " not installed; using solver " ^ quote fallback ^ " instead."); + SatSolver.invoke_solver fallback fm)) + end +in + SatSolver.add_solver ("auto", auto_solver) +end; + +(* ------------------------------------------------------------------------- *) +(* ZChaff, Version 2003.12.04 *) +(* ------------------------------------------------------------------------- *) + +if getenv "ZCHAFF_HOME" <> "" then + let + val inname = "isabelle.cnf" + val outname = "result" + val inpath = File.tmp_path (Path.unpack inname) + val outpath = File.tmp_path (Path.unpack outname) + val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) + fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm + fun readfn () = SatSolver.parse_std_result_file outpath "Verify Solution successful. Instance satisfiable" + fun zchaff fm = + let + val _ = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)") + val _ = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)") + val assignment = SatSolver.make_external_solver cmd writefn readfn fm + val _ = (File.rm inpath handle _ => ()) + val _ = (File.rm outpath handle _ => ()) + in + assignment + end + in + SatSolver.add_solver ("zchaff", zchaff); + SatSolver.preferred := "zchaff" + end +else + (); + +(* ------------------------------------------------------------------------- *) +(* Add code for other SAT solvers below. *) +(* ------------------------------------------------------------------------- *) + +(* +if mysolver_is_installed then + let + fun mysolver fm = ... + in + SatSolver.add_solver ("myname", mysolver); -- register the solver + SatSolver.preferred := "myname" -- make it the preferred solver (optional) + end +else + (); + +-- the solver is now available as SatSolver.invoke_solver "myname" +*)