--- a/src/HOL/Tools/sat_solver.ML Sun Jul 16 14:26:22 2006 +0200
+++ b/src/HOL/Tools/sat_solver.ML Mon Jul 17 00:37:06 2006 +0200
@@ -528,7 +528,7 @@
(if name="dpll" orelse name="enumerate" then
warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
else
- Output.debug ("Using SAT solver " ^ quote name ^ "."));
+ tracing ("Using SAT solver " ^ quote name ^ "."));
(* apply 'solver' to 'fm' *)
solver fm
handle SatSolver.NOT_CONFIGURED => loop solvers
@@ -545,6 +545,247 @@
(* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *)
(* ------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
+(* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
+(* Matthews, which can output ASCII proof traces. Replaying binary proof *)
+(* traces generated by MiniSat-p_v1.14 has _not_ been implemented. *)
+(* ------------------------------------------------------------------------- *)
+
+(* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
+(* that the latter is preferred by the "auto" solver *)
+
+(* There are two complications that must be dealt with in the code below: *)
+(* 1. MiniSat introduces IDs for original clauses in the proof trace. It *)
+(* does not in general follow the convention that the original clauses *)
+(* are numbered from 0 to n-1 (where n is the number of clauses in the *)
+(* formula). *)
+(* 2. MiniSat considers some problems (presumably those that can be solved *)
+(* by unit propagation alone) to be "trivial" and does not provide a *)
+(* proof for them. *)
+
+let
+ exception INVALID_PROOF of string
+ exception TRIVIAL_PROOF of SatSolver.proof
+ fun minisat_with_proofs fm =
+ let
+ val _ = if (getenv "MINISAT_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 proofpath = File.tmp_path (Path.unpack "result.prf")
+ val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
+ fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
+ fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ (* since MiniSat only generates proof traces for "non-trivial" problems, *)
+ (* an old proof trace must be deleted so that it is not mistaken as the *)
+ (* proof trace for this (possibly trivial) problem *)
+ val _ = try File.rm proofpath
+ val cnf = PropLogic.defcnf fm
+ val result = SatSolver.make_external_solver cmd writefn readfn cnf
+ val _ = try File.rm inpath
+ val _ = try File.rm outpath
+ in case result of
+ SatSolver.UNSATISFIABLE NONE =>
+ (let
+ (* a simple representation of the CNF formula as list of clauses (paired with their ID), *)
+ (* where each clause is a sorted list of literals, where each literal is an int *)
+ (* removes duplicates from an ordered list *)
+ (* int list -> int list *)
+ fun remove_dups [] = []
+ | remove_dups [x] = [x]
+ | remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs)
+ (* prop_formula -> int list *)
+ fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = clause_to_lit_list fm1 @ clause_to_lit_list fm2
+ | clause_to_lit_list (PropLogic.BoolVar i) = [i]
+ | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i]
+ | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula."
+ (* prop_formula -> int list list *)
+ fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2
+ | cnf_to_clause_list fm = [(remove_dups o sort int_ord o clause_to_lit_list) fm]
+ (* (int list * int) list * int *)
+ val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0
+ (* string list *)
+ val proof_lines = ((split_lines o File.read) proofpath)
+ handle IO.Io _ =>
+ (* the problem may be "trivial", i.e. provable by unit propagation only *)
+ let
+ val _ = tracing "Unable to read MiniSat proof file, searching for a proof by unit propagation only ..."
+ (* int list -> bool *)
+ fun is_empty_clause [] = true
+ | is_empty_clause _ = false
+ (* int list -> bool *)
+ fun is_unit_clause [_] = true
+ | is_unit_clause _ = false
+ (* int list -> int *)
+ fun unit_literal [l] = l
+ | unit_literal _ = raise INVALID_PROOF "Error during unit propagation: clause is not a unit clause."
+ (* proof -> ... -> proof *)
+ fun proof_by_iterated_unit_propagation (clause_table, next_id) (units_new, units, clauses_done, clauses_todo) = (
+ case clauses_todo of
+ [] =>
+ if units_new = [] then
+ (* no further unit propagation possible -- give up *)
+ raise INVALID_PROOF "Could not read file \"result.prf\", and no proof by unit propagation only found."
+ else
+ (* start over again, this time with the new unit clauses *)
+ proof_by_iterated_unit_propagation (clause_table, next_id) ([], units_new, [], clauses_done)
+ | (clause_lits, clause_id) :: clauses_todo' =>
+ let
+ (* resolve the given list of literals with all possible unit clauses, *)
+ (* return the remaining literals and the resolvents' IDs *)
+ (* int list * int list -> int list * int list *)
+ fun resolve_loop ([], rs) = ([], rs)
+ | resolve_loop (l :: ls, rs) =
+ (case AList.lookup (op =) units (~l) of
+ SOME unit_id => resolve_loop (ls, unit_id :: rs)
+ | NONE => apfst (cons l) (resolve_loop (ls, rs)))
+ val (new_clause_lits, rs) = resolve_loop (clause_lits, [])
+ in
+ if rs = [] then
+ (* no resolution possible, clause remains unchanged -- continue with the next clause *)
+ proof_by_iterated_unit_propagation (clause_table, next_id)
+ (units_new, units, (clause_lits, clause_id) :: clauses_done, clauses_todo')
+ else
+ let
+ (* we have a new clause -- add its derivation to the proof trace *)
+ val new_clause_table = Inttab.update_new (next_id, clause_id :: rs) clause_table
+ handle Inttab.DUP _ => raise INVALID_PROOF ("Error during unit propagation: internal clause ID " ^ Int.toString next_id ^ " already used.")
+ in
+ if is_empty_clause new_clause_lits then
+ (* proof found *)
+ (new_clause_table, next_id)
+ else if is_unit_clause new_clause_lits then
+ (* continue search with a new unit clause *)
+ proof_by_iterated_unit_propagation (new_clause_table, next_id + 1)
+ ((unit_literal new_clause_lits, next_id + 1) :: units_new, units, (new_clause_lits, next_id + 1) :: clauses_done, clauses_todo')
+ else
+ (* continue search with a new clause *)
+ proof_by_iterated_unit_propagation (new_clause_table, next_id + 1)
+ (units_new, units, (new_clause_lits, next_id + 1) :: clauses_done, clauses_todo')
+ end
+ end
+ )
+ val units = map (apfst unit_literal) (filter (is_unit_clause o fst) clauses)
+ val proof = proof_by_iterated_unit_propagation (Inttab.empty, length_clauses) ([], units, [], clauses)
+ in
+ raise TRIVIAL_PROOF proof
+ end (* end of "trivial" proof search *)
+ (* string -> int *)
+ fun int_from_string s = (
+ case Int.fromString s of
+ SOME i => i
+ | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
+ )
+ (* parse the proof file *)
+ (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
+ (* our proof format, where original clauses are numbered starting from 0 *)
+ val clause_id_map = ref (Inttab.empty : int Inttab.table)
+ fun sat_to_proof id = (
+ case Inttab.lookup (!clause_id_map) id of
+ SOME id' => id'
+ | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
+ )
+ val next_id = ref (length_clauses - 1)
+ (* string list -> proof -> proof *)
+ fun process_tokens [] proof =
+ proof
+ | process_tokens (tok::toks) (clause_table, empty_id) =
+ if tok="R" then (
+ case toks of
+ id::sep::lits =>
+ let
+ val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
+ val cid = int_from_string id
+ val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
+ val zero = List.last lits handle List.Empty => raise INVALID_PROOF "File format error: \"R\" not terminated by \"0\"."
+ val ls = sort int_ord (map int_from_string (butlast lits))
+ val _ = if zero = "0" then () else raise INVALID_PROOF ("File format error: \"0\" expected (" ^ quote zero ^ " encountered).")
+ val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
+ (* so testing for equality should suffice -- barring duplicate literals *)
+ case AList.lookup (op =) clauses ls of
+ SOME orig_id => orig_id
+ | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
+ (* extend the mapping of clause IDs with this newly defined ID *)
+ val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
+ handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
+ in
+ (* the proof itself doesn't change *)
+ (clause_table, empty_id)
+ end
+ | _ =>
+ raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
+ ) else if tok="C" then (
+ case toks of
+ id::sep::ids =>
+ let
+ val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
+ val cid = int_from_string id
+ val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
+ val dot = List.last ids handle List.Empty => raise INVALID_PROOF "File format error: \"C\" not terminated by \".\"."
+ (* ignore the pivot literals in MiniSat's trace *)
+ fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
+ | unevens (x :: []) = x :: []
+ | unevens (x :: _ :: xs) = x :: unevens xs
+ val rs = (map sat_to_proof o unevens o map int_from_string o butlast) ids
+ val _ = if dot = "." then () else raise INVALID_PROOF ("File format error: \".\" expected (" ^ quote dot ^ " encountered).")
+ (* extend the mapping of clause IDs with this newly defined ID *)
+ val proof_id = inc next_id
+ val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
+ handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
+ in
+ (* update clause table *)
+ (Inttab.update_new (proof_id, rs) clause_table, empty_id)
+ handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
+ end
+ | _ =>
+ raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
+ ) else if tok="D" then (
+ case toks of
+ [id] =>
+ let
+ val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
+ val _ = sat_to_proof (int_from_string id)
+ in
+ (* simply ignore "D" *)
+ (clause_table, empty_id)
+ end
+ | _ =>
+ raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
+ ) else if tok="X" then (
+ case toks of
+ [id1, id2] =>
+ let
+ val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
+ val _ = sat_to_proof (int_from_string id1)
+ val new_empty_id = sat_to_proof (int_from_string id2)
+ in
+ (* update conflict id *)
+ (clause_table, new_empty_id)
+ end
+ | _ =>
+ raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
+ ) else
+ raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
+ (* string list -> proof -> proof *)
+ fun process_lines [] proof =
+ proof
+ | process_lines (l::ls) proof =
+ process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
+ (* proof *)
+ val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
+ val _ = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
+ in
+ SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
+ end handle TRIVIAL_PROOF proof => SatSolver.UNSATISFIABLE (SOME proof)
+ | INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
+ | result =>
+ result
+ end
+in
+ SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
+end;
+
let
fun minisat fm =
let
@@ -589,7 +830,7 @@
(let
(* string list *)
val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
- handle _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
+ handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
(* PropLogic.prop_formula -> int *)
fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
| cnf_number_of_clauses _ = 1