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 *)