author webertj Fri, 07 Jul 2006 18:13:58 +0200 changeset 20039 4293f932fe83 parent 20038 73231d03a2ac child 20040 02c59ec2f2e1
"solver" reference added to make the SAT solver configurable
 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/sat_funcs.ML	Fri Jul 07 15:13:15 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Fri Jul 07 18:13:58 2006 +0200
@@ -22,39 +22,49 @@

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
-       the two input clauses, and resulting in new clauses, leading to
-       the empty clause (i.e., False).  The tactic replays this proof
-       in Isabelle and thus solves the overall goal.
+      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
+      the two input clauses, and resulting in new clauses, leading to
+      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
-   used. The "sat_tac" uses naive CNF transformation to transform the theorem
-   to be proved before giving it to SAT solver. The naive transformation in
-   some worst case can lead to explonential blow up in formula size.
-   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
-   which produces formula of linear size increase compared to the input formula.
-   This transformation introduces new variables. See also cnf_funcs.ML for
-   more comments.
+  There are two 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
+  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.

- Notes for the current revision:
-   - The current version supports only zChaff prover.
-   - The environment variable ZCHAFF_HOME must be set to point to
-     the directory where zChaff executable resides
-   - The environment variable ZCHAFF_VERSION must be set according to
-     the version of zChaff used. Current supported version of zChaff:
+  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-
+  dependent) configuration settings.  To replay SAT proofs in Isabelle, you
+  must of course use a proof-producing SAT solver in the first place.
+
+  Notes for the current revision:
+   - Currently zChaff is the only proof-producing SAT solver that is supported.
+   - The environment variable ZCHAFF_HOME must be set to point to the directory
+     where the zChaff executable resides.
+   - The environment variable ZCHAFF_VERSION must be set according to the
+     version of zChaff used.  Current supported version of zChaff:
zChaff version 2004.11.15
- zChaff must have been compiled with proof generation enabled
(#define VERIFY_ON).
+
+  Proofs are replayed only if "!quick_and_dirty" is false.  If
+  "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
+  negation to be unsatisfiable) is proved via an oracle.
*)

signature SAT =
sig
-	val trace_sat : bool ref  (* print trace messages *)
+	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 counter   : int ref  (* number of resolution steps during last proof replay *)
end

functor SATFunc (structure cnf : CNF) : SAT =
@@ -62,6 +72,8 @@

val trace_sat = ref false;

+val solver = ref "zchaff_with_proofs";
+
val counter = ref 0;

(* Thm.thm *)
@@ -273,7 +285,7 @@
SkipProof.make_thm (the_context ()) (HOLogic.Trueprop \$ HOLogic.false_const)
)
in
-	case SatSolver.invoke_solver "zchaff_with_proofs" fm of
+	case SatSolver.invoke_solver (!solver) fm of
SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
if !trace_sat then
tracing ("Proof trace from SAT solver:\n" ^
@@ -397,4 +409,4 @@

fun satx_tac i = pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;

-end;  (* of structure *)
+end;  (* of structure SATFunc *)```
```--- a/src/HOL/ex/SAT_Examples.thy	Fri Jul 07 15:13:15 2006 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Jul 07 18:13:58 2006 +0200
@@ -10,6 +10,7 @@

begin

+(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
ML {* set sat.trace_sat; *}
ML {* set quick_and_dirty; *}
```