src/HOL/SAT.thy
author webertj
Sun Oct 09 17:06:03 2005 +0200 (2005-10-09)
changeset 17809 195045659c06
parent 17722 8e098e040c2e
child 21588 cd0dc678a205
permissions -rw-r--r--
Tactics sat and satx reimplemented, several improvements
     1 (*  Title:      HOL/SAT.thy
     2     ID:         $Id$
     3     Author:     Alwen Tiu, Tjark Weber
     4     Copyright   2005
     5 
     6 Basic setup for the 'sat' and 'satx' tactic.
     7 *)
     8 
     9 header {* Reconstructing external resolution proofs for propositional logic *}
    10 
    11 theory SAT imports Refute
    12 
    13 uses
    14      "Tools/cnf_funcs.ML"
    15      "Tools/sat_funcs.ML"
    16 
    17 begin
    18 
    19 text {* \medskip Late package setup: default values for refute, see
    20   also theory @{text Refute}. *}
    21 
    22 refute_params
    23  ["itself"=1,
    24   minsize=1,
    25   maxsize=8,
    26   maxvars=10000,
    27   maxtime=60,
    28   satsolver="auto"]
    29 
    30 
    31 ML {* structure sat = SATFunc(structure cnf = cnf); *}
    32 
    33 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
    34   "SAT solver"
    35 
    36 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
    37   "SAT solver (with definitional CNF)"
    38 
    39 end