--- 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'
--- 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