--- a/src/HOL/Tools/sat_solver.ML Thu Jun 17 21:58:51 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Jun 17 22:01:23 2004 +0200
@@ -8,14 +8,19 @@
signature SAT_SOLVER =
sig
- type solver (* PropLogic.prop_formula -> (int -> bool) option option *)
+ exception NOT_CONFIGURED
- (* external SAT solvers *)
+ type assignment = int -> bool option
+ datatype result = SATISFIABLE of assignment
+ | UNSATISFIABLE
+ | UNKNOWN
+ type solver = PropLogic.prop_formula -> result
+
+ (* auxiliary functions to create 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)
- -> PropLogic.prop_formula -> (int -> bool) option
+ val parse_std_result_file : Path.T -> string * string * string -> result
+ val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
(* generic interface *)
val solvers : (string * solver) list ref
@@ -29,20 +34,41 @@
open PropLogic;
(* ------------------------------------------------------------------------- *)
-(* Type of SAT solvers: given a propositional formula, a satisfying *)
-(* assignment may be returned *)
-(* - 'Some None' means that no satisfying assignment was found *)
-(* - 'None' means that the solver was not configured/installed properly *)
+(* should be raised by an external SAT solver to indicate that the solver is *)
+(* not configured properly *)
+(* ------------------------------------------------------------------------- *)
+
+ exception NOT_CONFIGURED;
+
+(* ------------------------------------------------------------------------- *)
+(* type of partial (satisfying) assignments: 'a i = None' means that 'a' is *)
+(* a satisfying assigment regardless of the value of variable 'i' *)
(* ------------------------------------------------------------------------- *)
- type solver = prop_formula -> (int -> bool) option option;
+ type assignment = int -> bool option;
+
+(* ------------------------------------------------------------------------- *)
+(* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *)
+(* assignment must be returned as well *)
+(* ------------------------------------------------------------------------- *)
+
+ datatype result = SATISFIABLE of assignment
+ | UNSATISFIABLE
+ | UNKNOWN;
+
+(* ------------------------------------------------------------------------- *)
+(* type of SAT solvers: given a propositional formula, a satisfying *)
+(* assignment may be returned *)
+(* ------------------------------------------------------------------------- *)
+
+ type solver = prop_formula -> result;
(* ------------------------------------------------------------------------- *)
(* 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. *)
+(* Note: 'fm' must be given in CNF. *)
(* ------------------------------------------------------------------------- *)
(* Path.T -> prop_formula -> unit *)
@@ -70,22 +96,23 @@
(assert (i>=1) "formula contains a variable index less than 1";
string_of_int i)
| cnf_string (Not fm) =
- "-" ^ (cnf_string fm)
+ "-" ^ cnf_string fm
| cnf_string (Or (fm1,fm2)) =
- (cnf_string fm1) ^ " " ^ (cnf_string fm2)
+ cnf_string fm1 ^ " " ^ cnf_string fm2
| cnf_string (And (fm1,fm2)) =
- (cnf_string fm1) ^ " 0\n" ^ (cnf_string 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
+ val fm' = cnf_True_False_elim fm
+ val number_of_vars = maxidx fm'
+ val number_of_clauses = cnf_number_of_clauses fm'
+ val cnfstring = cnf_string fm'
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"
+ "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
+ cnfstring ^ " 0\n"
end)
end;
@@ -109,11 +136,11 @@
(assert (i>=1) "formula contains a variable index less than 1";
string_of_int i)
| sat_string (Not fm) =
- "-(" ^ (sat_string fm) ^ ")"
+ "-(" ^ sat_string fm ^ ")"
| sat_string (Or (fm1,fm2)) =
- "+(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
+ "+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
| sat_string (And (fm1,fm2)) =
- "*(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
+ "*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
in
File.write path
(let
@@ -121,29 +148,28 @@
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"
+ "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'. *)
+(* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *)
+(* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
+(* neither 'satisfiable' nor 'unsatisfiable'. Empty lines are ignored. *)
+(* The assignment must be given in one or more lines immediately after *)
+(* the line that contains 'satisfiable'. These lines must begin with *)
+(* 'assignment_prefix'. Variables must be separated by " ". Non- *)
+(* integer strings are ignored. If variable i is contained in the *)
+(* assignment, then i is interpreted as 'true'. If ~i is contained in *)
+(* the assignment, then i is interpreted as 'false'. Otherwise the *)
+(* value of i is taken to be unspecified. *)
(* ------------------------------------------------------------------------- *)
- (* Path.T -> string -> (int -> bool) option *)
+ (* Path.T -> string * string * string -> result *)
- fun parse_std_result_file path success =
+ fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
let
(* 'a option -> 'a Library.option *)
fun option (SOME a) =
@@ -153,13 +179,21 @@
(* string -> int list *)
fun int_list_from_string s =
mapfilter (option o Int.fromString) (space_explode " " s)
- (* int list -> int -> bool *)
+ (* int list -> assignment *)
fun assignment_from_list [] i =
- false (* could be 'true' just as well; the SAT solver didn't provide a value for this variable *)
+ None (* 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
+ if x=i then (Some true)
+ else if x=(~i) then (Some false)
else assignment_from_list xs i
+ (* int list -> string list -> assignment *)
+ fun parse_assignment xs [] =
+ assignment_from_list xs
+ | parse_assignment xs (line::lines) =
+ if String.isPrefix assignment_prefix line then
+ parse_assignment (xs @ int_list_from_string line) lines
+ else
+ assignment_from_list xs
(* string -> string -> bool *)
fun is_substring needle haystack =
let
@@ -172,29 +206,28 @@
true
else is_substring needle (String.substring (haystack, 1, length2-1))
end
- (* string list -> int list option *)
+ (* string list -> result *)
fun parse_lines [] =
- None
+ UNKNOWN
| 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
+ if is_substring satisfiable line then
+ SATISFIABLE (parse_assignment [] lines)
+ else if is_substring unsatisfiable line then
+ UNSATISFIABLE
else
parse_lines lines
in
- (parse_lines o split_lines o File.read) path
+ (parse_lines o (filter (fn l => l <> "")) 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) -> prop_formula -> (int -> bool) option *)
+ (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> 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 ());
+ (writefn fm; system cmd; readfn ());
(* ------------------------------------------------------------------------- *)
(* solvers: a (reference to a) table of all registered SAT solvers *)
@@ -255,20 +288,20 @@
(* int list -> int -> bool *)
fun assignment_from_list xs i =
i mem xs
- (* int list -> (int -> bool) option *)
+ (* int list -> SatSolver.result *)
fun solver_loop xs =
if PropLogic.eval (assignment_from_list xs) fm then
- Some (assignment_from_list xs)
+ SatSolver.SATISFIABLE (Some o (assignment_from_list xs))
else
(case next_list xs indices of
Some xs' => solver_loop xs'
- | None => None)
+ | None => SatSolver.UNSATISFIABLE)
in
- (* start with the "first" assignment (all variables are interpreted as 'False') *)
+ (* start with the "first" assignment (all variables are interpreted as 'false') *)
solver_loop []
end
in
- SatSolver.add_solver ("enumerate", Some o enum_solver)
+ SatSolver.add_solver ("enumerate", enum_solver)
end;
(* ------------------------------------------------------------------------- *)
@@ -283,9 +316,9 @@
in
fun dpll_solver fm =
let
- (* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
- (* sometimes introduces more boolean variables than we can handle *)
- (* efficiently. *)
+ (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
+ (* but that sometimes introduces more boolean variables than we can *)
+ (* handle efficiently. *)
val fm' = PropLogic.nnf fm
(* int list *)
val indices = PropLogic.indices fm'
@@ -342,66 +375,132 @@
| None => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *)
end
end
- (* int list -> int -> bool *)
+ (* int list -> assignment *)
fun assignment_from_list [] i =
- false (* could be 'true' just as well; the DPLL procedure didn't provide a value for this variable *)
+ None (* 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
+ 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 *)
- apsome assignment_from_list (dpll [] fm')
+ case dpll [] fm' of
+ Some assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
+ | None => SatSolver.UNSATISFIABLE
end
end (* local *)
in
- SatSolver.add_solver ("dpll", Some o dpll_solver)
+ SatSolver.add_solver ("dpll", dpll_solver)
end;
(* ------------------------------------------------------------------------- *)
(* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *)
-(* the first installed solver (other than "auto" itself) *)
+(* all installed solvers (other than "auto" itself) until one returns either *)
+(* SATISFIABLE or UNSATISFIABLE *)
(* ------------------------------------------------------------------------- *)
let
fun auto_solver fm =
- get_first (fn (name,solver) =>
+ let
+ fun loop [] =
+ SatSolver.UNKNOWN
+ | loop ((name, solver)::solvers) =
if name="auto" then
- None
+ (* do not call solver "auto" from within "auto" *)
+ loop solvers
else
- ((if name="dpll" orelse name="enumerate" then
+ (
+ (if name="dpll" orelse name="enumerate" then
warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
else
());
- solver fm)) (rev (!SatSolver.solvers))
+ (* apply 'solver' to 'fm' *)
+ (case solver fm of
+ SatSolver.SATISFIABLE a => SatSolver.SATISFIABLE a
+ | SatSolver.UNSATISFIABLE => SatSolver.UNSATISFIABLE
+ | SatSolver.UNKNOWN => loop solvers)
+ handle SatSolver.NOT_CONFIGURED => loop solvers
+ )
+ in
+ loop (rev (!SatSolver.solvers))
+ end
in
SatSolver.add_solver ("auto", auto_solver)
end;
(* ------------------------------------------------------------------------- *)
-(* ZChaff, Version 2003.12.04 *)
+(* ZChaff, Version 2003.12.04 (http://www.princeton.edu/~chaff/zchaff.html) *)
(* ------------------------------------------------------------------------- *)
let
fun zchaff fm =
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 _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
+ val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
+ val outpath = File.tmp_path (Path.unpack "result")
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 writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+ fun readfn () = SatSolver.parse_std_result_file outpath ("Verify Solution successful. Instance satisfiable", "", "Instance unsatisfiable")
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 result = SatSolver.make_external_solver cmd writefn readfn fm
val _ = (File.rm inpath handle _ => ())
val _ = (File.rm outpath handle _ => ())
in
- assignment
+ result
end
in
- SatSolver.add_solver ("zchaff", (fn fm => if getenv "ZCHAFF_HOME" <> "" then Some (zchaff fm) else None))
+ SatSolver.add_solver ("zchaff", zchaff)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *)
+(* ------------------------------------------------------------------------- *)
+
+let
+ fun berkmin fm =
+ let
+ val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
+ val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
+ val outpath = File.tmp_path (Path.unpack "result")
+ val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+ fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+ fun readfn () = SatSolver.parse_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
+ 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 result = SatSolver.make_external_solver cmd writefn readfn fm
+ val _ = (File.rm inpath handle _ => ())
+ val _ = (File.rm outpath handle _ => ())
+ in
+ result
+ end
+in
+ SatSolver.add_solver ("berkmin", berkmin)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *)
+(* ------------------------------------------------------------------------- *)
+
+let
+ fun jerusat fm =
+ let
+ val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
+ val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
+ val outpath = File.tmp_path (Path.unpack "result")
+ val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+ fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+ fun readfn () = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
+ 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 result = SatSolver.make_external_solver cmd writefn readfn fm
+ val _ = (File.rm inpath handle _ => ())
+ val _ = (File.rm outpath handle _ => ())
+ in
+ result
+ end
+in
+ SatSolver.add_solver ("jerusat", jerusat)
end;
(* ------------------------------------------------------------------------- *)
@@ -412,7 +511,7 @@
let
fun mysolver fm = ...
in
- SatSolver.add_solver ("myname", (fn fm => if mysolver_is_installed then Some (mysolver fm) else None)); -- register the solver
+ SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver
end;
-- the solver is now available as SatSolver.invoke_solver "myname"