# HG changeset patch # User webertj # Date 1142004710 -3600 # Node ID 150e8b0fb9914fe27cb59d87e6bf2880b861b8db # Parent 868129805da8039a25f548296a92e37a7946bb36 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup diff -r 868129805da8 -r 150e8b0fb991 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Fri Mar 10 16:21:49 2006 +0100 +++ b/src/HOL/Tools/cnf_funcs.ML Fri Mar 10 16:31:50 2006 +0100 @@ -2,14 +2,14 @@ ID: $Id$ Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) Author: Tjark Weber - Copyright 2005 + Copyright 2005-2006 Description: This file contains functions and tactics to transform a formula into Conjunctive Normal Form (CNF). A formula in CNF is of the following form: - (x11 | x12 | .. x1n) & ... & (xm1 | xm2 | ... | xmk) + (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk) False True @@ -23,11 +23,13 @@ representation of clauses, which we call the "raw clauses". Raw clauses are of the form - x1 ==> x2 ==> .. ==> xn ==> False , + x1', x2', ..., xn', ~ (x1 | x2 | ... | xn) ==> False |- False , + + where each xi is a literal, and each xi' is the negation normal form of ~xi. - where each xi is a literal. Note that the above raw clause corresponds - to the clause (x1' | ... | xn'), where each xi' is the negation normal - form of ~xi. + Raw clauses may contain further hyps of the form "~ clause ==> False". + Literals are successively removed from the hyps of raw clauses by resolution + during SAT proof reconstruction. *) signature CNF = @@ -37,8 +39,8 @@ val is_clause : Term.term -> bool val clause_is_trivial : Term.term -> bool - val is_raw_clause : Term.term -> bool - val clause2raw_thm : Thm.thm -> Thm.thm + val clause2raw_thm : Thm.thm -> Thm.thm + val rawhyps2clausehyps_thm : Thm.thm -> Thm.thm val weakening_tac : int -> Tactical.tactic (* removes the first hypothesis of a subgoal *) @@ -137,24 +139,10 @@ end; (* ------------------------------------------------------------------------- *) -(* is_raw_clause: returns true iff the term is of the form *) -(* x1 ==> ... ==> xn ==> False , *) -(* with n >= 1, where each xi is a literal *) -(* ------------------------------------------------------------------------- *) - -(* Term.term -> bool *) - -fun is_raw_clause (Const ("==>", _) $ x $ y) = - is_literal x andalso - (y = HOLogic.mk_Trueprop HOLogic.false_const orelse is_raw_clause y) - | is_raw_clause _ = - false; - -(* ------------------------------------------------------------------------- *) (* clause2raw_thm: translates a clause into a raw clause, i.e. *) -(* x1 | ... | xn *) +(* ... |- x1 | ... | xn *) (* (where each xi is a literal) is translated to *) -(* x1' ==> ... ==> xn' ==> False , *) +(* ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False , *) (* where each xi' is the negation normal form of ~xi. *) (* ------------------------------------------------------------------------- *) @@ -162,7 +150,9 @@ fun clause2raw_thm c = let - val thm1 = c RS clause2raw_notE (* ~(x1 | ... | xn) ==> False *) + val disj = HOLogic.dest_Trueprop (prop_of c) + val not_disj_imp_false = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_not disj), HOLogic.mk_Trueprop HOLogic.false_const) + val thm1 = Thm.assume (cterm_of (theory_of_thm c) not_disj_imp_false) (* ~(x1 | ... | xn) ==> False |- ~(x1 | ... | xn) ==> False *) (* eliminates negated disjunctions from the i-th premise, possibly *) (* adding new premises, then continues with the (i+1)-th premise *) (* Thm.thm -> int -> Thm.thm *) @@ -171,13 +161,38 @@ thm else not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1) - val thm2 = not_disj_to_prem thm1 1 (* ~x1 ==> ... ==> ~xn ==> False *) - val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2) (* x1' ==> ... ==> xn' ==> False *) + val thm2 = not_disj_to_prem thm1 1 (* ~(x1 | ... | xn) ==> False |- ~x1 ==> ... ==> ~xn ==> False *) + val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2) (* ~(x1 | ... | xn) ==> False |- x1' ==> ... ==> xn' ==> False *) + val thy3 = theory_of_thm thm3 + val thm4 = fold (fn prem => fn thm => Thm.implies_elim thm (Thm.assume (cterm_of thy3 prem))) (prems_of thm3) thm3 (* ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False *) in - thm3 + thm4 end; (* ------------------------------------------------------------------------- *) +(* rawhyps2clausehyps_thm: translates all hyps of the form "~P ==> False" to *) +(* hyps of the form "P" *) +(* ------------------------------------------------------------------------- *) + +(* Thm.thm -> Thm.thm *) + +fun rawhyps2clausehyps_thm c = + fold (fn hyp => fn thm => + case hyp of Const ("==>", _) $ (Const ("Trueprop", _) $ (Const ("Not", _) $ P)) $ (Const ("Trueprop", _) $ Const ("False", _)) => + let + val cterm = cterm_of (theory_of_thm thm) + val thm1 = Thm.implies_intr (cterm hyp) thm (* hyps |- (~P ==> False) ==> goal *) + val varP = Var (("P", 0), HOLogic.boolT) + val notE = Thm.instantiate ([], [(cterm varP, cterm P)]) clause2raw_notE (* P ==> ~P ==> False *) + val notE' = Thm.implies_elim notE (Thm.assume (cterm (HOLogic.mk_Trueprop P))) (* P |- ~P ==> False *) + val thm2 = Thm.implies_elim thm1 notE' (* hyps, P |- goal *) + in + thm2 + end + | _ => + thm) (#hyps (rep_thm c)) c; + +(* ------------------------------------------------------------------------- *) (* inst_thm: instantiates a theorem with a list of terms *) (* ------------------------------------------------------------------------- *) diff -r 868129805da8 -r 150e8b0fb991 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Fri Mar 10 16:21:49 2006 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Fri Mar 10 16:31:50 2006 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) Author: Tjark Weber - Copyright 2005 + Copyright 2005-2006 Proof reconstruction from SAT solvers. @@ -14,15 +14,14 @@ We use a sequent presentation of clauses to speed up resolution proof reconstruction. We call such clauses "raw clauses", which are of the form - [| c1; c2; ...; ck |] ==> False + x1; ...; xn; c1; c2; ...; ck |- False + (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here), where each clause ci is of the form - [| l1; l2; ...; lm |] ==> False, - where each li is a literal (see also comments in cnf_funcs.ML). + ~ (l1 | l2 | ... | lm) ==> False, + where each xi and each li is a literal (see also comments in cnf_funcs.ML). - -- Observe that this is the "dualized" version of the standard - clausal form - l1' \/ l2' \/ ... \/ lm', where li is the negation normal - form of ~li'. + This does not work for goals containing schematic variables! + The tactic produces a clause representation of the given goal in DIMACS format and invokes a SAT solver, which should return a proof consisting of a sequence of resolution steps, indicating @@ -65,21 +64,15 @@ val counter = ref 0; -(* ------------------------------------------------------------------------- *) -(* swap_prem: convert raw clauses of the form *) -(* [| l1; l2; ...; li; ... |] ==> False *) -(* to *) -(* [| l1; l2; ... |] ==> ~li . *) -(* Note that ~li may be equal to ~~a for some atom a. *) -(* ------------------------------------------------------------------------- *) - -(* Thm.thm -> int -> Thm.thm *) - -fun swap_prem raw_cl i = - Seq.hd ((metacut_tac raw_cl 1 (* [| [| ?P; False |] ==> False; ?P ==> l1; ...; ?P ==> li; ... |] ==> ~ ?P *) - THEN atac (i+1) (* [| [| li; False |] ==> False; li ==> l1; ... |] ==> ~ li *) - THEN atac 1 (* [| li ==> l1; ... |] ==> ~ li *) - THEN ALLGOALS cnf.weakening_tac) notI); +(* Thm.thm *) +val resolution_thm = (* "[| P ==> False; ~P ==> False |] ==> False" *) + let + val cterm = cterm_of (the_context ()) + val Q = Var (("Q", 0), HOLogic.boolT) + val False = HOLogic.false_const + in + Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm + end; (* ------------------------------------------------------------------------- *) (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) @@ -109,35 +102,70 @@ fun is_neg (Const ("Not", _) $ _) = true | is_neg _ = false - (* find out which premises are used in the resolution *) - (* Term.term list -> Term.term list -> int -> (int * int * bool) *) - fun res_prems [] _ _ = + (* find out which two hyps are used in the resolution *) + (* Term.term list -> Term.term list -> Term.term * Term.term *) + fun res_hyps [] _ = + raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) + | res_hyps _ [] = raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) - | res_prems (x::xs) ys idx1 = - let - val x' = HOLogic.dest_Trueprop x - val idx2 = find_index_eq (dual x') ys - in - if idx2 = (~1) then - res_prems xs ys (idx1+1) + | res_hyps ((Const ("Trueprop", _) $ x) :: xs) ys = + let val dx = dual x in + (* hyps are implemented as ordered list in the kernel, and *) + (* stripping 'Trueprop' should not change the order *) + if OrdList.member Term.fast_term_ord ys dx then + (x, dx) else - (idx1, idx2, is_neg x') + res_hyps xs ys end + | res_hyps (_ :: xs) ys = + (* hyps are implemented as ordered list in the kernel, all hyps are of *) + (* the form 'Trueprop $ lit' or 'implies $ (negated clause) $ False', *) + (* and the former are LESS than the latter according to the order -- *) + (* therefore there is no need to continue the search via *) + (* 'res_hyps xs ys' here *) + raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) (* Thm.thm -> Thm.thm -> Thm.thm *) fun resolution c1 c2 = let val _ = if !trace_sat then - tracing ("Resolving clause: " ^ string_of_thm c1 ^ "\nwith clause: " ^ string_of_thm c2) + tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))) + ^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2))) ^ ")") else () - val prems2 = map HOLogic.dest_Trueprop (prems_of c2) - val (idx1, idx2, is_neg_lit) = res_prems (prems_of c1) prems2 0 - val swap_c1 = swap_prem c1 (idx1+1) - val swap_c1_nnf = if is_neg_lit then Seq.hd (rtac swap_c1 1 notnotD) else swap_c1 (* deal with double-negation *) - val c_new = Seq.hd ((rtac swap_c1_nnf (idx2+1) THEN distinct_subgoals_tac) c2) + (* Term.term list -> Term.term list *) + fun dest_filter_Trueprop [] = [] + | dest_filter_Trueprop ((Const ("Trueprop", _) $ x) :: xs) = x :: dest_filter_Trueprop xs + | dest_filter_Trueprop (_ :: xs) = dest_filter_Trueprop xs + + val hyps1 = (#hyps o rep_thm) c1 + (* minor optimization: dest/filter over the second list outside 'res_hyps' to do it only once *) + val hyps2 = (dest_filter_Trueprop o #hyps o rep_thm) c2 + + val (l1, l2) = res_hyps hyps1 hyps2 (* the two literals used for resolution, with 'Trueprop' stripped *) + val is_neg = is_neg l1 + + val c1' = Thm.implies_intr (cterm_of (theory_of_thm c1) (HOLogic.mk_Trueprop l1)) c1 (* Gamma1 |- l1 ==> False *) + val c2' = Thm.implies_intr (cterm_of (theory_of_thm c2) (HOLogic.mk_Trueprop l2)) c2 (* Gamma2 |- l2 ==> False *) - val _ = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm c_new) else () + val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) + let + val P = Var (("P", 0), HOLogic.boolT) + val (lit, thy) = if is_neg then (l2, theory_of_thm c2') else (l1, theory_of_thm c1') + val cterm = cterm_of thy + in + Thm.instantiate ([], [(cterm P, cterm lit)]) resolution_thm + end + + val _ = if !trace_sat then + tracing ("Resolution theorem: " ^ string_of_thm res_thm) + else () + + 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 *) + + val _ = if !trace_sat then + 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))) ^ ")") + else () val _ = inc counter in c_new @@ -248,11 +276,17 @@ (* but converted to raw clause format *) val max_idx = valOf (Inttab.max_key clause_table) val clause_arr = Array.array (max_idx + 1, NONE) - val raw_clauses = map (Seq.hd o distinct_subgoals_tac o cnf.clause2raw_thm) non_triv_clauses + val raw_clauses = map cnf.clause2raw_thm non_triv_clauses + (* Every raw clause has only its literals and itself as hyp, and hyps are *) + (* accumulated during resolution steps. Experimental results indicate *) + (* that it is NOT faster to weaken all raw_clauses to contain every *) + (* clause in the hyps beforehand. *) val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0 + (* replay the proof to derive the empty clause *) + val FalseThm = replay_proof clause_arr (clause_table, empty_id) in - (* replay the proof to derive the empty clause *) - replay_proof clause_arr (clause_table, empty_id) + (* convert the hyps back to the original format *) + cnf.rawhyps2clausehyps_thm FalseThm end) | SatSolver.UNSATISFIABLE NONE => if !quick_and_dirty then ( diff -r 868129805da8 -r 150e8b0fb991 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Fri Mar 10 16:21:49 2006 +0100 +++ b/src/HOL/ex/SAT_Examples.thy Fri Mar 10 16:31:50 2006 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/ex/SAT_Examples.thy ID: $Id$ Author: Alwen Tiu, Tjark Weber - Copyright 2005 + Copyright 2005-2006 *) header {* Examples for the 'sat' and 'satx' tactic *} @@ -11,6 +11,7 @@ begin ML {* set sat.trace_sat; *} +ML {* set quick_and_dirty; *} lemma "True" by sat @@ -64,10 +65,9 @@ by satx ML {* reset sat.trace_sat; *} +ML {* reset quick_and_dirty; *} -(* ML {* Toplevel.profiling := 1; *} -*) (* Translated from TPTP problem library: PUZ015-2.006.dimacs *) @@ -488,8 +488,6 @@ 200 201 202 203 204 by sat -(* ML {* Toplevel.profiling := 0; *} -*) end