# HG changeset patch # User webertj # Date 1153089426 -7200 # Node ID 5a6b33268bb6484f18d0b0d99dc91359db0a0c03 # Parent 73cb5384319019a5880a2400f7aa43eac79467b0 support for MiniSat proof traces added diff -r 73cb53843190 -r 5a6b33268bb6 src/HOL/Tools/sat_solver.ML --- 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 diff -r 73cb53843190 -r 5a6b33268bb6 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sun Jul 16 14:26:22 2006 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Mon Jul 17 00:37:06 2006 +0200 @@ -11,6 +11,7 @@ begin (* ML {* sat.solver := "zchaff_with_proofs"; *} *) +(* ML {* sat.solver := "minisat_with_proofs"; *} *) ML {* set sat.trace_sat; *} ML {* set quick_and_dirty; *}