src/HOL/SAT.thy
author wenzelm
Thu, 22 Dec 2005 00:28:36 +0100
changeset 18457 356a9f711899
parent 17809 195045659c06
child 21588 cd0dc678a205
permissions -rw-r--r--
structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     1
(*  Title:      HOL/SAT.thy
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     2
    ID:         $Id$
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     3
    Author:     Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
    Copyright   2005
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     5
17627
ff1923b1978b cnf_struct renamed to cnf
webertj
parents: 17625
diff changeset
     6
Basic setup for the 'sat' and 'satx' tactic.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     7
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     8
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     9
header {* Reconstructing external resolution proofs for propositional logic *}
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    10
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    11
theory SAT imports Refute
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    12
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    13
uses
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    14
     "Tools/cnf_funcs.ML"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
     "Tools/sat_funcs.ML"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    16
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
begin
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    18
17722
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    19
text {* \medskip Late package setup: default values for refute, see
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    20
  also theory @{text Refute}. *}
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    21
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    22
refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    23
 ["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    24
  minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    25
  maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    26
  maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    27
  maxtime=60,
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    28
  satsolver="auto"]
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    29
8e098e040c2e explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17631
diff changeset
    30
17627
ff1923b1978b cnf_struct renamed to cnf
webertj
parents: 17625
diff changeset
    31
ML {* structure sat = SATFunc(structure cnf = cnf); *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    32
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17722
diff changeset
    33
method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    34
  "SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    35
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 17722
diff changeset
    36
method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    37
  "SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    38
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    39
end