(* Title: HOL/Tools/sat_funcs.ML ID: $Id: sat_funcs.ML,v 1.5 2005/09/28 12:41:43 webertj Exp $ Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) Author: Tjark Weber Copyright 2005 Proof reconstruction from SAT solvers. Description: This file defines several tactics to invoke a proof-producing SAT solver on a propositional goal in clausal form. We use a sequent presentation of clauses to speed up resolution proof reconstruction. We call such clauses "raw clauses", which are of the form [| c1; c2; ...; ck |] ==> False where each clause ci is of the form [| l1; l2; ...; lm |] ==> False, where each li is a literal (see also comments in cnf_funcs.ML). -- observe that this is the "dualized" version of the standard clausal form l1' \/ l2' \/ ... \/ lm', where li is the negation normal form of ~li'. 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. 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: zChaff version 2004.11.15 - zChaff must have been compiled with proof generation enabled (#define VERIFY_ON). *) signature SAT = sig val trace_sat : bool ref (* print trace messages *) val sat_tac : Tactical.tactic val satx_tac : Tactical.tactic end functor SATFunc (structure cnf : CNF) : SAT = struct val trace_sat = ref false; val counter = ref 0; (* ------------------------------------------------------------------------- *) (* rev_lookup: look up the Isabelle/HOL atom corresponding to a DIMACS *) (* variable index in the dictionary. This index should exist in the *) (* dictionary, otherwise exception Option is raised. *) (* ------------------------------------------------------------------------- *) (* 'b -> ('a * 'b) list -> 'a *) fun rev_lookup idx [] = raise Option | rev_lookup idx ((key, entry)::dict) = if entry=idx then key else rev_lookup idx dict; (* ------------------------------------------------------------------------- *) (* swap_prem: convert rules of the form *) (* l1 ==> l2 ==> .. ==> li ==> .. ==> False *) (* to *) (* l1 ==> l2 ==> .... ==> ~li *) (* ------------------------------------------------------------------------- *) fun swap_prem rslv c = let val thm1 = rule_by_tactic (metacut_tac c 1 THEN (atac 1) THEN (REPEAT_SOME atac)) rslv in rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1 end; (* ------------------------------------------------------------------------- *) (* is_dual: check if two atoms are dual to each other *) (* ------------------------------------------------------------------------- *) (* Term.term -> Term.term -> bool *) fun is_dual (Const ("Trueprop", _) $ x) y = is_dual x y | is_dual x (Const ("Trueprop", _) $ y) = is_dual x y | is_dual (Const ("Not", _) $ x) y = (x = y) | is_dual x (Const ("Not", _) $ y) = (x = y) | is_dual x y = false; (* ------------------------------------------------------------------------- *) (* dual_mem: check if an atom has a dual in a list of atoms *) (* ------------------------------------------------------------------------- *) (* Term.term -> Term.term list -> bool *) fun dual_mem x [] = false | dual_mem x (y::ys) = is_dual x y orelse dual_mem x ys; (* ------------------------------------------------------------------------- *) (* replay_chain: proof reconstruction: given two clauses *) (* [| x1 ; .. ; a ; .. ; xn |] ==> False *) (* and *) (* [| y1 ; .. ; ~a ; .. ; ym |] ==> False , *) (* we first convert the first clause into *) (* [| x1 ; ... ; xn |] ==> ~a (using swap_prem) *) (* and do a resolution with the second clause to produce *) (* [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False *) (* ------------------------------------------------------------------------- *) (* Theory.theory -> Thm.thm option Array.array -> int -> int list -> unit *) fun replay_chain sg clauses idx (c::cs) = let val fc = (valOf o Array.sub) (clauses, c) fun strip_neg (Const ("Trueprop", _) $ x) = strip_neg x | strip_neg (Const ("Not", _) $ x) = x | strip_neg x = x (* find out which atom (literal) is used in the resolution *) fun res_atom [] _ = raise THM ("Proof reconstruction failed!", 0, []) | res_atom (x::xs) ys = if dual_mem x ys then strip_neg x else res_atom xs ys fun replay old [] = old | replay old (cl::cls) = let val icl = (valOf o Array.sub) (clauses, cl) val var = res_atom (prems_of old) (prems_of icl) val atom = cterm_of sg var val rslv = instantiate' [] [SOME atom] notI val _ = if !trace_sat then tracing ("Resolving clause: " ^ string_of_thm old ^ "\nwith clause: " ^ string_of_thm icl ^ "\nusing literal " ^ string_of_cterm atom ^ ".") else () val thm1 = (rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icl handle THM _ => rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icl))) old) val new = rule_by_tactic distinct_subgoals_tac thm1 val _ = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm new) else () val _ = inc counter in replay new cls end val _ = Array.update (clauses, idx, SOME (replay fc cs)) val _ = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int idx) else () in () end; (* ------------------------------------------------------------------------- *) (* replay_proof: replay the resolution proof returned by the SAT solver; cf. *) (* SatSolver.proof for details of the proof format. Returns the *) (* theorem established by the proof (which is just False). *) (* ------------------------------------------------------------------------- *) (* Theory.theory -> Thm.thm option Array.array -> SatSolver.proof -> Thm.thm *) fun replay_proof sg clauses (clause_table, empty_id) = let (* int -> unit *) fun prove_clause id = case Array.sub (clauses, id) of SOME _ => () | NONE => let val ids = valOf (Inttab.lookup clause_table id) val _ = map prove_clause ids in replay_chain sg clauses id ids end val _ = counter := 0 val _ = prove_clause empty_id val _ = if !trace_sat then tracing (string_of_int (!counter) ^ " resolution step(s) total.") else () in (valOf o Array.sub) (clauses, empty_id) end; (* ------------------------------------------------------------------------- *) (* Functions to build the sat tactic *) (* ------------------------------------------------------------------------- *) fun collect_atoms (Const ("Trueprop", _) $ x) ls = collect_atoms x ls | collect_atoms (Const ("op |", _) $ x $ y) ls = collect_atoms x (collect_atoms y ls) | collect_atoms x ls = x ins ls; fun has_duals [] = false | has_duals (x::xs) = dual_mem x xs orelse has_duals xs; fun is_trivial_clause (Const ("True", _)) = true | is_trivial_clause c = has_duals (collect_atoms c []); (* ------------------------------------------------------------------------- *) (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) (* a proof from the resulting proof trace of the SAT solver. *) (* ------------------------------------------------------------------------- *) fun rawsat_thm sg prems = let val thms = filter (not o is_trivial_clause o term_of o cprop_of) prems (* remove trivial clauses *) val (fm, dict) = cnf.cnf2prop thms val _ = if !trace_sat then tracing "Invoking SAT solver ..." else () in case SatSolver.invoke_solver "zchaff_with_proofs" fm of SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => let val _ = if !trace_sat then tracing ("Proof trace from SAT solver:\n" ^ "clauses: [" ^ commas (map (fn (c, cs) => "(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^ "empty clause: " ^ string_of_int empty_id) else () val raw_thms = cnf.cnf2raw_thms thms val raw_thms' = map (rule_by_tactic distinct_subgoals_tac) raw_thms (* initialize the clause array with the original clauses *) val max_idx = valOf (Inttab.max_key clause_table) val clauses = Array.array (max_idx + 1, NONE) val _ = fold (fn thm => fn idx => (Array.update (clauses, idx, SOME thm); idx+1)) raw_thms' 0 in replay_proof sg clauses (clause_table, empty_id) end | SatSolver.UNSATISFIABLE NONE => raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) | SatSolver.SATISFIABLE assignment => let val msg = "SAT solver found a countermodel:\n" ^ (enclose "{" "}" o commas o map (Sign.string_of_term sg o fst) o filter (fn (_, idx) => getOpt (assignment idx, false))) dict in raise THM (msg, 0, []) end | SatSolver.UNKNOWN => raise THM ("SAT solver failed to decide the formula", 0, []) end; (* ------------------------------------------------------------------------- *) (* Tactics *) (* ------------------------------------------------------------------------- *) fun cnfsat_basic_tac state = let val sg = Thm.sign_of_thm state in METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state end; (* a trivial tactic, used in preprocessing before calling the main tactic *) val pre_sat_tac = (REPEAT (etac conjE 1)) THEN (REPEAT ((atac 1) ORELSE (etac FalseE 1))); (* tactic for calling external SAT solver, taking as input CNF clauses *) val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac); (* tactic for calling external SAT solver, taking as input arbitrary formula *) val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac; (* Tactic for calling external SAT solver, taking as input arbitrary formula. The input is translated to CNF (in primitive form), possibly introducing new literals. *) val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac; end; (* of structure *)