author webertj Fri, 10 Mar 2006 16:31:50 +0100 changeset 19236 150e8b0fb991 parent 19235 868129805da8 child 19237 f51301fafdc2
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
 src/HOL/Tools/cnf_funcs.ML file | annotate | diff | comparison | revisions src/HOL/Tools/sat_funcs.ML file | annotate | diff | comparison | revisions src/HOL/ex/SAT_Examples.thy file | annotate | diff | comparison | revisions
```--- 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

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

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,
+          ~ (l1 | l2 | ... | lm) ==> False,

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

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```