src/HOL/Tools/sat_solver.ML
changeset 20152 b6373fe199e1
parent 20137 6c04453ac1bd
child 20441 a9034285b96b
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Jul 18 20:01:47 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Jul 19 02:35:22 2006 +0200
     1.3 @@ -554,18 +554,13 @@
     1.4  (* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
     1.5  (* that the latter is preferred by the "auto" solver                         *)
     1.6  
     1.7 -(* There are two complications that must be dealt with in the code below:    *)
     1.8 -(* 1. MiniSat introduces IDs for original clauses in the proof trace.  It    *)
     1.9 -(*    does not in general follow the convention that the original clauses    *)
    1.10 -(*    are numbered from 0 to n-1 (where n is the number of clauses in the    *)
    1.11 -(*    formula).                                                              *)
    1.12 -(* 2. MiniSat considers some problems (presumably those that can be solved   *)
    1.13 -(*    by unit propagation alone) to be "trivial" and does not provide a      *)
    1.14 -(*    proof for them.                                                        *)
    1.15 +(* There is a complication that is dealt with in the code below: MiniSat     *)
    1.16 +(* introduces IDs for original clauses in the proof trace.  It does not (in  *)
    1.17 +(* general) follow the convention that the original clauses are numbered     *)
    1.18 +(* from 0 to n-1 (where n is the number of clauses in the formula).          *)
    1.19  
    1.20  let
    1.21  	exception INVALID_PROOF of string
    1.22 -	exception TRIVIAL_PROOF of SatSolver.proof
    1.23  	fun minisat_with_proofs fm =
    1.24  	let
    1.25  		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
    1.26 @@ -577,10 +572,6 @@
    1.27  		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    1.28  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.29  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.30 -		(* since MiniSat only generates proof traces for "non-trivial" problems, *)
    1.31 -		(* an old proof trace must be deleted so that it is not mistaken as the  *)
    1.32 -		(* proof trace for this (possibly trivial) problem                       *)
    1.33 -		val _          = try File.rm proofpath
    1.34  		val cnf        = PropLogic.defcnf fm
    1.35  		val result     = SatSolver.make_external_solver cmd writefn readfn cnf
    1.36  		val _          = try File.rm inpath
    1.37 @@ -588,6 +579,9 @@
    1.38  	in  case result of
    1.39  	  SatSolver.UNSATISFIABLE NONE =>
    1.40  		(let
    1.41 +			(* string list *)
    1.42 +			val proof_lines = ((split_lines o File.read) proofpath)
    1.43 +				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
    1.44  			(* a simple representation of the CNF formula as list of clauses (paired with their ID), *)
    1.45  			(* where each clause is a sorted list of literals, where each literal is an int          *)
    1.46  			(* removes duplicates from an ordered list *)
    1.47 @@ -605,72 +599,6 @@
    1.48  			  | cnf_to_clause_list fm                         = [(remove_dups o sort int_ord o clause_to_lit_list) fm]
    1.49  			(* (int list * int) list * int *)
    1.50  			val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0
    1.51 -			(* string list *)
    1.52 -			val proof_lines = ((split_lines o File.read) proofpath)
    1.53 -				handle IO.Io _ =>
    1.54 -					(* the problem may be "trivial", i.e. provable by unit propagation only *)
    1.55 -					let
    1.56 -						val _ = tracing "Unable to read MiniSat proof file, searching for a proof by unit propagation only ..."
    1.57 -						(* int list -> bool *)
    1.58 -						fun is_empty_clause [] = true
    1.59 -						  | is_empty_clause _  = false
    1.60 -						(* int list -> bool *)
    1.61 -						fun is_unit_clause [_] = true
    1.62 -						  | is_unit_clause _   = false
    1.63 -						(* int list -> int *)
    1.64 -						fun unit_literal [l] = l
    1.65 -						  | unit_literal _   = raise INVALID_PROOF "Error during unit propagation: clause is not a unit clause."
    1.66 -						(* proof -> ... -> proof *)
    1.67 -						fun proof_by_iterated_unit_propagation (clause_table, next_id) (units_new, units, clauses_done, clauses_todo) = (
    1.68 -							case clauses_todo of
    1.69 -							  [] =>
    1.70 -								if units_new = [] then
    1.71 -									(* no further unit propagation possible -- give up *)
    1.72 -									raise INVALID_PROOF "Could not read file \"result.prf\", and no proof by unit propagation only found."
    1.73 -								else
    1.74 -									(* start over again, this time with the new unit clauses *)
    1.75 -									proof_by_iterated_unit_propagation (clause_table, next_id) ([], units_new, [], clauses_done)
    1.76 -							| (clause_lits, clause_id) :: clauses_todo' =>
    1.77 -								let
    1.78 -									(* resolve the given list of literals with all possible unit clauses, *)
    1.79 -									(* return the remaining literals and the resolvents' IDs              *)
    1.80 -									(* int list * int list -> int list * int list *)
    1.81 -									fun resolve_loop ([],      rs) = ([], rs)
    1.82 -									  | resolve_loop (l :: ls, rs) =
    1.83 -										(case AList.lookup (op =) units (~l) of
    1.84 -										  SOME unit_id => resolve_loop (ls, unit_id :: rs)
    1.85 -										| NONE         => apfst (cons l) (resolve_loop (ls, rs)))
    1.86 -									val (new_clause_lits, rs) = resolve_loop (clause_lits, [])
    1.87 -								in
    1.88 -									if rs = [] then
    1.89 -										(* no resolution possible, clause remains unchanged -- continue with the next clause *)
    1.90 -										proof_by_iterated_unit_propagation (clause_table, next_id)
    1.91 -										  (units_new, units, (clause_lits, clause_id) :: clauses_done, clauses_todo')
    1.92 -									else
    1.93 -										let
    1.94 -											(* we have a new clause -- add its derivation to the proof trace *)
    1.95 -											val new_clause_table = Inttab.update_new (next_id, clause_id :: rs) clause_table
    1.96 -											                         handle Inttab.DUP _ => raise INVALID_PROOF ("Error during unit propagation: internal clause ID " ^ Int.toString next_id ^ " already used.")
    1.97 -										in
    1.98 -											if is_empty_clause new_clause_lits then
    1.99 -												(* proof found *)
   1.100 -												(new_clause_table, next_id)
   1.101 -											else if is_unit_clause new_clause_lits then
   1.102 -												(* continue search with a new unit clause *)
   1.103 -												proof_by_iterated_unit_propagation (new_clause_table, next_id + 1)
   1.104 -												  ((unit_literal new_clause_lits, next_id + 1) :: units_new, units, (new_clause_lits, next_id + 1) :: clauses_done, clauses_todo')
   1.105 -											else
   1.106 -												(* continue search with a new clause *)
   1.107 -												proof_by_iterated_unit_propagation (new_clause_table, next_id + 1)
   1.108 -												  (units_new, units, (new_clause_lits, next_id + 1) :: clauses_done, clauses_todo')
   1.109 -										end
   1.110 -								end
   1.111 -						)
   1.112 -						val units = map (apfst unit_literal) (filter (is_unit_clause o fst) clauses)
   1.113 -						val proof = proof_by_iterated_unit_propagation (Inttab.empty, length_clauses) ([], units, [], clauses)
   1.114 -					in
   1.115 -						raise TRIVIAL_PROOF proof
   1.116 -					end  (* end of "trivial" proof search *)
   1.117  			(* string -> int *)
   1.118  			fun int_from_string s = (
   1.119  				case Int.fromString s of
   1.120 @@ -698,9 +626,7 @@
   1.121  							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   1.122  							val cid      = int_from_string id
   1.123  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.124 -							val zero     = List.last lits handle List.Empty => raise INVALID_PROOF "File format error: \"R\" not terminated by \"0\"."
   1.125 -							val ls       = sort int_ord (map int_from_string ((fst o split_last) lits))
   1.126 -							val _        = if zero = "0" then () else raise INVALID_PROOF ("File format error: \"0\" expected (" ^ quote zero ^ " encountered).")
   1.127 +							val ls       = sort int_ord (map int_from_string lits)
   1.128  							val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
   1.129  							               (* so testing for equality should suffice -- barring duplicate literals    *)
   1.130  							               case AList.lookup (op =) clauses ls of
   1.131 @@ -722,13 +648,11 @@
   1.132  							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   1.133  							val cid      = int_from_string id
   1.134  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.135 -							val dot      = List.last ids handle List.Empty => raise INVALID_PROOF "File format error: \"C\" not terminated by \".\"."
   1.136  							(* ignore the pivot literals in MiniSat's trace *)
   1.137  							fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
   1.138  							  | unevens (x :: [])      = x :: []
   1.139  							  | unevens (x :: _ :: xs) = x :: unevens xs
   1.140 -							val rs       = (map sat_to_proof o unevens o map int_from_string o fst o split_last) ids
   1.141 -							val _        = if dot = "." then () else raise INVALID_PROOF ("File format error: \".\" expected (" ^ quote dot ^ " encountered).")
   1.142 +							val rs       = (map sat_to_proof o unevens o map int_from_string) ids
   1.143  							(* extend the mapping of clause IDs with this newly defined ID *)
   1.144  							val proof_id = inc next_id
   1.145  							val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   1.146 @@ -777,8 +701,7 @@
   1.147  			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.148  		in
   1.149  			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
   1.150 -		end handle TRIVIAL_PROOF proof => SatSolver.UNSATISFIABLE (SOME proof)
   1.151 -		         | INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   1.152 +		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   1.153  	| result =>
   1.154  		result
   1.155  	end