src/HOL/Tools/sat_funcs.ML
 author wenzelm Wed Feb 15 21:34:55 2006 +0100 (2006-02-15) changeset 19046 bc5c6c9b114e parent 17843 0a451f041853 child 19236 150e8b0fb991 permissions -rw-r--r--
removed distinct, renamed gen_distinct to distinct;
```     1 (*  Title:      HOL/Tools/sat_funcs.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
```
```     4     Author:     Tjark Weber
```
```     5     Copyright   2005
```
```     6
```
```     7
```
```     8 Proof reconstruction from SAT solvers.
```
```     9
```
```    10   Description:
```
```    11     This file defines several tactics to invoke a proof-producing
```
```    12     SAT solver on a propositional goal in clausal form.
```
```    13
```
```    14     We use a sequent presentation of clauses to speed up resolution
```
```    15     proof reconstruction.
```
```    16     We call such clauses "raw clauses", which are of the form
```
```    17           [| c1; c2; ...; ck |] ==> False
```
```    18     where each clause ci is of the form
```
```    19           [| l1; l2; ...; lm |] ==> False,
```
```    20     where each li is a literal (see also comments in cnf_funcs.ML).
```
```    21
```
```    22     -- Observe that this is the "dualized" version of the standard
```
```    23        clausal form
```
```    24            l1' \/ l2' \/ ... \/ lm', where li is the negation normal
```
```    25        form of ~li'.
```
```    26        The tactic produces a clause representation of the given goal
```
```    27        in DIMACS format and invokes a SAT solver, which should return
```
```    28        a proof consisting of a sequence of resolution steps, indicating
```
```    29        the two input clauses, and resulting in new clauses, leading to
```
```    30        the empty clause (i.e., False).  The tactic replays this proof
```
```    31        in Isabelle and thus solves the overall goal.
```
```    32
```
```    33    There are two SAT tactics available. They differ in the CNF transformation
```
```    34    used. The "sat_tac" uses naive CNF transformation to transform the theorem
```
```    35    to be proved before giving it to SAT solver. The naive transformation in
```
```    36    some worst case can lead to explonential blow up in formula size.
```
```    37    The other tactic, the "satx_tac" uses the "definitional CNF transformation"
```
```    38    which produces formula of linear size increase compared to the input formula.
```
```    39    This transformation introduces new variables. See also cnf_funcs.ML for
```
```    40    more comments.
```
```    41
```
```    42  Notes for the current revision:
```
```    43    - The current version supports only zChaff prover.
```
```    44    - The environment variable ZCHAFF_HOME must be set to point to
```
```    45      the directory where zChaff executable resides
```
```    46    - The environment variable ZCHAFF_VERSION must be set according to
```
```    47      the version of zChaff used. Current supported version of zChaff:
```
```    48      zChaff version 2004.11.15
```
```    49    - zChaff must have been compiled with proof generation enabled
```
```    50      (#define VERIFY_ON).
```
```    51 *)
```
```    52
```
```    53 signature SAT =
```
```    54 sig
```
```    55 	val trace_sat : bool ref  (* print trace messages *)
```
```    56 	val sat_tac   : int -> Tactical.tactic
```
```    57 	val satx_tac  : int -> Tactical.tactic
```
```    58 	val counter   : int ref  (* number of resolution steps during last proof replay *)
```
```    59 end
```
```    60
```
```    61 functor SATFunc (structure cnf : CNF) : SAT =
```
```    62 struct
```
```    63
```
```    64 val trace_sat = ref false;
```
```    65
```
```    66 val counter = ref 0;
```
```    67
```
```    68 (* ------------------------------------------------------------------------- *)
```
```    69 (* swap_prem: convert raw clauses of the form                                *)
```
```    70 (*        [| l1; l2; ...; li; ... |] ==> False                               *)
```
```    71 (*      to                                                                   *)
```
```    72 (*        [| l1; l2; ... |] ==> ~li .                                        *)
```
```    73 (*      Note that ~li may be equal to ~~a for some atom a.                   *)
```
```    74 (* ------------------------------------------------------------------------- *)
```
```    75
```
```    76 (* Thm.thm -> int -> Thm.thm *)
```
```    77
```
```    78 fun swap_prem raw_cl i =
```
```    79 	Seq.hd ((metacut_tac raw_cl 1  (* [| [| ?P; False |] ==> False; ?P ==> l1; ...; ?P ==> li; ... |] ==> ~ ?P *)
```
```    80 		THEN atac (i+1)            (* [| [| li; False |] ==> False; li ==> l1; ... |] ==> ~ li *)
```
```    81 		THEN atac 1                (* [| li ==> l1; ... |] ==> ~ li *)
```
```    82 		THEN ALLGOALS cnf.weakening_tac) notI);
```
```    83
```
```    84 (* ------------------------------------------------------------------------- *)
```
```    85 (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
```
```    86 (*      resolution over the list (starting with its head), i.e. with two raw *)
```
```    87 (*      clauses                                                              *)
```
```    88 (*        [| x1; ... ; a; ...; xn |] ==> False                               *)
```
```    89 (*      and                                                                  *)
```
```    90 (*        [| y1; ... ; a'; ...; ym |] ==> False                              *)
```
```    91 (*      (where a and a' are dual to each other), we first convert the first  *)
```
```    92 (*      clause to                                                            *)
```
```    93 (*        [| x1; ...; xn |] ==> a'                                           *)
```
```    94 (*      (using swap_prem and perhaps notnotD), and then do a resolution with *)
```
```    95 (*      the second clause to produce                                         *)
```
```    96 (*        [| y1; ...; x1; ...; xn; ...; yn |] ==> False                      *)
```
```    97 (*      amd finally remove duplicate literals.                               *)
```
```    98 (* ------------------------------------------------------------------------- *)
```
```    99
```
```   100 (* Thm.thm list -> Thm.thm *)
```
```   101
```
```   102 fun resolve_raw_clauses [] =
```
```   103 	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
```
```   104   | resolve_raw_clauses (c::cs) =
```
```   105 	let
```
```   106 		fun dual (Const ("Not", _) \$ x) = x
```
```   107 		  | dual x                      = HOLogic.Not \$ x
```
```   108
```
```   109 		fun is_neg (Const ("Not", _) \$ _) = true
```
```   110 		  | is_neg _                      = false
```
```   111
```
```   112 		(* find out which premises are used in the resolution *)
```
```   113 		(* Term.term list -> Term.term list -> int -> (int * int * bool) *)
```
```   114 		fun res_prems []      _  _    =
```
```   115 			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
```
```   116 		  | res_prems (x::xs) ys idx1 =
```
```   117 			let
```
```   118 				val x'   = HOLogic.dest_Trueprop x
```
```   119 				val idx2 = find_index_eq (dual x') ys
```
```   120 			in
```
```   121 				if idx2 = (~1) then
```
```   122 					res_prems xs ys (idx1+1)
```
```   123 				else
```
```   124 					(idx1, idx2, is_neg x')
```
```   125 			end
```
```   126
```
```   127 		(* Thm.thm -> Thm.thm -> Thm.thm *)
```
```   128 		fun resolution c1 c2 =
```
```   129 		let
```
```   130 			val _ = if !trace_sat then
```
```   131 					tracing ("Resolving clause: " ^ string_of_thm c1 ^ "\nwith clause: " ^ string_of_thm c2)
```
```   132 				else ()
```
```   133
```
```   134 			val prems2                   = map HOLogic.dest_Trueprop (prems_of c2)
```
```   135 			val (idx1, idx2, is_neg_lit) = res_prems (prems_of c1) prems2 0
```
```   136 			val swap_c1                  = swap_prem c1 (idx1+1)
```
```   137 			val swap_c1_nnf              = if is_neg_lit then Seq.hd (rtac swap_c1 1 notnotD) else swap_c1  (* deal with double-negation *)
```
```   138 			val c_new                    = Seq.hd ((rtac swap_c1_nnf (idx2+1) THEN distinct_subgoals_tac) c2)
```
```   139
```
```   140 			val _ = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm c_new) else ()
```
```   141 			val _ = inc counter
```
```   142 		in
```
```   143 			c_new
```
```   144 		end
```
```   145 	in
```
```   146 		fold resolution cs c
```
```   147 	end;
```
```   148
```
```   149 (* ------------------------------------------------------------------------- *)
```
```   150 (* replay_proof: replays the resolution proof returned by the SAT solver;    *)
```
```   151 (*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
```
```   152 (*      'clauses' array with derived clauses, and returns the derived clause *)
```
```   153 (*      at index 'empty_id' (which should just be "False" if proof           *)
```
```   154 (*      reconstruction was successful, with the used clauses as hyps).       *)
```
```   155 (* ------------------------------------------------------------------------- *)
```
```   156
```
```   157 (* Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *)
```
```   158
```
```   159 fun replay_proof clauses (clause_table, empty_id) =
```
```   160 let
```
```   161 	(* int -> Thm.thm *)
```
```   162 	fun prove_clause id =
```
```   163 		case Array.sub (clauses, id) of
```
```   164 		  SOME thm =>
```
```   165 			thm
```
```   166 		| NONE     =>
```
```   167 			let
```
```   168 				val _   = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
```
```   169 				val ids = valOf (Inttab.lookup clause_table id)
```
```   170 				val thm = resolve_raw_clauses (map prove_clause ids)
```
```   171 				val _   = Array.update (clauses, id, SOME thm)
```
```   172 				val _   = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
```
```   173 			in
```
```   174 				thm
```
```   175 			end
```
```   176
```
```   177 	val _            = counter := 0
```
```   178 	val empty_clause = prove_clause empty_id
```
```   179 	val _            = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else ()
```
```   180 in
```
```   181 	empty_clause
```
```   182 end;
```
```   183
```
```   184 (* PropLogic.prop_formula -> string *)
```
```   185 fun string_of_prop_formula PropLogic.True             = "True"
```
```   186   | string_of_prop_formula PropLogic.False            = "False"
```
```   187   | string_of_prop_formula (PropLogic.BoolVar i)      = "x" ^ string_of_int i
```
```   188   | string_of_prop_formula (PropLogic.Not fm)         = "~" ^ string_of_prop_formula fm
```
```   189   | string_of_prop_formula (PropLogic.Or (fm1, fm2))  = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
```
```   190   | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
```
```   191
```
```   192 (* ------------------------------------------------------------------------- *)
```
```   193 (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
```
```   194 (*      a proof from the resulting proof trace of the SAT solver.  Each      *)
```
```   195 (*      premise in 'prems' that is not a clause is ignored, and the theorem  *)
```
```   196 (*      returned is just "False" (with some clauses as hyps).                *)
```
```   197 (* ------------------------------------------------------------------------- *)
```
```   198
```
```   199 (* Thm.thm list -> Thm.thm *)
```
```   200
```
```   201 fun rawsat_thm prems =
```
```   202 let
```
```   203 	(* remove premises that equal "True" *)
```
```   204 	val non_triv_prems    = filter (fn thm =>
```
```   205 		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm
```
```   206 			handle TERM ("dest_Trueprop", _) => true) prems
```
```   207 	(* remove non-clausal premises -- of course this shouldn't actually   *)
```
```   208 	(* remove anything as long as 'rawsat_thm' is only called after the   *)
```
```   209 	(* premises have been converted to clauses                            *)
```
```   210 	val clauses           = filter (fn thm =>
```
```   211 		((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false)
```
```   212 		orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems
```
```   213 	(* remove trivial clauses -- this is necessary because zChaff removes *)
```
```   214 	(* trivial clauses during preprocessing, and otherwise our clause     *)
```
```   215 	(* numbering would be off                                             *)
```
```   216 	val non_triv_clauses  = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
```
```   217 	(* translate clauses from HOL terms to PropLogic.prop_formula *)
```
```   218 	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
```
```   219 	val _                 = if !trace_sat then
```
```   220 			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
```
```   221 		else ()
```
```   222 	val fm                = PropLogic.all fms
```
```   223 	(* unit -> Thm.thm *)
```
```   224 	fun make_quick_and_dirty_thm () = (
```
```   225 		if !trace_sat then
```
```   226 			tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
```
```   227 		else ();
```
```   228 		(* of course just returning "False" is unsound; what we should return *)
```
```   229 		(* instead is "False" with all 'non_triv_clauses' as hyps -- but this *)
```
```   230 		(* might be rather slow, and it makes no real difference as long as   *)
```
```   231 		(* 'rawsat_thm' is only called from 'rawsat_tac'                      *)
```
```   232 		SkipProof.make_thm (the_context ()) (HOLogic.Trueprop \$ HOLogic.false_const)
```
```   233 	)
```
```   234 in
```
```   235 	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
```
```   236 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
```
```   237 		if !trace_sat then
```
```   238 			tracing ("Proof trace from SAT solver:\n" ^
```
```   239 				"clauses: [" ^ commas (map (fn (c, cs) =>
```
```   240 					"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^
```
```   241 				"empty clause: " ^ string_of_int empty_id)
```
```   242 		else ();
```
```   243 		if !quick_and_dirty then
```
```   244 			make_quick_and_dirty_thm ()
```
```   245 		else
```
```   246 			let
```
```   247 				(* initialize the clause array with the given clauses, *)
```
```   248 				(* but converted to raw clause format                  *)
```
```   249 				val max_idx     = valOf (Inttab.max_key clause_table)
```
```   250 				val clause_arr  = Array.array (max_idx + 1, NONE)
```
```   251 				val raw_clauses = map (Seq.hd o distinct_subgoals_tac o cnf.clause2raw_thm) non_triv_clauses
```
```   252 				val _           = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0
```
```   253 			in
```
```   254 				(* replay the proof to derive the empty clause *)
```
```   255 				replay_proof clause_arr (clause_table, empty_id)
```
```   256 			end)
```
```   257 	| SatSolver.UNSATISFIABLE NONE =>
```
```   258 		if !quick_and_dirty then (
```
```   259 			warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
```
```   260 			make_quick_and_dirty_thm ()
```
```   261 		) else
```
```   262 			raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
```
```   263 	| SatSolver.SATISFIABLE assignment =>
```
```   264 		let
```
```   265 			val msg = "SAT solver found a countermodel:\n"
```
```   266 				^ (commas
```
```   267 					o map (fn (term, idx) =>
```
```   268 						Sign.string_of_term (the_context ()) term ^ ": "
```
```   269 							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
```
```   270 					(Termtab.dest atom_table)
```
```   271 		in
```
```   272 			raise THM (msg, 0, [])
```
```   273 		end
```
```   274 	| SatSolver.UNKNOWN =>
```
```   275 		raise THM ("SAT solver failed to decide the formula", 0, [])
```
```   276 end;
```
```   277
```
```   278 (* ------------------------------------------------------------------------- *)
```
```   279 (* Tactics                                                                   *)
```
```   280 (* ------------------------------------------------------------------------- *)
```
```   281
```
```   282 (* ------------------------------------------------------------------------- *)
```
```   283 (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
```
```   284 (*      should be of the form                                                *)
```
```   285 (*        [| c1; c2; ...; ck |] ==> False                                    *)
```
```   286 (*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
```
```   287 (*      or "True"                                                            *)
```
```   288 (* ------------------------------------------------------------------------- *)
```
```   289
```
```   290 (* int -> Tactical.tactic *)
```
```   291
```
```   292 fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i;
```
```   293
```
```   294 (* ------------------------------------------------------------------------- *)
```
```   295 (* pre_cnf_tac: converts the i-th subgoal                                    *)
```
```   296 (*        [| A1 ; ... ; An |] ==> B                                          *)
```
```   297 (*      to                                                                   *)
```
```   298 (*        [| A1; ... ; An ; ~B |] ==> False                                  *)
```
```   299 (*      (handling meta-logical connectives in B properly before negating),   *)
```
```   300 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
```
```   301 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
```
```   302 (*      "-->", "!", and "=")                                                 *)
```
```   303 (* ------------------------------------------------------------------------- *)
```
```   304
```
```   305 (* int -> Tactical.tactic *)
```
```   306
```
```   307 fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i;
```
```   308
```
```   309 (* ------------------------------------------------------------------------- *)
```
```   310 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
```
```   311 (*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
```
```   312 (*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
```
```   313 (*      subgoal                                                              *)
```
```   314 (* ------------------------------------------------------------------------- *)
```
```   315
```
```   316 (* int -> Tactical.tactic *)
```
```   317
```
```   318 fun cnfsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
```
```   319
```
```   320 (* ------------------------------------------------------------------------- *)
```
```   321 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
```
```   322 (*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
```
```   323 (*      CNF formula becomes a separate premise) and existential quantifiers, *)
```
```   324 (*      then applies 'rawsat_tac' to solve the subgoal                       *)
```
```   325 (* ------------------------------------------------------------------------- *)
```
```   326
```
```   327 (* int -> Tactical.tactic *)
```
```   328
```
```   329 fun cnfxsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
```
```   330
```
```   331 (* ------------------------------------------------------------------------- *)
```
```   332 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
```
```   333 (*      arbitrary formula.  The input is translated to CNF, possibly causing *)
```
```   334 (*      an exponential blowup.                                               *)
```
```   335 (* ------------------------------------------------------------------------- *)
```
```   336
```
```   337 (* int -> Tactical.tactic *)
```
```   338
```
```   339 fun sat_tac i = pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
```
```   340
```
```   341 (* ------------------------------------------------------------------------- *)
```
```   342 (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
```
```   343 (*      arbitrary formula.  The input is translated to CNF, possibly         *)
```
```   344 (*      introducing new literals.                                            *)
```
```   345 (* ------------------------------------------------------------------------- *)
```
```   346
```
```   347 (* int -> Tactical.tactic *)
```
```   348
```
```   349 fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
```
```   350
```
```   351 end;  (* of structure *)
```