# Theory SAT

Up to index of Isabelle/HOL

theory SAT
imports Refute
uses Tools/cnf_funcs.ML Tools/sat_funcs.ML
begin

    (*  Title:      HOL/SAT.thy
        ID:         $Id: SAT.thy,v 1.5 2005/09/29 13:50:45 wenzelm Exp $
        Author:     Alwen Tiu, Tjark Weber
        Copyright   2005

    Basic setup for the 'sat' and 'satx' tactic.
    *)

    header {* Reconstructing external resolution proofs for propositional logic *}

    theory SAT imports Refute

    uses
         "Tools/cnf_funcs.ML"
         "Tools/sat_funcs.ML"

    begin

    text {* \medskip Late package setup: default values for refute, see
      also theory @{text Refute}. *}

    refute_params
     ["itself"=1,
      minsize=1,
      maxsize=8,
      maxvars=10000,
      maxtime=60,
      satsolver="auto"]

    ML {* structure sat = SATFunc(structure cnf = cnf); *}

    method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
      "SAT solver"

    method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
      "SAT solver (with definitional CNF)"

    end