10 Description: |
10 Description: |
11 This file defines several tactics to invoke a proof-producing |
11 This file defines several tactics to invoke a proof-producing |
12 SAT solver on a propositional goal in clausal form. |
12 SAT solver on a propositional goal in clausal form. |
13 |
13 |
14 We use a sequent presentation of clauses to speed up resolution |
14 We use a sequent presentation of clauses to speed up resolution |
15 proof reconstruction. |
15 proof reconstruction. |
16 We call such clauses as "raw clauses", which are of the form |
16 We call such clauses "raw clauses", which are of the form |
17 [| c1; c2; ...; ck |] ==> False |
17 [| c1; c2; ...; ck |] ==> False |
18 where each clause ci is of the form |
18 where each clause ci is of the form |
19 [|l1, l2, ..., lm |] ==> False, |
19 [| l1; l2; ...; lm |] ==> False, |
20 where li is a literal (see also comments in cnf_funcs.ML). |
20 where each li is a literal (see also comments in cnf_funcs.ML). |
21 |
21 |
22 -- observe that this is the "dualized" version of the standard |
22 -- observe that this is the "dualized" version of the standard |
23 clausal form |
23 clausal form |
24 l1' \/ l2' \/ ... \/ lm', where li is the negation normal |
24 l1' \/ l2' \/ ... \/ lm', where li is the negation normal |
25 form of ~li'. |
25 form of ~li'. |
26 The tactic produces a clause representation of the given goal |
26 The tactic produces a clause representation of the given goal |
27 in DIMACS format and invokes a SAT solver, which should return |
27 in DIMACS format and invokes a SAT solver, which should return |
28 a proof consisting of a sequence of resolution steps, indicating |
28 a proof consisting of a sequence of resolution steps, indicating |
29 the two input clauses and the variable resolved upon, and resulting |
29 the two input clauses, and resulting in new clauses, leading to |
30 in new clauses, leading to the empty clause (i.e., False). |
30 the empty clause (i.e., False). The tactic replays this proof |
31 The tactic replays this proof in Isabelle and thus solves the |
31 in Isabelle and thus solves the overall goal. |
32 overall goal. |
|
33 |
32 |
34 There are two SAT tactics available. They differ in the CNF transformation |
33 There are two SAT tactics available. They differ in the CNF transformation |
35 used. The "sat_tac" uses naive CNF transformation to transform the theorem |
34 used. The "sat_tac" uses naive CNF transformation to transform the theorem |
36 to be proved before giving it to SAT solver. The naive transformation in |
35 to be proved before giving it to SAT solver. The naive transformation in |
37 some worst case can lead to explonential blow up in formula size. |
36 some worst case can lead to explonential blow up in formula size. |
38 The other tactic, the "satx_tac" uses the "definitional CNF transformation" |
37 The other tactic, the "satx_tac" uses the "definitional CNF transformation" |
39 which produces formula of linear size increase compared to the input formula. |
38 which produces formula of linear size increase compared to the input formula. |
40 This transformation introduces new variables. See also cnf_funcs.ML for |
39 This transformation introduces new variables. See also cnf_funcs.ML for |
41 more comments. |
40 more comments. |
45 - The environment variable ZCHAFF_HOME must be set to point to |
44 - The environment variable ZCHAFF_HOME must be set to point to |
46 the directory where zChaff executable resides |
45 the directory where zChaff executable resides |
47 - The environment variable ZCHAFF_VERSION must be set according to |
46 - The environment variable ZCHAFF_VERSION must be set according to |
48 the version of zChaff used. Current supported version of zChaff: |
47 the version of zChaff used. Current supported version of zChaff: |
49 zChaff version 2004.11.15 |
48 zChaff version 2004.11.15 |
|
49 - zChaff must have been compiled with proof generation enabled |
|
50 (#define VERIFY_ON). |
50 *) |
51 *) |
51 |
52 |
52 signature SAT = |
53 signature SAT = |
53 sig |
54 sig |
54 val trace_sat : bool ref (* print trace messages *) |
55 val trace_sat : bool ref (* print trace messages *) |