src/HOL/Tools/sat_solver.ML
author webertj
Wed May 26 17:42:46 2004 +0200 (2004-05-26)
changeset 14805 eff7b9df27e9
parent 14753 f40b45db8cf0
child 14965 7155b319eafa
permissions -rw-r--r--
solver "auto" now issues a warning when it uses solver "enumerate"
     1 (*  Title:      HOL/Tools/sat_solver.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2004
     5 
     6 Interface to external SAT solvers, and (simple) built-in SAT solvers.
     7 *)
     8 
     9 signature SAT_SOLVER =
    10 sig
    11 	type solver  (* PropLogic.prop_formula -> (int -> bool) option option *)
    12 
    13 	(* external SAT solvers *)
    14 	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
    15 	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
    16 	val parse_std_result_file : Path.T -> string -> (int -> bool) option
    17 	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option)
    18 			-> PropLogic.prop_formula -> (int -> bool) option
    19 
    20 	(* generic interface *)
    21 	val solvers       : (string * solver) list ref
    22 	val add_solver    : string * solver -> unit
    23 	val invoke_solver : string -> solver  (* exception OPTION *)
    24 end;
    25 
    26 structure SatSolver : SAT_SOLVER =
    27 struct
    28 
    29 	open PropLogic;
    30 
    31 (* ------------------------------------------------------------------------- *)
    32 (* Type of SAT solvers: given a propositional formula, a satisfying          *)
    33 (*      assignment may be returned                                           *)
    34 (*      - 'Some None' means that no satisfying assignment was found          *)
    35 (*      - 'None' means that the solver was not configured/installed properly *)
    36 (* ------------------------------------------------------------------------- *)
    37 
    38 	type solver = prop_formula -> (int -> bool) option option;
    39 
    40 (* ------------------------------------------------------------------------- *)
    41 (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
    42 (*      to a file in DIMACS CNF format (see "Satisfiability Suggested        *)
    43 (*      Format", May 8 1993, Section 2.1)                                    *)
    44 (* Note: 'fm' must not contain a variable index less than 1.                 *)
    45 (* Note: 'fm' is converted into (definitional) CNF.                          *)
    46 (* ------------------------------------------------------------------------- *)
    47 
    48 	(* Path.T -> prop_formula -> unit *)
    49 
    50 	fun write_dimacs_cnf_file path fm =
    51 	let
    52 		(* prop_formula -> prop_formula *)
    53 		fun cnf_True_False_elim True =
    54 			Or (BoolVar 1, Not (BoolVar 1))
    55 		  | cnf_True_False_elim False =
    56 			And (BoolVar 1, Not (BoolVar 1))
    57 		  | cnf_True_False_elim fm =
    58 			fm  (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *)
    59 		(* prop_formula -> int *)
    60 		fun cnf_number_of_clauses (And (fm1,fm2)) =
    61 			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
    62 		  | cnf_number_of_clauses _ =
    63 			1
    64 		(* prop_formula -> string *)
    65 		fun cnf_string True =
    66 			error "formula is not in CNF"
    67 		  | cnf_string False =
    68 			error "formula is not in CNF"
    69 		  | cnf_string (BoolVar i) =
    70 			(assert (i>=1) "formula contains a variable index less than 1";
    71 			string_of_int i)
    72 		  | cnf_string (Not fm) =
    73 			"-" ^ (cnf_string fm)
    74 		  | cnf_string (Or (fm1,fm2)) =
    75 			(cnf_string fm1) ^ " " ^ (cnf_string fm2)
    76 		  | cnf_string (And (fm1,fm2)) =
    77 			(cnf_string fm1) ^ " 0\n" ^ (cnf_string fm2)
    78 	in
    79 		File.write path
    80 			(let
    81 				val cnf               = (cnf_True_False_elim o defcnf) fm  (* conversion into def. CNF *)
    82 				val number_of_vars    = maxidx cnf
    83 				val number_of_clauses = cnf_number_of_clauses cnf
    84 			in
    85 				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
    86 				"c (c) Tjark Weber\n" ^
    87 				"p cnf " ^ (string_of_int number_of_vars) ^ " " ^ (string_of_int number_of_clauses) ^ "\n" ^
    88 				(cnf_string cnf) ^ "\n"
    89 			end)
    90 	end;
    91 
    92 (* ------------------------------------------------------------------------- *)
    93 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)
    94 (*      to a file in DIMACS SAT format (see "Satisfiability Suggested        *)
    95 (*      Format", May 8 1993, Section 2.2)                                    *)
    96 (* Note: 'fm' must not contain a variable index less than 1.                 *)
    97 (* ------------------------------------------------------------------------- *)
    98 
    99 	(* Path.T -> prop_formula -> unit *)
   100 
   101 	fun write_dimacs_sat_file path fm =
   102 	let
   103 		(* prop_formula -> string *)
   104 		fun sat_string True =
   105 			"*()"
   106 		  | sat_string False =
   107 			"+()"
   108 		  | sat_string (BoolVar i) =
   109 			(assert (i>=1) "formula contains a variable index less than 1";
   110 			string_of_int i)
   111 		  | sat_string (Not fm) =
   112 			"-(" ^ (sat_string fm) ^ ")"
   113 		  | sat_string (Or (fm1,fm2)) =
   114 			"+(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
   115 		  | sat_string (And (fm1,fm2)) =
   116 			"*(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
   117 	in
   118 		File.write path
   119 			(let
   120 				val number_of_vars = Int.max (maxidx fm, 1)
   121 			in
   122 				"c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
   123 				"c (c) Tjark Weber\n" ^
   124 				"p sat " ^ (string_of_int number_of_vars) ^ "\n" ^
   125 				"(" ^ (sat_string fm) ^ ")\n"
   126 			end)
   127 	end;
   128 
   129 (* ------------------------------------------------------------------------- *)
   130 (* parse_std_result_file: scans a SAT solver's output file for a satisfying  *)
   131 (*      variable assignment.  Returns the assignment, or 'None' if the SAT   *)
   132 (*      solver did not find one.  The file format must be as follows:        *)
   133 (*      ,-----                                                               *)
   134 (*      | 0 or more lines not containing 'success'                           *)
   135 (*      | A line containing 'success' as a substring                         *)
   136 (*      | A line ASSIGNMENT containing integers, separated by " "            *)
   137 (*      | 0 or more lines                                                    *)
   138 (*      `-----                                                               *)
   139 (*      If variable i is contained in ASSIGNMENT, then i is interpreted as   *)
   140 (*      'true'.  If ~i is contained in ASSIGNMENT, then i is interpreted as  *)
   141 (*      'false'.                                                             *)
   142 (* ------------------------------------------------------------------------- *)
   143 
   144 	(* Path.T -> string -> (int -> bool) option *)
   145 
   146 	fun parse_std_result_file path success =
   147 	let
   148 		(* 'a option -> 'a Library.option *)
   149 		fun option (SOME a) =
   150 			Some a
   151 		  | option NONE =
   152 			None
   153 		(* string -> int list *)
   154 		fun int_list_from_string s =
   155 			mapfilter (option o Int.fromString) (space_explode " " s)
   156 		(* int list -> int -> bool *)
   157 		fun assignment_from_list [] i =
   158 			false  (* could be 'true' just as well; the SAT solver didn't provide a value for this variable *)
   159 		  | assignment_from_list (x::xs) i =
   160 			if x=i then true
   161 			else if x=(~i) then false
   162 			else assignment_from_list xs i
   163 		(* string -> string -> bool *)
   164 		fun is_substring needle haystack =
   165 		let
   166 			val length1 = String.size needle
   167 			val length2 = String.size haystack
   168 		in
   169 			if length2 < length1 then
   170 				false
   171 			else if needle = String.substring (haystack, 0, length1) then
   172 				true
   173 			else is_substring needle (String.substring (haystack, 1, length2-1))
   174 		end
   175 		(* string list -> int list option *)
   176 		fun parse_lines [] =
   177 			None
   178 		  | parse_lines (line::lines) =
   179 			if is_substring success line then
   180 				(* the next line must be a list of integers *)
   181 				(Some o assignment_from_list o int_list_from_string o hd) lines
   182 			else
   183 				parse_lines lines
   184 	in
   185 		(parse_lines o split_lines o File.read) path
   186 	end;
   187 
   188 (* ------------------------------------------------------------------------- *)
   189 (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
   190 (* ------------------------------------------------------------------------- *)
   191 
   192 	(* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> prop_formula -> (int -> bool) option *)
   193 
   194 	fun make_external_solver cmd writefn readfn fm =
   195 		(writefn fm;
   196 		assert ((system cmd)=0) ("system command " ^ quote cmd ^ " failed (make sure the SAT solver is installed)");
   197 		readfn ());
   198 
   199 (* ------------------------------------------------------------------------- *)
   200 (* solvers: a (reference to a) table of all registered SAT solvers           *)
   201 (* ------------------------------------------------------------------------- *)
   202 
   203 	val solvers = ref ([] : (string * solver) list);
   204 
   205 (* ------------------------------------------------------------------------- *)
   206 (* add_solver: updates 'solvers' by adding a new solver                      *)
   207 (* ------------------------------------------------------------------------- *)
   208 
   209 	(* string * solver -> unit *)
   210 
   211 	fun add_solver (name, new_solver) =
   212 		(solvers := overwrite_warn (!solvers, (name, new_solver)) ("SAT solver " ^ quote name ^ " was defined before"));
   213 
   214 (* ------------------------------------------------------------------------- *)
   215 (* invoke_solver: returns the solver associated with the given 'name'        *)
   216 (* Note: If no solver is associated with 'name', exception 'OPTION' will be  *)
   217 (*       raised.                                                             *)
   218 (* ------------------------------------------------------------------------- *)
   219 
   220 	(* string -> solver *)
   221 
   222 	fun invoke_solver name =
   223 		(the o assoc) (!solvers, name);
   224 
   225 end;  (* SatSolver *)
   226 
   227 
   228 (* ------------------------------------------------------------------------- *)
   229 (* Predefined SAT solvers                                                    *)
   230 (* ------------------------------------------------------------------------- *)
   231 
   232 (* ------------------------------------------------------------------------- *)
   233 (* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"'   *)
   234 (* -- simply enumerates assignments until a satisfying assignment is found   *)
   235 (* ------------------------------------------------------------------------- *)
   236 
   237 let
   238 	fun enum_solver fm =
   239 	let
   240 		(* int list *)
   241 		val indices = PropLogic.indices fm
   242 		(* int list -> int list -> int list option *)
   243 		(* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
   244 		fun next_list _ ([]:int list) =
   245 			None
   246 		  | next_list [] (y::ys) =
   247 			Some [y]
   248 		  | next_list (x::xs) (y::ys) =
   249 			if x=y then
   250 				(* reset the bit, continue *)
   251 				next_list xs ys
   252 			else
   253 				(* set the lowest bit that wasn't set before, keep the higher bits *)
   254 				Some (y::x::xs)
   255 		(* int list -> int -> bool *)
   256 		fun assignment_from_list xs i =
   257 			i mem xs
   258 		(* int list -> (int -> bool) option *)
   259 		fun solver_loop xs =
   260 			if PropLogic.eval (assignment_from_list xs) fm then
   261 				Some (assignment_from_list xs)
   262 			else
   263 				(case next_list xs indices of
   264 				  Some xs' => solver_loop xs'
   265 				| None     => None)
   266 	in
   267 		(* start with the "first" assignment (all variables are interpreted as 'False') *)
   268 		solver_loop []
   269 	end
   270 in
   271 	SatSolver.add_solver ("enumerate", Some o enum_solver)
   272 end;
   273 
   274 (* ------------------------------------------------------------------------- *)
   275 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a   *)
   276 (* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
   277 (* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1).  *)
   278 (* ------------------------------------------------------------------------- *)
   279 
   280 let
   281 	local
   282 		open PropLogic
   283 	in
   284 		fun dpll_solver fm =
   285 		let
   286 			(* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
   287 			(* sometimes introduces more boolean variables than we can handle   *)
   288 			(* efficiently.                                                     *)
   289 			val fm' = PropLogic.nnf fm
   290 			(* int list *)
   291 			val indices = PropLogic.indices fm'
   292 			(* int list -> int -> prop_formula *)
   293 			fun partial_var_eval []      i = BoolVar i
   294 			  | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
   295 			(* int list -> prop_formula -> prop_formula *)
   296 			fun partial_eval xs True             = True
   297 			  | partial_eval xs False            = False
   298 			  | partial_eval xs (BoolVar i)      = partial_var_eval xs i
   299 			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
   300 			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
   301 			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
   302 			(* prop_formula -> int list *)
   303 			fun forced_vars True              = []
   304 			  | forced_vars False             = []
   305 			  | forced_vars (BoolVar i)       = [i]
   306 			  | forced_vars (Not (BoolVar i)) = [~i]
   307 			  | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
   308 			  | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
   309 			  (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   310 			  (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   311 			  | forced_vars _                 = raise ERROR  (* formula is not in negation normal form *)
   312 			(* int list -> prop_formula -> (int list * prop_formula) *)
   313 			fun eval_and_force xs fm =
   314 			let
   315 				val fm' = partial_eval xs fm
   316 				val xs' = forced_vars fm'
   317 			in
   318 				if null xs' then
   319 					(xs, fm')
   320 				else
   321 					eval_and_force (xs@xs') fm'  (* xs and xs' should be distinct, so '@' here should have *)
   322 					                             (* the same effect as 'union_int'                         *)
   323 			end
   324 			(* int list -> int option *)
   325 			fun fresh_var xs =
   326 				Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices
   327 			(* int list -> prop_formula -> int list option *)
   328 			(* partial assignment 'xs' *)
   329 			fun dpll xs fm =
   330 			let
   331 				val (xs', fm') = eval_and_force xs fm
   332 			in
   333 				case fm' of
   334 				  True  => Some xs'
   335 				| False => None
   336 				| _     =>
   337 					let
   338 						val x = the (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
   339 					in
   340 						case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
   341 						  Some xs'' => Some xs''
   342 						| None      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
   343 					end
   344 			end
   345 			(* int list -> int -> bool *)
   346 			fun assignment_from_list [] i =
   347 				false  (* could be 'true' just as well; the DPLL procedure didn't provide a value for this variable *)
   348 			  | assignment_from_list (x::xs) i =
   349 				if x=i then true
   350 				else if x=(~i) then false
   351 				else assignment_from_list xs i
   352 		in
   353 			(* initially, no variable is interpreted yet *)
   354 			apsome assignment_from_list (dpll [] fm')
   355 		end
   356 	end  (* local *)
   357 in
   358 	SatSolver.add_solver ("dpll", Some o dpll_solver)
   359 end;
   360 
   361 (* ------------------------------------------------------------------------- *)
   362 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
   363 (* the first installed solver (other than "auto" itself)                     *)
   364 (* ------------------------------------------------------------------------- *)
   365 
   366 let
   367 	fun auto_solver fm =
   368 		get_first (fn (name,solver) =>
   369 			if name="auto" then
   370 				None
   371 			else
   372 				((if name="dpll" orelse name="enumerate" then
   373 					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
   374 				else
   375 					());
   376 				solver fm)) (rev (!SatSolver.solvers))
   377 in
   378 	SatSolver.add_solver ("auto", auto_solver)
   379 end;
   380 
   381 (* ------------------------------------------------------------------------- *)
   382 (* ZChaff, Version 2003.12.04                                                *)
   383 (* ------------------------------------------------------------------------- *)
   384 
   385 let
   386 	fun zchaff fm =
   387 	let
   388 		val inname     = "isabelle.cnf"
   389 		val outname    = "result"
   390 		val inpath     = File.tmp_path (Path.unpack inname)
   391 		val outpath    = File.tmp_path (Path.unpack outname)
   392 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   393 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   394 		fun readfn ()  = SatSolver.parse_std_result_file outpath "Verify Solution successful. Instance satisfiable"
   395 		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   396 		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   397 		val assignment = SatSolver.make_external_solver cmd writefn readfn fm
   398 		val _          = (File.rm inpath handle _ => ())
   399 		val _          = (File.rm outpath handle _ => ())
   400 	in
   401 		assignment
   402 	end
   403 in
   404 		SatSolver.add_solver ("zchaff", (fn fm => if getenv "ZCHAFF_HOME" <> "" then Some (zchaff fm) else None))
   405 end;
   406 
   407 (* ------------------------------------------------------------------------- *)
   408 (* Add code for other SAT solvers below.                                     *)
   409 (* ------------------------------------------------------------------------- *)
   410 
   411 (*
   412 let
   413 	fun mysolver fm = ...
   414 in
   415 	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_installed then Some (mysolver fm) else None));  -- register the solver
   416 end;
   417 
   418 -- the solver is now available as SatSolver.invoke_solver "myname"
   419 *)