src/HOL/Tools/sat_funcs.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19553 9d15911f1893
child 19976 aa35f8e27c73
permissions -rw-r--r--
adding case theorems for code generator
     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-2006
     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           x1; ...; xn; c1; c2; ...; ck |- False
    18     (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
    19     where each clause ci is of the form
    20           ~ (l1 | l2 | ... | lm) ==> False,
    21     where each xi and each li is a literal (see also comments in cnf_funcs.ML).
    22 
    23     This does not work for goals containing schematic variables!
    24 
    25        The tactic produces a clause representation of the given goal
    26        in DIMACS format and invokes a SAT solver, which should return
    27        a proof consisting of a sequence of resolution steps, indicating
    28        the two input clauses, and resulting in new clauses, leading to
    29        the empty clause (i.e., False).  The tactic replays this proof
    30        in Isabelle and thus solves the overall goal.
    31 
    32    There are two SAT tactics available. They differ in the CNF transformation
    33    used. The "sat_tac" uses naive CNF transformation to transform the theorem
    34    to be proved before giving it to SAT solver. The naive transformation in
    35    some worst case can lead to explonential blow up in formula size.
    36    The other tactic, the "satx_tac" uses the "definitional CNF transformation"
    37    which produces formula of linear size increase compared to the input formula.
    38    This transformation introduces new variables. See also cnf_funcs.ML for
    39    more comments.
    40 
    41  Notes for the current revision:
    42    - The current version supports only zChaff prover.
    43    - The environment variable ZCHAFF_HOME must be set to point to
    44      the directory where zChaff executable resides
    45    - The environment variable ZCHAFF_VERSION must be set according to
    46      the version of zChaff used. Current supported version of zChaff:
    47      zChaff version 2004.11.15
    48    - zChaff must have been compiled with proof generation enabled
    49      (#define VERIFY_ON).
    50 *)
    51 
    52 signature SAT =
    53 sig
    54 	val trace_sat : bool ref  (* print trace messages *)
    55 	val sat_tac   : int -> Tactical.tactic
    56 	val satx_tac  : int -> Tactical.tactic
    57 	val counter   : int ref  (* number of resolution steps during last proof replay *)
    58 end
    59 
    60 functor SATFunc (structure cnf : CNF) : SAT =
    61 struct
    62 
    63 val trace_sat = ref false;
    64 
    65 val counter = ref 0;
    66 
    67 (* Thm.thm *)
    68 val resolution_thm =  (* "[| P ==> False; ~P ==> False |] ==> False" *)
    69 	let
    70 		val cterm = cterm_of (the_context ())
    71 		val Q     = Var (("Q", 0), HOLogic.boolT)
    72 		val False = HOLogic.false_const
    73 	in
    74 		Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm
    75 	end;
    76 
    77 (* ------------------------------------------------------------------------- *)
    78 (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
    79 (*      resolution over the list (starting with its head), i.e. with two raw *)
    80 (*      clauses                                                              *)
    81 (*        [| x1; ... ; a; ...; xn |] ==> False                               *)
    82 (*      and                                                                  *)
    83 (*        [| y1; ... ; a'; ...; ym |] ==> False                              *)
    84 (*      (where a and a' are dual to each other), we first convert the first  *)
    85 (*      clause to                                                            *)
    86 (*        [| x1; ...; xn |] ==> a'                                           *)
    87 (*      (using swap_prem and perhaps notnotD), and then do a resolution with *)
    88 (*      the second clause to produce                                         *)
    89 (*        [| y1; ...; x1; ...; xn; ...; yn |] ==> False                      *)
    90 (*      amd finally remove duplicate literals.                               *)
    91 (* ------------------------------------------------------------------------- *)
    92 
    93 (* Thm.thm list -> Thm.thm *)
    94 
    95 fun resolve_raw_clauses [] =
    96 	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
    97   | resolve_raw_clauses (c::cs) =
    98 	let
    99 		fun dual (Const ("Not", _) $ x) = x
   100 		  | dual x                      = HOLogic.Not $ x
   101 
   102 		fun is_neg (Const ("Not", _) $ _) = true
   103 		  | is_neg _                      = false
   104 
   105 		(* find out which two hyps are used in the resolution *)
   106 		(* Term.term list -> Term.term list -> Term.term * Term.term *)
   107 		fun res_hyps [] _ =
   108 			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   109 		  | res_hyps _ [] =
   110 			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   111 		  | res_hyps ((Const ("Trueprop", _) $ x) :: xs) ys =
   112 			let val dx = dual x in
   113 				(* hyps are implemented as ordered list in the kernel, and *)
   114 				(* stripping 'Trueprop' should not change the order        *)
   115 				if OrdList.member Term.fast_term_ord ys dx then
   116 					(x, dx)
   117 				else
   118 					res_hyps xs ys
   119 			end
   120 		  | res_hyps (_ :: xs) ys =
   121 			(* hyps are implemented as ordered list in the kernel, all hyps are of *)
   122 			(* the form 'Trueprop $ lit' or 'implies $ (negated clause) $ False',  *)
   123 			(* and the former are LESS than the latter according to the order --   *)
   124 			(* therefore there is no need to continue the search via               *)
   125 			(* 'res_hyps xs ys' here                                               *)
   126 			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   127 
   128 		(* Thm.thm -> Thm.thm -> Thm.thm *)
   129 		fun resolution c1 c2 =
   130 		let
   131 			val _ = if !trace_sat then
   132 					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1)))
   133 						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2))) ^ ")")
   134 				else ()
   135 
   136 			(* Term.term list -> Term.term list *)
   137 			fun dest_filter_Trueprop []                                  = []
   138 			  | dest_filter_Trueprop ((Const ("Trueprop", _) $ x) :: xs) = x :: dest_filter_Trueprop xs
   139 			  | dest_filter_Trueprop (_ :: xs)                           =      dest_filter_Trueprop xs
   140 
   141 			val hyps1    =                        (#hyps o rep_thm) c1
   142 			(* minor optimization: dest/filter over the second list outside 'res_hyps' to do it only once *)
   143 			val hyps2    = (dest_filter_Trueprop o #hyps o rep_thm) c2
   144 
   145 			val (l1, l2) = res_hyps hyps1 hyps2  (* the two literals used for resolution, with 'Trueprop' stripped *)
   146 			val is_neg   = is_neg l1
   147 
   148 			val c1'      = Thm.implies_intr (cterm_of (theory_of_thm c1) (HOLogic.mk_Trueprop l1)) c1  (* Gamma1 |- l1 ==> False *)
   149 			val c2'      = Thm.implies_intr (cterm_of (theory_of_thm c2) (HOLogic.mk_Trueprop l2)) c2  (* Gamma2 |- l2 ==> False *)
   150 
   151 			val res_thm  =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
   152 				let
   153 					val P          = Var (("P", 0), HOLogic.boolT)
   154 					val (lit, thy) = if is_neg then (l2, theory_of_thm c2') else (l1, theory_of_thm c1')
   155 					val cterm      = cterm_of thy
   156 				in
   157 					Thm.instantiate ([], [(cterm P, cterm lit)]) resolution_thm
   158 				end
   159 
   160 			val _ = if !trace_sat then
   161 					tracing ("Resolution theorem: " ^ string_of_thm res_thm)
   162 				else ()
   163 
   164 			val c_new    = Thm.implies_elim (Thm.implies_elim res_thm (if is_neg then c2' else c1')) (if is_neg then c1' else c2')  (* Gamma1, Gamma2 |- False *)
   165 
   166 			val _ = if !trace_sat then
   167 					tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new))) ^ ")")
   168 				else ()
   169 			val _ = inc counter
   170 		in
   171 			c_new
   172 		end
   173 	in
   174 		fold resolution cs c
   175 	end;
   176 
   177 (* ------------------------------------------------------------------------- *)
   178 (* replay_proof: replays the resolution proof returned by the SAT solver;    *)
   179 (*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
   180 (*      'clauses' array with derived clauses, and returns the derived clause *)
   181 (*      at index 'empty_id' (which should just be "False" if proof           *)
   182 (*      reconstruction was successful, with the used clauses as hyps).       *)
   183 (* ------------------------------------------------------------------------- *)
   184 
   185 (* Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *)
   186 
   187 fun replay_proof clauses (clause_table, empty_id) =
   188 let
   189 	(* int -> Thm.thm *)
   190 	fun prove_clause id =
   191 		case Array.sub (clauses, id) of
   192 		  SOME thm =>
   193 			thm
   194 		| NONE     =>
   195 			let
   196 				val _   = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   197 				val ids = valOf (Inttab.lookup clause_table id)
   198 				val thm = resolve_raw_clauses (map prove_clause ids)
   199 				val _   = Array.update (clauses, id, SOME thm)
   200 				val _   = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
   201 			in
   202 				thm
   203 			end
   204 
   205 	val _            = counter := 0
   206 	val empty_clause = prove_clause empty_id
   207 	val _            = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else ()
   208 in
   209 	empty_clause
   210 end;
   211 
   212 (* PropLogic.prop_formula -> string *)
   213 fun string_of_prop_formula PropLogic.True             = "True"
   214   | string_of_prop_formula PropLogic.False            = "False"
   215   | string_of_prop_formula (PropLogic.BoolVar i)      = "x" ^ string_of_int i
   216   | string_of_prop_formula (PropLogic.Not fm)         = "~" ^ string_of_prop_formula fm
   217   | string_of_prop_formula (PropLogic.Or (fm1, fm2))  = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   218   | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
   219 
   220 (* ------------------------------------------------------------------------- *)
   221 (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   222 (*      a proof from the resulting proof trace of the SAT solver.  Each      *)
   223 (*      premise in 'prems' that is not a clause is ignored, and the theorem  *)
   224 (*      returned is just "False" (with some clauses as hyps).                *)
   225 (* ------------------------------------------------------------------------- *)
   226 
   227 (* Thm.thm list -> Thm.thm *)
   228 
   229 fun rawsat_thm prems =
   230 let
   231 	(* remove premises that equal "True" *)
   232 	val non_triv_prems    = filter (fn thm =>
   233 		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm
   234 			handle TERM ("dest_Trueprop", _) => true) prems
   235 	(* remove non-clausal premises -- of course this shouldn't actually   *)
   236 	(* remove anything as long as 'rawsat_thm' is only called after the   *)
   237 	(* premises have been converted to clauses                            *)
   238 	val clauses           = filter (fn thm =>
   239 		((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false)
   240 		orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems
   241 	(* remove trivial clauses -- this is necessary because zChaff removes *)
   242 	(* trivial clauses during preprocessing, and otherwise our clause     *)
   243 	(* numbering would be off                                             *)
   244 	val non_triv_clauses  = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
   245 	val _                 = if !trace_sat then
   246 			tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses))
   247 		else ()
   248 	(* translate clauses from HOL terms to PropLogic.prop_formula *)
   249 	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
   250 	val _                 = if !trace_sat then
   251 			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
   252 		else ()
   253 	val fm                = PropLogic.all fms
   254 	(* unit -> Thm.thm *)
   255 	fun make_quick_and_dirty_thm () = (
   256 		if !trace_sat then
   257 			tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   258 		else ();
   259 		(* of course just returning "False" is unsound; what we should return *)
   260 		(* instead is "False" with all 'non_triv_clauses' as hyps -- but this *)
   261 		(* might be rather slow, and it makes no real difference as long as   *)
   262 		(* 'rawsat_thm' is only called from 'rawsat_tac'                      *)
   263 		SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
   264 	)
   265 in
   266 	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
   267 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
   268 		if !trace_sat then
   269 			tracing ("Proof trace from SAT solver:\n" ^
   270 				"clauses: [" ^ commas (map (fn (c, cs) =>
   271 					"(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^
   272 				"empty clause: " ^ string_of_int empty_id)
   273 		else ();
   274 		if !quick_and_dirty then
   275 			make_quick_and_dirty_thm ()
   276 		else
   277 			let
   278 				(* initialize the clause array with the given clauses, *)
   279 				(* but converted to raw clause format                  *)
   280 				val max_idx     = valOf (Inttab.max_key clause_table)
   281 				val clause_arr  = Array.array (max_idx + 1, NONE)
   282 				val raw_clauses = map cnf.clause2raw_thm non_triv_clauses
   283 				(* Every raw clause has only its literals and itself as hyp, and hyps are *)
   284 				(* accumulated during resolution steps.  Experimental results indicate    *)
   285 				(* that it is NOT faster to weaken all raw_clauses to contain every       *)
   286 				(* clause in the hyps beforehand.                                         *)
   287 				val _           = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0
   288 				(* replay the proof to derive the empty clause *)
   289 				val FalseThm    = replay_proof clause_arr (clause_table, empty_id)
   290 			in
   291 				(* convert the hyps back to the original format *)
   292 				cnf.rawhyps2clausehyps_thm FalseThm
   293 			end)
   294 	| SatSolver.UNSATISFIABLE NONE =>
   295 		if !quick_and_dirty then (
   296 			warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
   297 			make_quick_and_dirty_thm ()
   298 		) else
   299 			raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
   300 	| SatSolver.SATISFIABLE assignment =>
   301 		let
   302 			val msg = "SAT solver found a countermodel:\n"
   303 				^ (commas
   304 					o map (fn (term, idx) =>
   305 						Sign.string_of_term (the_context ()) term ^ ": "
   306 							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
   307 					(Termtab.dest atom_table)
   308 		in
   309 			raise THM (msg, 0, [])
   310 		end
   311 	| SatSolver.UNKNOWN =>
   312 		raise THM ("SAT solver failed to decide the formula", 0, [])
   313 end;
   314 
   315 (* ------------------------------------------------------------------------- *)
   316 (* Tactics                                                                   *)
   317 (* ------------------------------------------------------------------------- *)
   318 
   319 (* ------------------------------------------------------------------------- *)
   320 (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
   321 (*      should be of the form                                                *)
   322 (*        [| c1; c2; ...; ck |] ==> False                                    *)
   323 (*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
   324 (*      or "True"                                                            *)
   325 (* ------------------------------------------------------------------------- *)
   326 
   327 (* int -> Tactical.tactic *)
   328 
   329 fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i;
   330 
   331 (* ------------------------------------------------------------------------- *)
   332 (* pre_cnf_tac: converts the i-th subgoal                                    *)
   333 (*        [| A1 ; ... ; An |] ==> B                                          *)
   334 (*      to                                                                   *)
   335 (*        [| A1; ... ; An ; ~B |] ==> False                                  *)
   336 (*      (handling meta-logical connectives in B properly before negating),   *)
   337 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
   338 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
   339 (*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
   340 (*      subgoal                                                              *)
   341 (* ------------------------------------------------------------------------- *)
   342 
   343 (* int -> Tactical.tactic *)
   344 
   345 fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
   346                       PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion)));
   347 
   348 (* ------------------------------------------------------------------------- *)
   349 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
   350 (*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
   351 (*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
   352 (*      subgoal                                                              *)
   353 (* ------------------------------------------------------------------------- *)
   354 
   355 (* int -> Tactical.tactic *)
   356 
   357 fun cnfsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
   358 
   359 (* ------------------------------------------------------------------------- *)
   360 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
   361 (*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
   362 (*      CNF formula becomes a separate premise) and existential quantifiers, *)
   363 (*      then applies 'rawsat_tac' to solve the subgoal                       *)
   364 (* ------------------------------------------------------------------------- *)
   365 
   366 (* int -> Tactical.tactic *)
   367 
   368 fun cnfxsat_tac i = (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
   369 
   370 (* ------------------------------------------------------------------------- *)
   371 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
   372 (*      arbitrary formula.  The input is translated to CNF, possibly causing *)
   373 (*      an exponential blowup.                                               *)
   374 (* ------------------------------------------------------------------------- *)
   375 
   376 (* int -> Tactical.tactic *)
   377 
   378 fun sat_tac i = pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
   379 
   380 (* ------------------------------------------------------------------------- *)
   381 (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
   382 (*      arbitrary formula.  The input is translated to CNF, possibly         *)
   383 (*      introducing new literals.                                            *)
   384 (* ------------------------------------------------------------------------- *)
   385 
   386 (* int -> Tactical.tactic *)
   387 
   388 fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
   389 
   390 end;  (* of structure *)