# HG changeset patch # User webertj # Date 1127166359 -7200 # Node ID cf8713d880b1141e2e90ade9a283e6c15f4ac7ba # Parent 714c95aab8bc742da64029741f492a2cf0a7294b SAT solver interface modified to support proofs of unsatisfiability diff -r 714c95aab8bc -r cf8713d880b1 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Mon Sep 19 23:23:51 2005 +0200 +++ b/src/HOL/Tools/refute.ML Mon Sep 19 23:45:59 2005 +0200 @@ -986,7 +986,7 @@ SatSolver.SATISFIABLE assignment => (writeln " model found!"; writeln ("*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of SOME b => b | NONE => true))) - | SatSolver.UNSATISFIABLE => + | SatSolver.UNSATISFIABLE _ => (immediate_output " no model exists.\n"; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' diff -r 714c95aab8bc -r cf8713d880b1 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Mon Sep 19 23:23:51 2005 +0200 +++ b/src/HOL/Tools/sat_solver.ML Mon Sep 19 23:45:59 2005 +0200 @@ -11,8 +11,9 @@ exception NOT_CONFIGURED type assignment = int -> bool option + type proof = int list Inttab.table * int datatype result = SATISFIABLE of assignment - | UNSATISFIABLE + | UNSATISFIABLE of proof option | UNKNOWN type solver = PropLogic.prop_formula -> result @@ -50,12 +51,30 @@ type assignment = int -> bool option; (* ------------------------------------------------------------------------- *) +(* a proof of unsatisfiability, to be interpreted as follows: each integer *) +(* is a clause ID, each list 'xs' stored under the key 'x' in the table *) +(* contains the IDs of clauses that must be resolved (in the given *) +(* order) to obtain the new clause 'x'. Each list 'xs' must be *) +(* non-empty, and the literal to be resolved upon must always be unique *) +(* (e.g. "A | ~B" must not be resolved with "~A| B"). Circular *) +(* dependencies of clauses are not allowed. (At least) one of the *) +(* clauses in the table must be the empty clause (i.e. contain no *) +(* literals); its ID is given by the second component of the proof. *) +(* The clauses of the original problem passed to the SAT solver have *) +(* consecutive IDs starting with 0. Clause IDs must be non-negative, *) +(* but do not need to be consecutive. *) +(* ------------------------------------------------------------------------- *) + + type proof = int list Inttab.table * int; + +(* ------------------------------------------------------------------------- *) (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) -(* assignment must be returned as well *) +(* assignment must be returned as well; if the result is *) +(* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) (* ------------------------------------------------------------------------- *) datatype result = SATISFIABLE of assignment - | UNSATISFIABLE + | UNSATISFIABLE of proof option | UNKNOWN; (* ------------------------------------------------------------------------- *) @@ -117,7 +136,6 @@ in File.write path ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ - "c (c) Tjark Weber\n" ^ "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); File.append_list path (cnf_string fm'); @@ -173,7 +191,6 @@ in File.write path ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ - "c (c) Tjark Weber\n" ^ "p sat " ^ string_of_int number_of_vars ^ "\n" ^ "("); File.append_list path @@ -237,7 +254,7 @@ if is_substring satisfiable line then SATISFIABLE (parse_assignment [] lines) else if is_substring unsatisfiable line then - UNSATISFIABLE + UNSATISFIABLE NONE else parse_lines lines in @@ -394,7 +411,7 @@ else (case next_list xs indices of SOME xs' => solver_loop xs' - | NONE => SatSolver.UNSATISFIABLE) + | NONE => SatSolver.UNSATISFIABLE NONE) in (* start with the "first" assignment (all variables are interpreted as 'false') *) solver_loop [] @@ -416,8 +433,8 @@ fun dpll_solver fm = let (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) - (* but that sometimes introduces more boolean variables than we can *) - (* handle efficiently. *) + (* but that sometimes leads to worse performance due to the *) + (* introduction of additional variables. *) val fm' = PropLogic.nnf fm (* int list *) val indices = PropLogic.indices fm' @@ -485,7 +502,7 @@ (* initially, no variable is interpreted yet *) case dpll [] fm' of SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) - | NONE => SatSolver.UNSATISFIABLE + | NONE => SatSolver.UNSATISFIABLE NONE end end (* local *) in @@ -527,6 +544,128 @@ (* zChaff (http://www.princeton.edu/~chaff/zchaff.html) *) (* ------------------------------------------------------------------------- *) +(* ------------------------------------------------------------------------- *) +(* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if *) +(* zChaff finds that the formula is unsatisfiable, a proof of this is read *) +(* from a file "resolve_trace" that was generated by zChaff. See the code *) +(* below for the expected format of the "resolve_trace" file. Aside from *) +(* some basic syntactic checks, no verification of the proof is performed. *) +(* ------------------------------------------------------------------------- *) + +(* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so *) +(* that the latter is preferred by the "auto" solver *) + +let + exception INVALID_PROOF of string + fun zchaff_with_proofs fm = + case SatSolver.invoke_solver "zchaff" fm of + SatSolver.UNSATISFIABLE NONE => + (let + (* string list *) + val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace")) + handle _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" + val _ = try File.rm (Path.unpack "resolve_trace") + (* PropLogic.prop_formula -> int *) + fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 + | cnf_number_of_clauses _ = 1 + (* string -> int *) + fun int_from_string s = ( + case Int.fromString s of + SOME i => i + | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") + ) + (* parse the "resolve_trace" file *) + (* int ref *) + val clause_offset = ref ~1 + (* string list -> proof -> proof *) + fun process_tokens [] proof = + proof + | process_tokens (tok::toks) (clause_table, conflict_id) = + if tok="CL:" then ( + case toks of + id::sep::ids => + let + val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") + val cid = int_from_string id + val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") + val rs = map int_from_string ids + in + (* update clause table *) + (Inttab.update_new ((cid, rs), clause_table), conflict_id) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") + end + | _ => + raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." + ) else if tok="VAR:" then ( + case toks of + id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => + let + (* set 'clause_offset' to the largest used clause ID *) + val _ = if !clause_offset = ~1 then clause_offset := + (case Inttab.max_key clause_table of + SOME id => id + | NONE => cnf_number_of_clauses (PropLogic.defcnf fm)) + else + () + val vid = int_from_string id + val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") + val _ = int_from_string levid + val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") + val _ = int_from_string valid + val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") + val aid = int_from_string anteid + val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") + val ls = map int_from_string lits + (* convert the data provided by zChaff to our resolution-style proof format *) + (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) + (* given by the literals in the antecedent clause *) + (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) + val cid = !clause_offset + vid + (* the low bit of each literal gives its sign (positive/negative), therefore *) + (* we have to divide each literal by 2 to obtain the proper variable ID; then *) + (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) + val vids = filter (not_equal vid) (map (fn l => l div 2) ls) + val rs = aid :: map (fn v => !clause_offset + v) vids + in + (* update clause table *) + (Inttab.update_new ((cid, rs), clause_table), conflict_id) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (antecedent for variable " ^ id ^ ") defined more than once.") + end + | _ => + raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." + ) else if tok="CONF:" then ( + case toks of + id::sep::ids => + let + val cid = int_from_string id + val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") + val _ = map int_from_string ids + val _ = if conflict_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." + in + (* update conflict id *) + (clause_table, cid) + end + | _ => + raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." + ) else + raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") + (* string list -> proof -> proof *) + fun process_lines [] proof = + proof + | process_lines (l::ls) proof = + process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof) + (* proof *) + val (clause_table, conflict_id) = process_lines proof_lines (Inttab.empty, ~1) + val _ = if conflict_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." + in + SatSolver.UNSATISFIABLE (SOME (clause_table, conflict_id)) + end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) + | result => + result +in + SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) +end; + let fun zchaff fm = let