src/HOL/Tools/sat_solver.ML

 signature SAT_SOLVER =
 sig
 	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
 
 	(* auxiliary functions to create external SAT solvers *)
 	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit

 (* ------------------------------------------------------------------------- *)
 
 	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;
 
 (* ------------------------------------------------------------------------- *)
 (* type of SAT solvers: given a propositional formula, a satisfying          *)
 (*      assignment may be returned                                           *)

 		val number_of_vars    = maxidx fm'
 		val number_of_clauses = cnf_number_of_clauses fm'
 	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');
 		File.append path
 			" 0\n"

 		end
 		val number_of_vars = Int.max (maxidx fm, 1)
 	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
 			(sat_string fm);
 		File.append path

 			UNKNOWN
 		  | parse_lines (line::lines) =
 			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
 		(parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path
 	end;

 			if PropLogic.eval (assignment_from_list xs) fm then
 				SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
 			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 []
 	end
 in

 		open PropLogic
 	in
 		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'
 			(* int list -> int -> prop_formula *)
 			fun partial_var_eval []      i = BoolVar i

 				else assignment_from_list xs i
 		in
 			(* 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
 	SatSolver.add_solver ("dpll", dpll_solver)
 end;

 
 (* ------------------------------------------------------------------------- *)
 (* 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
 		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
 		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso