support for MiniSat proof traces added
authorwebertj
Mon Jul 17 00:37:06 2006 +0200 (2006-07-17)
changeset 201355a6b33268bb6
parent 20134 73cb53843190
child 20136 8e92a8f9720b
support for MiniSat proof traces added
src/HOL/Tools/sat_solver.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Sun Jul 16 14:26:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Mon Jul 17 00:37:06 2006 +0200
     1.3 @@ -528,7 +528,7 @@
     1.4  				(if name="dpll" orelse name="enumerate" then
     1.5  					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
     1.6  				else
     1.7 -					Output.debug ("Using SAT solver " ^ quote name ^ "."));
     1.8 +					tracing ("Using SAT solver " ^ quote name ^ "."));
     1.9  				(* apply 'solver' to 'fm' *)
    1.10  				solver fm
    1.11  					handle SatSolver.NOT_CONFIGURED => loop solvers
    1.12 @@ -545,6 +545,247 @@
    1.13  (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
    1.14  (* ------------------------------------------------------------------------- *)
    1.15  
    1.16 +(* ------------------------------------------------------------------------- *)
    1.17 +(* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
    1.18 +(* Matthews, which can output ASCII proof traces.  Replaying binary proof    *)
    1.19 +(* traces generated by MiniSat-p_v1.14 has _not_ been implemented.           *)
    1.20 +(* ------------------------------------------------------------------------- *)
    1.21 +
    1.22 +(* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
    1.23 +(* that the latter is preferred by the "auto" solver                         *)
    1.24 +
    1.25 +(* There are two complications that must be dealt with in the code below:    *)
    1.26 +(* 1. MiniSat introduces IDs for original clauses in the proof trace.  It    *)
    1.27 +(*    does not in general follow the convention that the original clauses    *)
    1.28 +(*    are numbered from 0 to n-1 (where n is the number of clauses in the    *)
    1.29 +(*    formula).                                                              *)
    1.30 +(* 2. MiniSat considers some problems (presumably those that can be solved   *)
    1.31 +(*    by unit propagation alone) to be "trivial" and does not provide a      *)
    1.32 +(*    proof for them.                                                        *)
    1.33 +
    1.34 +let
    1.35 +	exception INVALID_PROOF of string
    1.36 +	exception TRIVIAL_PROOF of SatSolver.proof
    1.37 +	fun minisat_with_proofs fm =
    1.38 +	let
    1.39 +		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.40 +		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.41 +		val outpath    = File.tmp_path (Path.unpack "result")
    1.42 +		val proofpath  = File.tmp_path (Path.unpack "result.prf")
    1.43 +		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
    1.44 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
    1.45 +		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    1.46 +		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.47 +		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.48 +		(* since MiniSat only generates proof traces for "non-trivial" problems, *)
    1.49 +		(* an old proof trace must be deleted so that it is not mistaken as the  *)
    1.50 +		(* proof trace for this (possibly trivial) problem                       *)
    1.51 +		val _          = try File.rm proofpath
    1.52 +		val cnf        = PropLogic.defcnf fm
    1.53 +		val result     = SatSolver.make_external_solver cmd writefn readfn cnf
    1.54 +		val _          = try File.rm inpath
    1.55 +		val _          = try File.rm outpath
    1.56 +	in  case result of
    1.57 +	  SatSolver.UNSATISFIABLE NONE =>
    1.58 +		(let
    1.59 +			(* a simple representation of the CNF formula as list of clauses (paired with their ID), *)
    1.60 +			(* where each clause is a sorted list of literals, where each literal is an int          *)
    1.61 +			(* removes duplicates from an ordered list *)
    1.62 +			(* int list -> int list *)
    1.63 +			fun remove_dups []             = []
    1.64 +			  | remove_dups [x]            = [x]
    1.65 +			  | remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs)
    1.66 +			(* prop_formula -> int list *)
    1.67 +			fun clause_to_lit_list (PropLogic.Or (fm1, fm2))             = clause_to_lit_list fm1 @ clause_to_lit_list fm2
    1.68 +			  | clause_to_lit_list (PropLogic.BoolVar i)                 = [i]
    1.69 +			  | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i]
    1.70 +			  | clause_to_lit_list _                 = raise INVALID_PROOF "Error: invalid clause in CNF formula."
    1.71 +			(* prop_formula -> int list list *)
    1.72 +			fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2
    1.73 +			  | cnf_to_clause_list fm                         = [(remove_dups o sort int_ord o clause_to_lit_list) fm]
    1.74 +			(* (int list * int) list * int *)
    1.75 +			val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0
    1.76 +			(* string list *)
    1.77 +			val proof_lines = ((split_lines o File.read) proofpath)
    1.78 +				handle IO.Io _ =>
    1.79 +					(* the problem may be "trivial", i.e. provable by unit propagation only *)
    1.80 +					let
    1.81 +						val _ = tracing "Unable to read MiniSat proof file, searching for a proof by unit propagation only ..."
    1.82 +						(* int list -> bool *)
    1.83 +						fun is_empty_clause [] = true
    1.84 +						  | is_empty_clause _  = false
    1.85 +						(* int list -> bool *)
    1.86 +						fun is_unit_clause [_] = true
    1.87 +						  | is_unit_clause _   = false
    1.88 +						(* int list -> int *)
    1.89 +						fun unit_literal [l] = l
    1.90 +						  | unit_literal _   = raise INVALID_PROOF "Error during unit propagation: clause is not a unit clause."
    1.91 +						(* proof -> ... -> proof *)
    1.92 +						fun proof_by_iterated_unit_propagation (clause_table, next_id) (units_new, units, clauses_done, clauses_todo) = (
    1.93 +							case clauses_todo of
    1.94 +							  [] =>
    1.95 +								if units_new = [] then
    1.96 +									(* no further unit propagation possible -- give up *)
    1.97 +									raise INVALID_PROOF "Could not read file \"result.prf\", and no proof by unit propagation only found."
    1.98 +								else
    1.99 +									(* start over again, this time with the new unit clauses *)
   1.100 +									proof_by_iterated_unit_propagation (clause_table, next_id) ([], units_new, [], clauses_done)
   1.101 +							| (clause_lits, clause_id) :: clauses_todo' =>
   1.102 +								let
   1.103 +									(* resolve the given list of literals with all possible unit clauses, *)
   1.104 +									(* return the remaining literals and the resolvents' IDs              *)
   1.105 +									(* int list * int list -> int list * int list *)
   1.106 +									fun resolve_loop ([],      rs) = ([], rs)
   1.107 +									  | resolve_loop (l :: ls, rs) =
   1.108 +										(case AList.lookup (op =) units (~l) of
   1.109 +										  SOME unit_id => resolve_loop (ls, unit_id :: rs)
   1.110 +										| NONE         => apfst (cons l) (resolve_loop (ls, rs)))
   1.111 +									val (new_clause_lits, rs) = resolve_loop (clause_lits, [])
   1.112 +								in
   1.113 +									if rs = [] then
   1.114 +										(* no resolution possible, clause remains unchanged -- continue with the next clause *)
   1.115 +										proof_by_iterated_unit_propagation (clause_table, next_id)
   1.116 +										  (units_new, units, (clause_lits, clause_id) :: clauses_done, clauses_todo')
   1.117 +									else
   1.118 +										let
   1.119 +											(* we have a new clause -- add its derivation to the proof trace *)
   1.120 +											val new_clause_table = Inttab.update_new (next_id, clause_id :: rs) clause_table
   1.121 +											                         handle Inttab.DUP _ => raise INVALID_PROOF ("Error during unit propagation: internal clause ID " ^ Int.toString next_id ^ " already used.")
   1.122 +										in
   1.123 +											if is_empty_clause new_clause_lits then
   1.124 +												(* proof found *)
   1.125 +												(new_clause_table, next_id)
   1.126 +											else if is_unit_clause new_clause_lits then
   1.127 +												(* continue search with a new unit clause *)
   1.128 +												proof_by_iterated_unit_propagation (new_clause_table, next_id + 1)
   1.129 +												  ((unit_literal new_clause_lits, next_id + 1) :: units_new, units, (new_clause_lits, next_id + 1) :: clauses_done, clauses_todo')
   1.130 +											else
   1.131 +												(* continue search with a new clause *)
   1.132 +												proof_by_iterated_unit_propagation (new_clause_table, next_id + 1)
   1.133 +												  (units_new, units, (new_clause_lits, next_id + 1) :: clauses_done, clauses_todo')
   1.134 +										end
   1.135 +								end
   1.136 +						)
   1.137 +						val units = map (apfst unit_literal) (filter (is_unit_clause o fst) clauses)
   1.138 +						val proof = proof_by_iterated_unit_propagation (Inttab.empty, length_clauses) ([], units, [], clauses)
   1.139 +					in
   1.140 +						raise TRIVIAL_PROOF proof
   1.141 +					end  (* end of "trivial" proof search *)
   1.142 +			(* string -> int *)
   1.143 +			fun int_from_string s = (
   1.144 +				case Int.fromString s of
   1.145 +				  SOME i => i
   1.146 +				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   1.147 +			)
   1.148 +			(* parse the proof file *)
   1.149 +			(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
   1.150 +			(* our proof format, where original clauses are numbered starting from 0  *)
   1.151 +			val clause_id_map = ref (Inttab.empty : int Inttab.table)
   1.152 +			fun sat_to_proof id = (
   1.153 +				case Inttab.lookup (!clause_id_map) id of
   1.154 +				  SOME id' => id'
   1.155 +				| NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
   1.156 +			)
   1.157 +			val next_id = ref (length_clauses - 1)
   1.158 +			(* string list -> proof -> proof *)
   1.159 +			fun process_tokens [] proof =
   1.160 +				proof
   1.161 +			  | process_tokens (tok::toks) (clause_table, empty_id) =
   1.162 +				if tok="R" then (
   1.163 +					case toks of
   1.164 +					  id::sep::lits =>
   1.165 +						let
   1.166 +							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   1.167 +							val cid      = int_from_string id
   1.168 +							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.169 +							val zero     = List.last lits handle List.Empty => raise INVALID_PROOF "File format error: \"R\" not terminated by \"0\"."
   1.170 +							val ls       = sort int_ord (map int_from_string (butlast lits))
   1.171 +							val _        = if zero = "0" then () else raise INVALID_PROOF ("File format error: \"0\" expected (" ^ quote zero ^ " encountered).")
   1.172 +							val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
   1.173 +							               (* so testing for equality should suffice -- barring duplicate literals    *)
   1.174 +							               case AList.lookup (op =) clauses ls of
   1.175 +							                 SOME orig_id => orig_id
   1.176 +						                   | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   1.177 +							(* extend the mapping of clause IDs with this newly defined ID *)
   1.178 +							val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   1.179 +							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   1.180 +						in
   1.181 +							(* the proof itself doesn't change *)
   1.182 +							(clause_table, empty_id)
   1.183 +						end
   1.184 +					| _ =>
   1.185 +						raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
   1.186 +				) else if tok="C" then (
   1.187 +					case toks of
   1.188 +					  id::sep::ids =>
   1.189 +						let
   1.190 +							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   1.191 +							val cid      = int_from_string id
   1.192 +							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.193 +							val dot      = List.last ids handle List.Empty => raise INVALID_PROOF "File format error: \"C\" not terminated by \".\"."
   1.194 +							(* ignore the pivot literals in MiniSat's trace *)
   1.195 +							fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
   1.196 +							  | unevens (x :: [])      = x :: []
   1.197 +							  | unevens (x :: _ :: xs) = x :: unevens xs
   1.198 +							val rs       = (map sat_to_proof o unevens o map int_from_string o butlast) ids
   1.199 +							val _        = if dot = "." then () else raise INVALID_PROOF ("File format error: \".\" expected (" ^ quote dot ^ " encountered).")
   1.200 +							(* extend the mapping of clause IDs with this newly defined ID *)
   1.201 +							val proof_id = inc next_id
   1.202 +							val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   1.203 +							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   1.204 +						in
   1.205 +							(* update clause table *)
   1.206 +							(Inttab.update_new (proof_id, rs) clause_table, empty_id)
   1.207 +								handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
   1.208 +						end
   1.209 +					| _ =>
   1.210 +						raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
   1.211 +				) else if tok="D" then (
   1.212 +					case toks of
   1.213 +					  [id] =>
   1.214 +						let
   1.215 +							val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   1.216 +							val _ = sat_to_proof (int_from_string id)
   1.217 +						in
   1.218 +							(* simply ignore "D" *)
   1.219 +							(clause_table, empty_id)
   1.220 +						end
   1.221 +					| _ =>
   1.222 +						raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
   1.223 +				) else if tok="X" then (
   1.224 +					case toks of
   1.225 +					  [id1, id2] =>
   1.226 +						let
   1.227 +							val _            = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   1.228 +							val _            = sat_to_proof (int_from_string id1)
   1.229 +							val new_empty_id = sat_to_proof (int_from_string id2)
   1.230 +						in
   1.231 +							(* update conflict id *)
   1.232 +							(clause_table, new_empty_id)
   1.233 +						end
   1.234 +					| _ =>
   1.235 +						raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
   1.236 +				) else
   1.237 +					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   1.238 +			(* string list -> proof -> proof *)
   1.239 +			fun process_lines [] proof =
   1.240 +				proof
   1.241 +			  | process_lines (l::ls) proof =
   1.242 +				process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
   1.243 +			(* proof *)
   1.244 +			val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
   1.245 +			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.246 +		in
   1.247 +			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
   1.248 +		end handle TRIVIAL_PROOF proof => SatSolver.UNSATISFIABLE (SOME proof)
   1.249 +		         | INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   1.250 +	| result =>
   1.251 +		result
   1.252 +	end
   1.253 +in
   1.254 +	SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
   1.255 +end;
   1.256 +
   1.257  let
   1.258  	fun minisat fm =
   1.259  	let
   1.260 @@ -589,7 +830,7 @@
   1.261  		(let
   1.262  			(* string list *)
   1.263  			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
   1.264 -				handle _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   1.265 +				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   1.266  			(* PropLogic.prop_formula -> int *)
   1.267  			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   1.268  			  | cnf_number_of_clauses _                          = 1
     2.1 --- a/src/HOL/ex/SAT_Examples.thy	Sun Jul 16 14:26:22 2006 +0200
     2.2 +++ b/src/HOL/ex/SAT_Examples.thy	Mon Jul 17 00:37:06 2006 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  begin
     2.5  
     2.6  (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
     2.7 +(* ML {* sat.solver := "minisat_with_proofs"; *} *)
     2.8  ML {* set sat.trace_sat; *}
     2.9  ML {* set quick_and_dirty; *}
    2.10