faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
--- a/src/HOL/Tools/cnf_funcs.ML Wed Aug 30 15:11:17 2006 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Wed Aug 30 16:27:53 2006 +0200
@@ -23,11 +23,10 @@
representation of clauses, which we call the "raw clauses".
Raw clauses are of the form
- x1', x2', ..., xn', ~ (x1 | x2 | ... | xn) ==> False |- False ,
+ [..., x1', x2', ..., xn'] |- False ,
where each xi is a literal, and 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.
*)
@@ -39,8 +38,7 @@
val is_clause : Term.term -> bool
val clause_is_trivial : Term.term -> bool
- val clause2raw_thm : Thm.thm -> Thm.thm
- val rawhyps2clausehyps_thm : Thm.thm -> Thm.thm
+ val clause2raw_thm : Thm.thm -> Thm.thm
val weakening_tac : int -> Tactical.tactic (* removes the first hypothesis of a subgoal *)
@@ -53,8 +51,7 @@
structure cnf : CNF =
struct
-(* string -> Thm.thm *)
-fun thm_by_auto G =
+fun thm_by_auto (G : string) : thm =
prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
(* Thm.thm *)
@@ -140,59 +137,42 @@
(* ------------------------------------------------------------------------- *)
(* 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 , *)
-(* where each xi' is the negation normal form of ~xi. *)
+(* [..., x1', ..., xn'] |- False , *)
+(* where each xi' is the negation normal form of ~xi *)
(* ------------------------------------------------------------------------- *)
(* Thm.thm -> Thm.thm *)
-fun clause2raw_thm c =
+fun clause2raw_thm clause =
let
- 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 *)
- fun not_disj_to_prem thm i =
+ (* int -> Thm.thm -> Thm.thm *)
+ fun not_disj_to_prem i thm =
if i > nprems_of thm then
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 |- ~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 *)
+ not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
+ (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
+ (* becomes "[..., A1, ..., An] |- B" *)
+ (* Thm.thm -> Thm.thm *)
+ fun prems_to_hyps thm =
+ fold (fn cprem => fn thm' =>
+ Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
in
- thm4
+ (* [...] |- ~(x1 | ... | xn) ==> False *)
+ (clause2raw_notE OF [clause])
+ (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
+ |> not_disj_to_prem 1
+ (* [...] |- x1' ==> ... ==> xn' ==> False *)
+ |> Seq.hd o TRYALL (rtac clause2raw_not_not)
+ (* [..., x1', ..., xn'] |- False *)
+ |> prems_to_hyps
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 *)
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/sat_funcs.ML Wed Aug 30 15:11:17 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Wed Aug 30 16:27:53 2006 +0200
@@ -14,11 +14,9 @@
We use a sequent presentation of clauses to speed up resolution
proof reconstruction.
We call such clauses "raw clauses", which are of the form
- x1; ...; xn; c1; c2; ...; ck |- False
+ [x1, ..., xn, P] |- 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 xi and each li is a literal (see also comments in cnf_funcs.ML).
+ where each xi is a literal (see also comments in cnf_funcs.ML).
This does not work for goals containing schematic variables!
@@ -29,14 +27,17 @@
the empty clause (i.e. "False"). The tactic replays this proof
in Isabelle and thus solves the overall goal.
- There are two SAT tactics available. They differ in the CNF transformation
+ There are three SAT tactics available. They differ in the CNF transformation
used. "sat_tac" uses naive CNF transformation to transform the theorem to be
proved before giving it to the SAT solver. The naive transformation in the
- worst case can lead to an exponential blow up in formula size. The other
+ worst case can lead to an exponential blow up in formula size. Another
tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
produce a formula of linear size increase compared to the input formula, at
the cost of possibly introducing new variables. See cnf_funcs.ML for more
- comments on the CNF transformation.
+ comments on the CNF transformation. "rawsat_tac" should be used with
+ caution: no CNF transformation is performed, and the tactic's behavior is
+ undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
+ where each Ci is a disjunction.
The SAT solver to be used can be set via the "solver" reference. See
sat_solvers.ML for possible values, and etc/settings for required (solver-
@@ -50,11 +51,12 @@
signature SAT =
sig
- val trace_sat : bool ref (* print trace messages *)
- val solver : string ref (* name of SAT solver to be used *)
- val counter : int ref (* number of resolution steps during last proof replay *)
- val sat_tac : int -> Tactical.tactic
- val satx_tac : int -> Tactical.tactic
+ val trace_sat : bool ref (* print trace messages *)
+ val solver : string ref (* name of SAT solver to be used *)
+ val counter : int ref (* number of resolution steps during last proof replay *)
+ val rawsat_tac : int -> Tactical.tactic
+ val sat_tac : int -> Tactical.tactic
+ val satx_tac : int -> Tactical.tactic
end
functor SATFunc (structure cnf : CNF) : SAT =
@@ -97,18 +99,18 @@
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *)
(* resolution over the list (starting with its head), i.e. with two raw *)
(* clauses *)
-(* x1; ... ; a; ...; xn |- False *)
+(* [P, x1, ..., a, ..., xn] |- False *)
(* and *)
-(* y1; ... ; a'; ...; ym |- False *)
+(* [Q, y1, ..., a', ..., ym] |- False *)
(* (where a and a' are dual to each other), we convert the first clause *)
(* to *)
-(* x1; ...; xn |- a ==> False , *)
+(* [P, x1, ..., xn] |- a ==> False , *)
(* the second clause to *)
-(* y1; ...; ym |- a' ==> False *)
+(* [Q, y1, ..., ym] |- a' ==> False *)
(* and then perform resolution with *)
(* [| ?P ==> False; ~?P ==> False |] ==> False *)
(* to produce *)
-(* x1; ...; xn; y1; ...; ym |- False *)
+(* [P, Q, x1, ..., xn, y1, ..., ym] |- False *)
(* Each clause is accompanied with a table mapping integers (positive *)
(* for positive literals, negative for negative literals, and the same *)
(* absolute value for dual literals) to the actual literals as cterms. *)
@@ -136,8 +138,8 @@
fun resolution (c1, hyp1_table) (c2, hyp2_table) =
let
val _ = if !trace_sat then
- 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))) ^ ")")
+ tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
+ ^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
else ()
(* the two literals used for resolution *)
@@ -158,15 +160,18 @@
tracing ("Resolution theorem: " ^ string_of_thm res_thm)
else ()
- val c_new = Thm.implies_elim (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) (if hyp1_is_neg then c1' else c2') (* Gamma1, Gamma2 |- False *)
+ (* Gamma1, Gamma2 |- False *)
+ val c_new = Thm.implies_elim
+ (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
+ (if hyp1_is_neg then c1' else c2')
(* since the mapping from integers to literals should be injective *)
(* (over different clauses), 'K true' here should be equivalent to *)
- (* 'op=' (but faster) *)
+ (* 'op=' (but slightly faster) *)
val hypnew_table = Inttab.merge (K true) (Inttab.delete i1 hyp1_table, Inttab.delete (~i1) hyp2_table)
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))) ^ ")")
+ tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ string_of_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
else ()
val _ = inc counter
in
@@ -307,15 +312,38 @@
make_quick_and_dirty_thm ()
else
let
+ (* optimization: convert the given clauses from "[c_i] |- c_i" to *)
+ (* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of *)
+ (* hypotheses during resolution *)
+ (* Thm.cterm list -> Thm.cterm *)
+ fun mk_conjunction_list [x] = x
+ | mk_conjunction_list (x::xs) = Conjunction.mk_conjunction (x, mk_conjunction_list xs)
+ (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
+ val cnf_cterm = mk_conjunction_list (map cprop_of non_triv_clauses)
+ val cnf_thm = Thm.assume cnf_cterm
+ (* cf. Conjunction.elim_list *)
+ fun right_elim_list th =
+ let val (th1, th2) = Conjunction.elim th
+ in [th1] @ right_elim_list th2 end handle THM _ => [th]
+ (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
+ val converted_clauses = right_elim_list cnf_thm
(* initialize the clause array with the given clauses *)
- val max_idx = valOf (Inttab.max_key clause_table)
- val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
- val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) non_triv_clauses 0
+ val max_idx = valOf (Inttab.max_key clause_table)
+ val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
+ val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) converted_clauses 0
(* replay the proof to derive the empty clause *)
- val FalseThm = replay_proof atom_table clause_arr (clause_table, empty_id)
+ (* [c_1 && ... && c_n] |- False *)
+ val FalseThm = replay_proof atom_table clause_arr (clause_table, empty_id)
in
- (* convert the hyps back to the original format *)
- cnf.rawhyps2clausehyps_thm FalseThm
+ (* convert the &&-hyp back to the original clauses format *)
+ FalseThm
+ (* [] |- c_1 && ... && c_n ==> False *)
+ |> Thm.implies_intr cnf_cterm
+ (* c_1 ==> ... ==> c_n ==> False *)
+ |> Conjunction.curry ~1
+ (* [c_1, ..., c_n] |- False *)
+ |> (fn thm => fold (fn cprem => fn thm' =>
+ Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm)
end)
| SatSolver.UNSATISFIABLE NONE =>
if !quick_and_dirty then (
--- a/src/HOL/ex/SAT_Examples.thy Wed Aug 30 15:11:17 2006 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Wed Aug 30 16:27:53 2006 +0200
@@ -82,6 +82,9 @@
ML {* reset sat.trace_sat; *}
ML {* reset quick_and_dirty; *}
+method_setup rawsat = {* Method.no_args (Method.SIMPLE_METHOD (sat.rawsat_tac 1)) *}
+ "SAT solver (no preprocessing)"
+
ML {* Toplevel.profiling := 1; *}
(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
@@ -281,7 +284,10 @@
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
180 181 182 183 184
+(*
by sat
+*)
+by rawsat -- {* this is without CNF conversion time *}
(* Translated from TPTP problem library: MSC007-1.008.dimacs *)
@@ -501,11 +507,23 @@
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
200 201 202 203 204
+(*
by sat
+*)
+by rawsat -- {* this is without CNF conversion time *}
+
+(* Old sequent clause representation ("[c_i, p, ~q, \<dots>] \<turnstile> False"):
+ sat, zchaff_with_proofs: 8705 resolution steps in +++ User 1.154 All 1.189 secs
+ sat, minisat_with_proofs: 40790 resolution steps in +++ User 3.762 All 3.806 secs
-(* zchaff_with_proofs: 8705 resolution steps in +++ User 1.154 All 1.189 secs
- minisat_with_proofs: 40790 resolution steps in +++ User 3.762 All 3.806 secs
- (as of 2006-08-01, on a 2.5 GHz Pentium 4)
+ rawsat, zchaff_with_proofs: 8705 resolution steps in +++ User 0.731 All 0.751 secs
+ rawsat, minisat_with_proofs: 40790 resolution steps in +++ User 3.514 All 3.550 secs
+
+ CNF clause representation ("[c_1 && \<dots> && c_n, p, ~q, \<dots>] \<turnstile> False"):
+ rawsat, zchaff_with_proofs: 8705 resolution steps in +++ User 0.653 All 0.670 secs
+ rawsat, minisat_with_proofs: 40790 resolution steps in +++ User 1.860 All 1.886 secs
+
+ (as of 2006-08-30, on a 2.5 GHz Pentium 4)
*)
ML {* Toplevel.profiling := 0; *}