src/HOL/Tools/sat_funcs.ML
 author wenzelm Mon Jul 27 23:17:40 2009 +0200 (2009-07-27 ago) changeset 32232 6c394343360f parent 32231 95b8afcbb0ed child 32283 3bebc195c124 permissions -rw-r--r--
proper context for SAT tactics;
eliminated METAHYPS;
tuned signatures;
```     1 (*  Title:      HOL/Tools/sat_funcs.ML
```
```     2     Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
```
```     3     Author:     Tjark Weber, TU Muenchen
```
```     4
```
```     5 Proof reconstruction from SAT solvers.
```
```     6
```
```     7   Description:
```
```     8     This file defines several tactics to invoke a proof-producing
```
```     9     SAT solver on a propositional goal in clausal form.
```
```    10
```
```    11     We use a sequent presentation of clauses to speed up resolution
```
```    12     proof reconstruction.
```
```    13     We call such clauses "raw clauses", which are of the form
```
```    14           [x1, ..., xn, P] |- False
```
```    15     (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
```
```    16     where each xi is a literal (see also comments in cnf_funcs.ML).
```
```    17
```
```    18     This does not work for goals containing schematic variables!
```
```    19
```
```    20       The tactic produces a clause representation of the given goal
```
```    21       in DIMACS format and invokes a SAT solver, which should return
```
```    22       a proof consisting of a sequence of resolution steps, indicating
```
```    23       the two input clauses, and resulting in new clauses, leading to
```
```    24       the empty clause (i.e. "False").  The tactic replays this proof
```
```    25       in Isabelle and thus solves the overall goal.
```
```    26
```
```    27   There are three SAT tactics available.  They differ in the CNF transformation
```
```    28   used. "sat_tac" uses naive CNF transformation to transform the theorem to be
```
```    29   proved before giving it to the SAT solver.  The naive transformation in the
```
```    30   worst case can lead to an exponential blow up in formula size.  Another
```
```    31   tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
```
```    32   produce a formula of linear size increase compared to the input formula, at
```
```    33   the cost of possibly introducing new variables.  See cnf_funcs.ML for more
```
```    34   comments on the CNF transformation.  "rawsat_tac" should be used with
```
```    35   caution: no CNF transformation is performed, and the tactic's behavior is
```
```    36   undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
```
```    37   where each Ci is a disjunction.
```
```    38
```
```    39   The SAT solver to be used can be set via the "solver" reference.  See
```
```    40   sat_solvers.ML for possible values, and etc/settings for required (solver-
```
```    41   dependent) configuration settings.  To replay SAT proofs in Isabelle, you
```
```    42   must of course use a proof-producing SAT solver in the first place.
```
```    43
```
```    44   Proofs are replayed only if "!quick_and_dirty" is false.  If
```
```    45   "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
```
```    46   negation to be unsatisfiable) is proved via an oracle.
```
```    47 *)
```
```    48
```
```    49 signature SAT =
```
```    50 sig
```
```    51 	val trace_sat: bool ref    (* input: print trace messages *)
```
```    52 	val solver: string ref  (* input: name of SAT solver to be used *)
```
```    53 	val counter: int ref     (* output: number of resolution steps during last proof replay *)
```
```    54 	val rawsat_thm: cterm list -> thm
```
```    55 	val rawsat_tac: Proof.context -> int -> tactic
```
```    56 	val sat_tac: Proof.context -> int -> tactic
```
```    57 	val satx_tac: Proof.context -> int -> tactic
```
```    58 end
```
```    59
```
```    60 functor SATFunc(cnf : CNF) : SAT =
```
```    61 struct
```
```    62
```
```    63 val trace_sat = ref false;
```
```    64
```
```    65 val solver = ref "zchaff_with_proofs";  (* see HOL/Tools/sat_solver.ML for possible values *)
```
```    66
```
```    67 val counter = ref 0;
```
```    68
```
```    69 val resolution_thm =
```
```    70   @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
```
```    71
```
```    72 val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
```
```    73
```
```    74 (* ------------------------------------------------------------------------- *)
```
```    75 (* lit_ord: an order on integers that considers their absolute values only,  *)
```
```    76 (*      thereby treating integers that represent the same atom (positively   *)
```
```    77 (*      or negatively) as equal                                              *)
```
```    78 (* ------------------------------------------------------------------------- *)
```
```    79
```
```    80 fun lit_ord (i, j) =
```
```    81 	int_ord (abs i, abs j);
```
```    82
```
```    83 (* ------------------------------------------------------------------------- *)
```
```    84 (* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
```
```    85 (*      distinguished:                                                       *)
```
```    86 (*      1. NO_CLAUSE: clause not proved (yet)                                *)
```
```    87 (*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
```
```    88 (*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
```
```    89 (*         (a mapping from int's to its literals) for faster proof           *)
```
```    90 (*         reconstruction                                                    *)
```
```    91 (* ------------------------------------------------------------------------- *)
```
```    92
```
```    93 datatype CLAUSE = NO_CLAUSE
```
```    94                 | ORIG_CLAUSE of Thm.thm
```
```    95                 | RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list;
```
```    96
```
```    97 (* ------------------------------------------------------------------------- *)
```
```    98 (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
```
```    99 (*      resolution over the list (starting with its head), i.e. with two raw *)
```
```   100 (*      clauses                                                              *)
```
```   101 (*        [P, x1, ..., a, ..., xn] |- False                                  *)
```
```   102 (*      and                                                                  *)
```
```   103 (*        [Q, y1, ..., a', ..., ym] |- False                                 *)
```
```   104 (*      (where a and a' are dual to each other), we convert the first clause *)
```
```   105 (*      to                                                                   *)
```
```   106 (*        [P, x1, ..., xn] |- a ==> False ,                                  *)
```
```   107 (*      the second clause to                                                 *)
```
```   108 (*        [Q, y1, ..., ym] |- a' ==> False                                   *)
```
```   109 (*      and then perform resolution with                                     *)
```
```   110 (*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
```
```   111 (*      to produce                                                           *)
```
```   112 (*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
```
```   113 (*      Each clause is accompanied with an association list mapping integers *)
```
```   114 (*      (positive for positive literals, negative for negative literals, and *)
```
```   115 (*      the same absolute value for dual literals) to the actual literals as *)
```
```   116 (*      cterms.                                                              *)
```
```   117 (* ------------------------------------------------------------------------- *)
```
```   118
```
```   119 (* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
```
```   120
```
```   121 fun resolve_raw_clauses [] =
```
```   122       raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
```
```   123   | resolve_raw_clauses (c::cs) =
```
```   124 	let
```
```   125 		(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
```
```   126 		fun merge xs      []      = xs
```
```   127 		  | merge []      ys      = ys
```
```   128 		  | merge (x::xs) (y::ys) =
```
```   129 			(case (lit_ord o pairself fst) (x, y) of
```
```   130 			  LESS    => x :: merge xs (y::ys)
```
```   131 			| EQUAL   => x :: merge xs ys
```
```   132 			| GREATER => y :: merge (x::xs) ys)
```
```   133
```
```   134 		(* find out which two hyps are used in the resolution *)
```
```   135 		(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
```
```   136 		fun find_res_hyps ([], _) _ =
```
```   137           raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
```
```   138 		  | find_res_hyps (_, []) _ =
```
```   139           raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
```
```   140 		  | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
```
```   141 			(case (lit_ord o pairself fst) (h1, h2) of
```
```   142 			  LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
```
```   143 			| EQUAL => let
```
```   144 				val (i1, chyp1) = h1
```
```   145 				val (i2, chyp2) = h2
```
```   146 			in
```
```   147 				if i1 = ~ i2 then
```
```   148 					(i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
```
```   149 				else (* i1 = i2 *)
```
```   150 					find_res_hyps (hyps1, hyps2) (h1 :: acc)
```
```   151 			end
```
```   152 			| GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
```
```   153
```
```   154 		(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
```
```   155 		fun resolution (c1, hyps1) (c2, hyps2) =
```
```   156 		let
```
```   157 			val _ =
```
```   158 			  if ! trace_sat then
```
```   159 					tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
```
```   160 					  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
```
```   161 						^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
```
```   162 						" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
```
```   163 				else ()
```
```   164
```
```   165 			(* the two literals used for resolution *)
```
```   166 			val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
```
```   167
```
```   168 			val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
```
```   169 			val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
```
```   170
```
```   171 			val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
```
```   172 				let
```
```   173 					val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
```
```   174 				in
```
```   175 					Thm.instantiate ([], [(cP, cLit)]) resolution_thm
```
```   176 				end
```
```   177
```
```   178 			val _ =
```
```   179 			  if !trace_sat then
```
```   180 					tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
```
```   181 				else ()
```
```   182
```
```   183 			(* Gamma1, Gamma2 |- False *)
```
```   184 			val c_new = Thm.implies_elim
```
```   185 				(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
```
```   186 				(if hyp1_is_neg then c1' else c2')
```
```   187
```
```   188 			val _ =
```
```   189 			  if !trace_sat then
```
```   190 					tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
```
```   191 					  " (hyps: " ^ ML_Syntax.print_list
```
```   192 					      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
```
```   193 				else ()
```
```   194 			val _ = inc counter
```
```   195 		in
```
```   196 			(c_new, new_hyps)
```
```   197 		end
```
```   198 	in
```
```   199 		fold resolution cs c
```
```   200 	end;
```
```   201
```
```   202 (* ------------------------------------------------------------------------- *)
```
```   203 (* replay_proof: replays the resolution proof returned by the SAT solver;    *)
```
```   204 (*      cf. SatSolver.proof for details of the proof format.  Updates the    *)
```
```   205 (*      'clauses' array with derived clauses, and returns the derived clause *)
```
```   206 (*      at index 'empty_id' (which should just be "False" if proof           *)
```
```   207 (*      reconstruction was successful, with the used clauses as hyps).       *)
```
```   208 (*      'atom_table' must contain an injective mapping from all atoms that   *)
```
```   209 (*      occur (as part of a literal) in 'clauses' to positive integers.      *)
```
```   210 (* ------------------------------------------------------------------------- *)
```
```   211
```
```   212 (* int Termtab.table -> CLAUSE Array.array -> SatSolver.proof -> Thm.thm *)
```
```   213
```
```   214 fun replay_proof atom_table clauses (clause_table, empty_id) =
```
```   215 let
```
```   216 	(* Thm.cterm -> int option *)
```
```   217 	fun index_of_literal chyp = (
```
```   218 		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
```
```   219 		  (Const ("Not", _) \$ atom) =>
```
```   220 			SOME (~(valOf (Termtab.lookup atom_table atom)))
```
```   221 		| atom =>
```
```   222 			SOME (valOf (Termtab.lookup atom_table atom))
```
```   223 	) handle TERM _ => NONE;  (* 'chyp' is not a literal *)
```
```   224
```
```   225 	(* int -> Thm.thm * (int * Thm.cterm) list *)
```
```   226 	fun prove_clause id =
```
```   227 		case Array.sub (clauses, id) of
```
```   228 		  RAW_CLAUSE clause =>
```
```   229 			clause
```
```   230 		| ORIG_CLAUSE thm =>
```
```   231 			(* convert the original clause *)
```
```   232 			let
```
```   233 				val _      = if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
```
```   234 				val raw    = cnf.clause2raw_thm thm
```
```   235 				val hyps   = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
```
```   236 					Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
```
```   237 				val clause = (raw, hyps)
```
```   238 				val _      = Array.update (clauses, id, RAW_CLAUSE clause)
```
```   239 			in
```
```   240 				clause
```
```   241 			end
```
```   242 		| NO_CLAUSE =>
```
```   243 			(* prove the clause, using information from 'clause_table' *)
```
```   244 			let
```
```   245 				val _      = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
```
```   246 				val ids    = valOf (Inttab.lookup clause_table id)
```
```   247 				val clause = resolve_raw_clauses (map prove_clause ids)
```
```   248 				val _      = Array.update (clauses, id, RAW_CLAUSE clause)
```
```   249 				val _      = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
```
```   250 			in
```
```   251 				clause
```
```   252 			end
```
```   253
```
```   254 	val _            = counter := 0
```
```   255 	val empty_clause = fst (prove_clause empty_id)
```
```   256 	val _            = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else ()
```
```   257 in
```
```   258 	empty_clause
```
```   259 end;
```
```   260
```
```   261 (* ------------------------------------------------------------------------- *)
```
```   262 (* string_of_prop_formula: return a human-readable string representation of  *)
```
```   263 (*      a 'prop_formula' (just for tracing)                                  *)
```
```   264 (* ------------------------------------------------------------------------- *)
```
```   265
```
```   266 (* PropLogic.prop_formula -> string *)
```
```   267
```
```   268 fun string_of_prop_formula PropLogic.True             = "True"
```
```   269   | string_of_prop_formula PropLogic.False            = "False"
```
```   270   | string_of_prop_formula (PropLogic.BoolVar i)      = "x" ^ string_of_int i
```
```   271   | string_of_prop_formula (PropLogic.Not fm)         = "~" ^ string_of_prop_formula fm
```
```   272   | string_of_prop_formula (PropLogic.Or (fm1, fm2))  = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
```
```   273   | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
```
```   274
```
```   275 (* ------------------------------------------------------------------------- *)
```
```   276 (* take_prefix:                                                              *)
```
```   277 (*      take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
```
```   278 (* ------------------------------------------------------------------------- *)
```
```   279
```
```   280 (* int -> 'a list -> 'a list * 'a list *)
```
```   281
```
```   282 fun take_prefix n xs =
```
```   283 let
```
```   284 	fun take 0 (rxs, xs)      = (rev rxs, xs)
```
```   285 	  | take _ (rxs, [])      = (rev rxs, [])
```
```   286 	  | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
```
```   287 in
```
```   288 	take n ([], xs)
```
```   289 end;
```
```   290
```
```   291 (* ------------------------------------------------------------------------- *)
```
```   292 (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
```
```   293 (*      a proof from the resulting proof trace of the SAT solver.  The       *)
```
```   294 (*      theorem returned is just "False" (with some of the given clauses as  *)
```
```   295 (*      hyps).                                                               *)
```
```   296 (* ------------------------------------------------------------------------- *)
```
```   297
```
```   298 (* Thm.cterm list -> Thm.thm *)
```
```   299
```
```   300 fun rawsat_thm clauses =
```
```   301 let
```
```   302 	(* remove premises that equal "True" *)
```
```   303 	val clauses' = filter (fn clause =>
```
```   304 		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause
```
```   305 			handle TERM ("dest_Trueprop", _) => true) clauses
```
```   306 	(* remove non-clausal premises -- of course this shouldn't actually   *)
```
```   307 	(* remove anything as long as 'rawsat_tac' is only called after the   *)
```
```   308 	(* premises have been converted to clauses                            *)
```
```   309 	val clauses'' = filter (fn clause =>
```
```   310 		((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
```
```   311 			handle TERM ("dest_Trueprop", _) => false)
```
```   312 		orelse (
```
```   313 			warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause);
```
```   314 			false)) clauses'
```
```   315 	(* remove trivial clauses -- this is necessary because zChaff removes *)
```
```   316 	(* trivial clauses during preprocessing, and otherwise our clause     *)
```
```   317 	(* numbering would be off                                             *)
```
```   318 	val nontrivial_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
```
```   319 	(* sort clauses according to the term order -- an optimization,       *)
```
```   320 	(* useful because forming the union of hypotheses, as done by         *)
```
```   321 	(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
```
```   322 	(* terms sorted in descending order, while only linear for terms      *)
```
```   323 	(* sorted in ascending order                                          *)
```
```   324 	val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
```
```   325 	val _ = if !trace_sat then
```
```   326 			tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
```
```   327 		else ()
```
```   328 	(* translate clauses from HOL terms to PropLogic.prop_formula *)
```
```   329 	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
```
```   330 	val _ = if !trace_sat then
```
```   331 			tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
```
```   332 		else ()
```
```   333 	val fm = PropLogic.all fms
```
```   334 	(* unit -> Thm.thm *)
```
```   335 	fun make_quick_and_dirty_thm () =
```
```   336 	let
```
```   337 		val _ = if !trace_sat then
```
```   338 				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
```
```   339 			else ()
```
```   340 		val False_thm = SkipProof.make_thm @{theory} (HOLogic.Trueprop \$ HOLogic.false_const)
```
```   341 	in
```
```   342 		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
```
```   343 		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
```
```   344 		(* clauses in ascending order (which is linear for                  *)
```
```   345 		(* 'Conjunction.intr_balanced', used below)                         *)
```
```   346 		fold Thm.weaken (rev sorted_clauses) False_thm
```
```   347 	end
```
```   348 in
```
```   349 	case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of
```
```   350 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
```
```   351 		if !trace_sat then
```
```   352 			tracing ("Proof trace from SAT solver:\n" ^
```
```   353 				"clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^
```
```   354 				"empty clause: " ^ Int.toString empty_id)
```
```   355 		else ();
```
```   356 		if !quick_and_dirty then
```
```   357 			make_quick_and_dirty_thm ()
```
```   358 		else
```
```   359 			let
```
```   360 				(* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
```
```   361 				(*               this avoids accumulation of hypotheses during resolution    *)
```
```   362 				(* [c_1, ..., c_n] |- c_1 && ... && c_n *)
```
```   363 				val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
```
```   364 				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
```
```   365 				val cnf_cterm = cprop_of clauses_thm
```
```   366 				val cnf_thm   = Thm.assume cnf_cterm
```
```   367 				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
```
```   368 				val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
```
```   369 				(* initialize the clause array with the given clauses *)
```
```   370 				val max_idx    = valOf (Inttab.max_key clause_table)
```
```   371 				val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
```
```   372 				val _          = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
```
```   373 				(* replay the proof to derive the empty clause *)
```
```   374 				(* [c_1 && ... && c_n] |- False *)
```
```   375 				val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
```
```   376 			in
```
```   377 				(* [c_1, ..., c_n] |- False *)
```
```   378 				Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
```
```   379 			end)
```
```   380 	| SatSolver.UNSATISFIABLE NONE =>
```
```   381 		if !quick_and_dirty then (
```
```   382 			warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
```
```   383 			make_quick_and_dirty_thm ()
```
```   384 		) else
```
```   385 			raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
```
```   386 	| SatSolver.SATISFIABLE assignment =>
```
```   387 		let
```
```   388 			val msg = "SAT solver found a countermodel:\n"
```
```   389 				^ (commas
```
```   390 					o map (fn (term, idx) =>
```
```   391 						Syntax.string_of_term_global @{theory} term ^ ": "
```
```   392 							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
```
```   393 					(Termtab.dest atom_table)
```
```   394 		in
```
```   395 			raise THM (msg, 0, [])
```
```   396 		end
```
```   397 	| SatSolver.UNKNOWN =>
```
```   398 		raise THM ("SAT solver failed to decide the formula", 0, [])
```
```   399 end;
```
```   400
```
```   401 (* ------------------------------------------------------------------------- *)
```
```   402 (* Tactics                                                                   *)
```
```   403 (* ------------------------------------------------------------------------- *)
```
```   404
```
```   405 (* ------------------------------------------------------------------------- *)
```
```   406 (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
```
```   407 (*      should be of the form                                                *)
```
```   408 (*        [| c1; c2; ...; ck |] ==> False                                    *)
```
```   409 (*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
```
```   410 (*      or "True"                                                            *)
```
```   411 (* ------------------------------------------------------------------------- *)
```
```   412
```
```   413 fun rawsat_tac ctxt i =
```
```   414   FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
```
```   415
```
```   416 (* ------------------------------------------------------------------------- *)
```
```   417 (* pre_cnf_tac: converts the i-th subgoal                                    *)
```
```   418 (*        [| A1 ; ... ; An |] ==> B                                          *)
```
```   419 (*      to                                                                   *)
```
```   420 (*        [| A1; ... ; An ; ~B |] ==> False                                  *)
```
```   421 (*      (handling meta-logical connectives in B properly before negating),   *)
```
```   422 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
```
```   423 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
```
```   424 (*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
```
```   425 (*      subgoal                                                              *)
```
```   426 (* ------------------------------------------------------------------------- *)
```
```   427
```
```   428 val pre_cnf_tac =
```
```   429         rtac ccontr THEN'
```
```   430         ObjectLogic.atomize_prems_tac THEN'
```
```   431         CONVERSION Drule.beta_eta_conversion;
```
```   432
```
```   433 (* ------------------------------------------------------------------------- *)
```
```   434 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
```
```   435 (*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
```
```   436 (*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
```
```   437 (*      subgoal                                                              *)
```
```   438 (* ------------------------------------------------------------------------- *)
```
```   439
```
```   440 fun cnfsat_tac ctxt i =
```
```   441 	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
```
```   442
```
```   443 (* ------------------------------------------------------------------------- *)
```
```   444 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
```
```   445 (*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
```
```   446 (*      CNF formula becomes a separate premise) and existential quantifiers, *)
```
```   447 (*      then applies 'rawsat_tac' to solve the subgoal                       *)
```
```   448 (* ------------------------------------------------------------------------- *)
```
```   449
```
```   450 fun cnfxsat_tac ctxt i =
```
```   451 	(etac FalseE i) ORELSE
```
```   452 		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
```
```   453
```
```   454 (* ------------------------------------------------------------------------- *)
```
```   455 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
```
```   456 (*      arbitrary formula.  The input is translated to CNF, possibly causing *)
```
```   457 (*      an exponential blowup.                                               *)
```
```   458 (* ------------------------------------------------------------------------- *)
```
```   459
```
```   460 fun sat_tac ctxt i =
```
```   461 	pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
```
```   462
```
```   463 (* ------------------------------------------------------------------------- *)
```
```   464 (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
```
```   465 (*      arbitrary formula.  The input is translated to CNF, possibly         *)
```
```   466 (*      introducing new literals.                                            *)
```
```   467 (* ------------------------------------------------------------------------- *)
```
```   468
```
```   469 fun satx_tac ctxt i =
```
```   470 	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
```
```   471
```
```   472 end;
```