1(* Title: HOL/Tools/sat_solver.ML 2 Author: Tjark Weber 3 Copyright 2004-2009 4 5Interface to external SAT solvers, and (simple) built-in SAT solvers. 6 7Relevant Isabelle environment settings: 8 9 # MiniSat 1.14 10 #MINISAT_HOME=/usr/local/bin 11 12 # zChaff 13 #ZCHAFF_HOME=/usr/local/bin 14 15 # BerkMin561 16 #BERKMIN_HOME=/usr/local/bin 17 #BERKMIN_EXE=BerkMin561-linux 18 #BERKMIN_EXE=BerkMin561-solaris 19 20 # Jerusat 1.3 21 #JERUSAT_HOME=/usr/local/bin 22*) 23 24signature SAT_SOLVER = 25sig 26 exception NOT_CONFIGURED 27 28 type assignment = int -> bool option 29 type proof = int list Inttab.table * int 30 datatype result = SATISFIABLE of assignment 31 | UNSATISFIABLE of proof option 32 | UNKNOWN 33 type solver = Prop_Logic.prop_formula -> result 34 35 (* auxiliary functions to create external SAT solvers *) 36 val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit 37 val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit 38 val read_std_result_file : Path.T -> string * string * string -> result 39 val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) -> 40 (unit -> result) -> solver 41 42 val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula 43 44 (* generic solver interface *) 45 val get_solvers : unit -> (string * solver) list 46 val add_solver : string * solver -> unit 47 val invoke_solver : string -> solver (* exception Option *) 48end; 49 50structure SAT_Solver : SAT_SOLVER = 51struct 52 53 open Prop_Logic; 54 55(* ------------------------------------------------------------------------- *) 56(* should be raised by an external SAT solver to indicate that the solver is *) 57(* not configured properly *) 58(* ------------------------------------------------------------------------- *) 59 60 exception NOT_CONFIGURED; 61 62(* ------------------------------------------------------------------------- *) 63(* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is *) 64(* a satisfying assignment regardless of the value of variable 'i' *) 65(* ------------------------------------------------------------------------- *) 66 67 type assignment = int -> bool option; 68 69(* ------------------------------------------------------------------------- *) 70(* a proof of unsatisfiability, to be interpreted as follows: each integer *) 71(* is a clause ID, each list 'xs' stored under the key 'x' in the table *) 72(* contains the IDs of clauses that must be resolved (in the given *) 73(* order) to obtain the new clause 'x'. Each list 'xs' must be *) 74(* non-empty, and the literal to be resolved upon must always be unique *) 75(* (e.g. "A | ~B" must not be resolved with "~A | B"). Circular *) 76(* dependencies of clauses are not allowed. (At least) one of the *) 77(* clauses in the table must be the empty clause (i.e. contain no *) 78(* literals); its ID is given by the second component of the proof. *) 79(* The clauses of the original problem passed to the SAT solver have *) 80(* consecutive IDs starting with 0. Clause IDs must be non-negative, *) 81(* but do not need to be consecutive. *) 82(* ------------------------------------------------------------------------- *) 83 84 type proof = int list Inttab.table * int; 85 86(* ------------------------------------------------------------------------- *) 87(* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) 88(* assignment must be returned as well; if the result is *) 89(* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) 90(* ------------------------------------------------------------------------- *) 91 92 datatype result = SATISFIABLE of assignment 93 | UNSATISFIABLE of proof option 94 | UNKNOWN; 95 96(* ------------------------------------------------------------------------- *) 97(* type of SAT solvers: given a propositional formula, a satisfying *) 98(* assignment may be returned *) 99(* ------------------------------------------------------------------------- *) 100 101 type solver = prop_formula -> result; 102 103(* ------------------------------------------------------------------------- *) 104(* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) 105(* to a file in DIMACS CNF format (see "Satisfiability Suggested *) 106(* Format", May 8 1993, Section 2.1) *) 107(* Note: 'fm' must not contain a variable index less than 1. *) 108(* Note: 'fm' must be given in CNF. *) 109(* ------------------------------------------------------------------------- *) 110 111 fun write_dimacs_cnf_file path fm = 112 let 113 fun cnf_True_False_elim True = 114 Or (BoolVar 1, Not (BoolVar 1)) 115 | cnf_True_False_elim False = 116 And (BoolVar 1, Not (BoolVar 1)) 117 | cnf_True_False_elim fm = 118 fm (* since 'fm' is in CNF, either 'fm'='True'/'False', 119 or 'fm' does not contain 'True'/'False' at all *) 120 fun cnf_number_of_clauses (And (fm1, fm2)) = 121 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) 122 | cnf_number_of_clauses _ = 123 1 124 fun write_cnf_file out = 125 let 126 fun write_formula True = 127 error "formula is not in CNF" 128 | write_formula False = 129 error "formula is not in CNF" 130 | write_formula (BoolVar i) = 131 (i>=1 orelse error "formula contains a variable index less than 1"; 132 File.output out (string_of_int i)) 133 | write_formula (Not (BoolVar i)) = 134 (File.output out "-"; 135 write_formula (BoolVar i)) 136 | write_formula (Not _) = 137 error "formula is not in CNF" 138 | write_formula (Or (fm1, fm2)) = 139 (write_formula fm1; 140 File.output out " "; 141 write_formula fm2) 142 | write_formula (And (fm1, fm2)) = 143 (write_formula fm1; 144 File.output out " 0\n"; 145 write_formula fm2) 146 val fm' = cnf_True_False_elim fm 147 val number_of_vars = maxidx fm' 148 val number_of_clauses = cnf_number_of_clauses fm' 149 in 150 File.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n"; 151 File.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^ 152 string_of_int number_of_clauses ^ "\n"); 153 write_formula fm'; 154 File.output out " 0\n" 155 end 156 in 157 File.open_output write_cnf_file path 158 end; 159 160(* ------------------------------------------------------------------------- *) 161(* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) 162(* to a file in DIMACS SAT format (see "Satisfiability Suggested *) 163(* Format", May 8 1993, Section 2.2) *) 164(* Note: 'fm' must not contain a variable index less than 1. *) 165(* ------------------------------------------------------------------------- *) 166 167 fun write_dimacs_sat_file path fm = 168 let 169 fun write_sat_file out = 170 let 171 fun write_formula True = 172 File.output out "*()" 173 | write_formula False = 174 File.output out "+()" 175 | write_formula (BoolVar i) = 176 (i>=1 orelse error "formula contains a variable index less than 1"; 177 File.output out (string_of_int i)) 178 | write_formula (Not (BoolVar i)) = 179 (File.output out "-"; 180 write_formula (BoolVar i)) 181 | write_formula (Not fm) = 182 (File.output out "-("; 183 write_formula fm; 184 File.output out ")") 185 | write_formula (Or (fm1, fm2)) = 186 (File.output out "+("; 187 write_formula_or fm1; 188 File.output out " "; 189 write_formula_or fm2; 190 File.output out ")") 191 | write_formula (And (fm1, fm2)) = 192 (File.output out "*("; 193 write_formula_and fm1; 194 File.output out " "; 195 write_formula_and fm2; 196 File.output out ")") 197 (* optimization to make use of n-ary disjunction/conjunction *) 198 and write_formula_or (Or (fm1, fm2)) = 199 (write_formula_or fm1; 200 File.output out " "; 201 write_formula_or fm2) 202 | write_formula_or fm = 203 write_formula fm 204 and write_formula_and (And (fm1, fm2)) = 205 (write_formula_and fm1; 206 File.output out " "; 207 write_formula_and fm2) 208 | write_formula_and fm = 209 write_formula fm 210 val number_of_vars = Int.max (maxidx fm, 1) 211 in 212 File.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n"; 213 File.output out ("p sat " ^ string_of_int number_of_vars ^ "\n"); 214 File.output out "("; 215 write_formula fm; 216 File.output out ")\n" 217 end 218 in 219 File.open_output write_sat_file path 220 end; 221 222(* ------------------------------------------------------------------------- *) 223(* read_std_result_file: scans a SAT solver's output file for a satisfying *) 224(* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) 225(* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *) 226(* neither 'satisfiable' nor 'unsatisfiable'. Empty lines are ignored. *) 227(* The assignment must be given in one or more lines immediately after *) 228(* the line that contains 'satisfiable'. These lines must begin with *) 229(* 'assignment_prefix'. Variables must be separated by " ". Non- *) 230(* integer strings are ignored. If variable i is contained in the *) 231(* assignment, then i is interpreted as 'true'. If ~i is contained in *) 232(* the assignment, then i is interpreted as 'false'. Otherwise the *) 233(* value of i is taken to be unspecified. *) 234(* ------------------------------------------------------------------------- *) 235 236 fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = 237 let 238 fun int_list_from_string s = 239 map_filter Int.fromString (space_explode " " s) 240 fun assignment_from_list [] i = 241 NONE (* the SAT solver didn't provide a value for this variable *) 242 | assignment_from_list (x::xs) i = 243 if x=i then (SOME true) 244 else if x=(~i) then (SOME false) 245 else assignment_from_list xs i 246 fun parse_assignment xs [] = 247 assignment_from_list xs 248 | parse_assignment xs (line::lines) = 249 if String.isPrefix assignment_prefix line then 250 parse_assignment (xs @ int_list_from_string line) lines 251 else 252 assignment_from_list xs 253 fun is_substring needle haystack = 254 let 255 val length1 = String.size needle 256 val length2 = String.size haystack 257 in 258 if length2 < length1 then 259 false 260 else if needle = String.substring (haystack, 0, length1) then 261 true 262 else is_substring needle (String.substring (haystack, 1, length2-1)) 263 end 264 fun parse_lines [] = 265 UNKNOWN 266 | parse_lines (line::lines) = 267 if is_substring unsatisfiable line then 268 UNSATISFIABLE NONE 269 else if is_substring satisfiable line then 270 SATISFIABLE (parse_assignment [] lines) 271 else 272 parse_lines lines 273 in 274 (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path 275 end; 276 277(* ------------------------------------------------------------------------- *) 278(* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) 279(* ------------------------------------------------------------------------- *) 280 281 fun make_external_solver cmd writefn readfn fm = 282 (writefn fm; Isabelle_System.bash cmd; readfn ()); 283 284(* ------------------------------------------------------------------------- *) 285(* read_dimacs_cnf_file: returns a propositional formula that corresponds to *) 286(* a SAT problem given in DIMACS CNF format *) 287(* ------------------------------------------------------------------------- *) 288 289 fun read_dimacs_cnf_file path = 290 let 291 fun filter_preamble [] = 292 error "problem line not found in DIMACS CNF file" 293 | filter_preamble (line::lines) = 294 if String.isPrefix "c " line orelse line = "c" then 295 (* ignore comments *) 296 filter_preamble lines 297 else if String.isPrefix "p " line then 298 (* ignore the problem line (which must be the last line of the preamble) *) 299 (* Ignoring the problem line implies that if the file contains more clauses *) 300 (* or variables than specified in its preamble, we will accept it anyway. *) 301 lines 302 else 303 error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" 304 fun int_from_string s = 305 case Int.fromString s of 306 SOME i => i 307 | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number") 308 fun clauses xs = 309 let 310 val (xs1, xs2) = chop_prefix (fn i => i <> 0) xs 311 in 312 case xs2 of 313 [] => [xs1] 314 | (0::[]) => [xs1] 315 | (0::tl) => xs1 :: clauses tl 316 | _ => raise Fail "SAT_Solver.clauses" 317 end 318 fun literal_from_int i = 319 (i<>0 orelse error "variable index in DIMACS CNF file is 0"; 320 if i>0 then 321 Prop_Logic.BoolVar i 322 else 323 Prop_Logic.Not (Prop_Logic.BoolVar (~i))) 324 fun disjunction [] = 325 error "empty clause in DIMACS CNF file" 326 | disjunction (x::xs) = 327 (case xs of 328 [] => x 329 | _ => Prop_Logic.Or (x, disjunction xs)) 330 fun conjunction [] = 331 error "no clause in DIMACS CNF file" 332 | conjunction (x::xs) = 333 (case xs of 334 [] => x 335 | _ => Prop_Logic.And (x, conjunction xs)) 336 in 337 (conjunction 338 o (map disjunction) 339 o (map (map literal_from_int)) 340 o clauses 341 o (map int_from_string) 342 o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"]))) 343 o filter_preamble 344 o filter (fn l => l <> "") 345 o split_lines 346 o File.read) 347 path 348 end; 349 350(* ------------------------------------------------------------------------- *) 351(* solvers: a table of all registered SAT solvers *) 352(* ------------------------------------------------------------------------- *) 353 354 val solvers = Synchronized.var "solvers" ([] : (string * solver) list); 355 356 fun get_solvers () = Synchronized.value solvers; 357 358(* ------------------------------------------------------------------------- *) 359(* add_solver: updates 'solvers' by adding a new solver *) 360(* ------------------------------------------------------------------------- *) 361 362 fun add_solver (name, new_solver) = 363 Synchronized.change solvers (fn the_solvers => 364 let 365 val _ = if AList.defined (op =) the_solvers name 366 then warning ("SAT solver " ^ quote name ^ " was defined before") 367 else (); 368 in AList.update (op =) (name, new_solver) the_solvers end); 369 370(* ------------------------------------------------------------------------- *) 371(* invoke_solver: returns the solver associated with the given 'name' *) 372(* Note: If no solver is associated with 'name', exception 'Option' will be *) 373(* raised. *) 374(* ------------------------------------------------------------------------- *) 375 376 fun invoke_solver name = 377 the (AList.lookup (op =) (get_solvers ()) name); 378 379end; (* SAT_Solver *) 380 381 382(* ------------------------------------------------------------------------- *) 383(* Predefined SAT solvers *) 384(* ------------------------------------------------------------------------- *) 385 386(* ------------------------------------------------------------------------- *) 387(* Internal SAT solver, available as 'SAT_Solver.invoke_solver "cdclite"' -- *) 388(* a simplified implementation of the conflict-driven clause-learning *) 389(* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean *) 390(* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models *) 391(* and proof traces. *) 392(* ------------------------------------------------------------------------- *) 393 394let 395 type clause = int list * int 396 type value = bool option 397 datatype reason = Decided | Implied of clause | Level0 of int 398 type variable = bool option * reason * int * int 399 type proofs = int * int list Inttab.table 400 type state = 401 int * int list * variable Inttab.table * clause list Inttab.table * proofs 402 exception CONFLICT of clause * state 403 exception UNSAT of clause * state 404 405 fun neg i = ~i 406 407 fun lit_value lit value = if lit > 0 then value else Option.map not value 408 409 fun var_of vars lit: variable = the (Inttab.lookup vars (abs lit)) 410 fun value_of vars lit = lit_value lit (#1 (var_of vars lit)) 411 fun reason_of vars lit = #2 (var_of vars lit) 412 fun level_of vars lit = #3 (var_of vars lit) 413 414 fun is_true vars lit = (value_of vars lit = SOME true) 415 fun is_false vars lit = (value_of vars lit = SOME false) 416 fun is_unassigned vars lit = (value_of vars lit = NONE) 417 fun assignment_of vars lit = the_default NONE (try (value_of vars) lit) 418 419 fun put_var value reason level (_, _, _, rank) = (value, reason, level, rank) 420 fun incr_rank (value, reason, level, rank) = (value, reason, level, rank + 1) 421 fun update_var lit f = Inttab.map_entry (abs lit) f 422 fun add_var lit = Inttab.update (abs lit, (NONE, Decided, ~1, 0)) 423 424 fun assign lit r l = update_var lit (put_var (SOME (lit > 0)) r l) 425 fun unassign lit = update_var lit (put_var NONE Decided ~1) 426 427 fun add_proof [] (idx, ptab) = (idx, (idx + 1, ptab)) 428 | add_proof ps (idx, ptab) = (idx, (idx + 1, Inttab.update (idx, ps) ptab)) 429 430 fun level0_proof_of (Level0 idx) = SOME idx 431 | level0_proof_of _ = NONE 432 433 fun level0_proofs_of vars = map_filter (level0_proof_of o reason_of vars) 434 fun prems_of vars (lits, p) = p :: level0_proofs_of vars lits 435 fun mk_proof vars cls proofs = add_proof (prems_of vars cls) proofs 436 437 fun push lit cls (level, trail, vars, clss, proofs) = 438 let 439 val (reason, proofs) = 440 if level = 0 then apfst Level0 (mk_proof vars cls proofs) 441 else (Implied cls, proofs) 442 in (level, lit :: trail, assign lit reason level vars, clss, proofs) end 443 444 fun push_decided lit (level, trail, vars, clss, proofs) = 445 let val vars' = assign lit Decided (level + 1) vars 446 in (level + 1, lit :: 0 :: trail, vars', clss, proofs) end 447 448 fun prop (cls as (lits, _)) (cx as (units, state as (level, _, vars, _, _))) = 449 if exists (is_true vars) lits then cx 450 else if forall (is_false vars) lits then 451 if level = 0 then raise UNSAT (cls, state) 452 else raise CONFLICT (cls, state) 453 else 454 (case filter (is_unassigned vars) lits of 455 [lit] => (lit :: units, push lit cls state) 456 | _ => cx) 457 458 fun propagate units (state as (_, _, _, clss, _)) = 459 (case fold (fold prop o Inttab.lookup_list clss) units ([], state) of 460 ([], state') => (NONE, state') 461 | (units', state') => propagate units' state') 462 handle CONFLICT (cls, state') => (SOME cls, state') 463 464 fun max_unassigned (v, (NONE, _, _, rank)) (x as (_, r)) = 465 if rank > r then (SOME v, rank) else x 466 | max_unassigned _ x = x 467 468 fun decide (state as (_, _, vars, _, _)) = 469 (case Inttab.fold max_unassigned vars (NONE, 0) of 470 (SOME lit, _) => SOME (lit, push_decided lit state) 471 | (NONE, _) => NONE) 472 473 fun mark lit = Inttab.update (abs lit, true) 474 fun marked ms lit = the_default false (Inttab.lookup ms (abs lit)) 475 fun ignore l ms lit = ((lit = l) orelse marked ms lit) 476 477 fun first_lit _ [] = raise Empty 478 | first_lit _ (0 :: _) = raise Empty 479 | first_lit pred (lit :: lits) = 480 if pred lit then (lit, lits) else first_lit pred lits 481 482 fun reason_cls_of vars lit = 483 (case reason_of vars lit of 484 Implied cls => cls 485 | _ => raise Option) 486 487 fun analyze conflicting_cls (level, trail, vars, _, _) = 488 let 489 fun back i lit (lits, p) trail ms ls ps = 490 let 491 val (lits0, lits') = List.partition (equal 0 o level_of vars) lits 492 val lits1 = filter_out (ignore lit ms) lits' 493 val lits2 = filter_out (equal level o level_of vars) lits1 494 val i' = length lits1 - length lits2 + i 495 val ms' = fold mark lits1 ms 496 val ls' = lits2 @ ls 497 val ps' = level0_proofs_of vars lits0 @ (p :: ps) 498 val (lit', trail') = first_lit (marked ms') trail 499 in 500 if i' = 1 then (neg lit', ls', rev ps') 501 else back (i' - 1) lit' (reason_cls_of vars lit') trail' ms' ls' ps' 502 end 503 in back 0 0 conflicting_cls trail Inttab.empty [] [] end 504 505 fun keep_clause (cls as (lits, _)) (level, trail, vars, clss, proofs) = 506 let 507 val vars' = fold (fn lit => update_var lit incr_rank) lits vars 508 val clss' = fold (fn lit => Inttab.cons_list (neg lit, cls)) lits clss 509 in (level, trail, vars', clss', proofs) end 510 511 fun learn (cls as (lits, _)) = (length lits <= 2) ? keep_clause cls 512 513 fun backjump _ (state as (_, [], _, _, _)) = state 514 | backjump i (level, 0 :: trail, vars, clss, proofs) = 515 (level - 1, trail, vars, clss, proofs) |> (i > 1) ? backjump (i - 1) 516 | backjump i (level, lit :: trail, vars, clss, proofs) = 517 backjump i (level, trail, unassign lit vars, clss, proofs) 518 519 fun search units state = 520 (case propagate units state of 521 (NONE, state' as (_, _, vars, _, _)) => 522 (case decide state' of 523 NONE => SAT_Solver.SATISFIABLE (assignment_of vars) 524 | SOME (lit, state'') => search [lit] state'') 525 | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) => 526 let 527 val (lit, lits, ps) = analyze conflicting_cls state' 528 val (idx, proofs') = add_proof ps proofs 529 val cls = (lit :: lits, idx) 530 in 531 (level, trail, vars, clss, proofs') 532 |> backjump (level - fold (Integer.max o level_of vars) lits 0) 533 |> learn cls 534 |> push lit cls 535 |> search [lit] 536 end) 537 538 fun has_opposing_lits [] = false 539 | has_opposing_lits (lit :: lits) = 540 member (op =) lits (neg lit) orelse has_opposing_lits lits 541 542 fun add_clause (cls as ([_], _)) (units, state) = 543 let val (units', state') = prop cls (units, state) 544 in (units', state') end 545 | add_clause (cls as (lits, _)) (cx as (units, state)) = 546 if has_opposing_lits lits then cx 547 else (units, keep_clause cls state) 548 549 fun mk_clause lits proofs = 550 apfst (pair (distinct (op =) lits)) (add_proof [] proofs) 551 552 fun solve litss = 553 let 554 val (clss, proofs) = fold_map mk_clause litss (0, Inttab.empty) 555 val vars = fold (fold add_var) litss Inttab.empty 556 val state = (0, [], vars, Inttab.empty, proofs) 557 in uncurry search (fold add_clause clss ([], state)) end 558 handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) => 559 let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs 560 in SAT_Solver.UNSATISFIABLE (SOME (ptab, idx)) end 561 562 fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable" 563 | variable_of (Prop_Logic.BoolVar i) = i 564 | variable_of _ = error "expected formula in CNF" 565 fun literal_of (Prop_Logic.Not fm) = neg (variable_of fm) 566 | literal_of fm = variable_of fm 567 fun clause_of (Prop_Logic.Or (fm1, fm2)) = clause_of fm1 @ clause_of fm2 568 | clause_of fm = [literal_of fm] 569 fun clauses_of (Prop_Logic.And (fm1, fm2)) = clauses_of fm1 @ clauses_of fm2 570 | clauses_of Prop_Logic.True = [[1, ~1]] 571 | clauses_of Prop_Logic.False = [[1], [~1]] 572 | clauses_of fm = [clause_of fm] 573 574 fun dpll_solver fm = 575 let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm 576 in solve (clauses_of fm') end 577in 578 SAT_Solver.add_solver ("cdclite", dpll_solver) 579end; 580 581(* ------------------------------------------------------------------------- *) 582(* Internal SAT solver, available as 'SAT_Solver.invoke_solver "auto"': uses *) 583(* the last installed solver (other than "auto" itself) that does not raise *) 584(* 'NOT_CONFIGURED'. (However, the solver may return 'UNKNOWN'.) *) 585(* ------------------------------------------------------------------------- *) 586 587let 588 fun auto_solver fm = 589 let 590 fun loop [] = 591 SAT_Solver.UNKNOWN 592 | loop ((name, solver)::solvers) = 593 if name="auto" then 594 (* do not call solver "auto" from within "auto" *) 595 loop solvers 596 else ( 597 (* apply 'solver' to 'fm' *) 598 solver fm 599 handle SAT_Solver.NOT_CONFIGURED => loop solvers 600 ) 601 in 602 loop (SAT_Solver.get_solvers ()) 603 end 604in 605 SAT_Solver.add_solver ("auto", auto_solver) 606end; 607 608(* ------------------------------------------------------------------------- *) 609(* MiniSat 1.14 *) 610(* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *) 611(* ------------------------------------------------------------------------- *) 612 613(* ------------------------------------------------------------------------- *) 614(* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *) 615(* Matthews, which can output ASCII proof traces. Replaying binary proof *) 616(* traces generated by MiniSat-p_v1.14 has _not_ been implemented. *) 617(* ------------------------------------------------------------------------- *) 618 619(* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *) 620(* that the latter is preferred by the "auto" solver *) 621 622(* There is a complication that is dealt with in the code below: MiniSat *) 623(* introduces IDs for original clauses in the proof trace. It does not (in *) 624(* general) follow the convention that the original clauses are numbered *) 625(* from 0 to n-1 (where n is the number of clauses in the formula). *) 626 627let 628 exception INVALID_PROOF of string 629 fun minisat_with_proofs fm = 630 let 631 val _ = if (getenv "MINISAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () 632 val serial_str = serial_string () 633 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) 634 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) 635 val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf")) 636 val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " -t " ^ File.bash_path proofpath ^ "> /dev/null" 637 fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm 638 fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT") 639 val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () 640 val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () 641 val cnf = Prop_Logic.defcnf fm 642 val result = SAT_Solver.make_external_solver cmd writefn readfn cnf 643 val _ = try File.rm inpath 644 val _ = try File.rm outpath 645 in case result of 646 SAT_Solver.UNSATISFIABLE NONE => 647 (let 648 val proof_lines = (split_lines o File.read) proofpath 649 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" 650 (* representation of clauses as ordered lists of literals (with duplicates removed) *) 651 fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) = 652 Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) 653 | clause_to_lit_list (Prop_Logic.BoolVar i) = 654 [i] 655 | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) = 656 [~i] 657 | clause_to_lit_list _ = 658 raise INVALID_PROOF "Error: invalid clause in CNF formula." 659 fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = 660 cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 661 | cnf_number_of_clauses _ = 662 1 663 val number_of_clauses = cnf_number_of_clauses cnf 664 (* int list array *) 665 val clauses = Array.array (number_of_clauses, []) 666 (* initialize the 'clauses' array *) 667 fun init_array (Prop_Logic.And (fm1, fm2), n) = 668 init_array (fm2, init_array (fm1, n)) 669 | init_array (fm, n) = 670 (Array.update (clauses, n, clause_to_lit_list fm); n+1) 671 val _ = init_array (cnf, 0) 672 (* optimization for the common case where MiniSat "R"s clauses in their *) 673 (* original order: *) 674 val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1) 675 (* search the 'clauses' array for the given list of literals 'lits', *) 676 (* starting at index '!last_ref_clause + 1' *) 677 fun original_clause_id lits = 678 let 679 fun original_clause_id_from index = 680 if index = number_of_clauses then 681 (* search from beginning again *) 682 original_clause_id_from 0 683 (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) 684 (* testing for equality should suffice -- barring duplicate literals *) 685 else if Array.sub (clauses, index) = lits then ( 686 (* success *) 687 last_ref_clause := index; 688 SOME index 689 ) else if index = !last_ref_clause then 690 (* failure *) 691 NONE 692 else 693 (* continue search *) 694 original_clause_id_from (index + 1) 695 in 696 original_clause_id_from (!last_ref_clause + 1) 697 end 698 fun int_from_string s = 699 (case Int.fromString s of 700 SOME i => i 701 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")) 702 (* parse the proof file *) 703 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) 704 val empty_id = Unsynchronized.ref ~1 705 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) 706 (* our proof format, where original clauses are numbered starting from 0 *) 707 val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table) 708 fun sat_to_proof id = ( 709 case Inttab.lookup (!clause_id_map) id of 710 SOME id' => id' 711 | NONE => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.") 712 ) 713 val next_id = Unsynchronized.ref (number_of_clauses - 1) 714 fun process_tokens [] = 715 () 716 | process_tokens (tok::toks) = 717 if tok="R" then ( 718 case toks of 719 id::sep::lits => 720 let 721 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." 722 val cid = int_from_string id 723 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") 724 val ls = sort int_ord (map int_from_string lits) 725 val proof_id = case original_clause_id ls of 726 SOME orig_id => orig_id 727 | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") 728 in 729 (* extend the mapping of clause IDs with this newly defined ID *) 730 clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) 731 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") 732 (* the proof itself doesn't change *) 733 end 734 | _ => 735 raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." 736 ) else if tok="C" then ( 737 case toks of 738 id::sep::ids => 739 let 740 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." 741 val cid = int_from_string id 742 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") 743 (* ignore the pivot literals in MiniSat's trace *) 744 fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." 745 | unevens (x :: []) = x :: [] 746 | unevens (x :: _ :: xs) = x :: unevens xs 747 val rs = (map sat_to_proof o unevens o map int_from_string) ids 748 (* extend the mapping of clause IDs with this newly defined ID *) 749 val proof_id = Unsynchronized.inc next_id 750 val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) 751 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") 752 in 753 (* update clause table *) 754 clause_table := Inttab.update_new (proof_id, rs) (!clause_table) 755 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") 756 end 757 | _ => 758 raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." 759 ) else if tok="D" then ( 760 case toks of 761 [id] => 762 let 763 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." 764 val _ = sat_to_proof (int_from_string id) 765 in 766 (* simply ignore "D" *) 767 () 768 end 769 | _ => 770 raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." 771 ) else if tok="X" then ( 772 case toks of 773 [id1, id2] => 774 let 775 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." 776 val _ = sat_to_proof (int_from_string id1) 777 val new_empty_id = sat_to_proof (int_from_string id2) 778 in 779 (* update conflict id *) 780 empty_id := new_empty_id 781 end 782 | _ => 783 raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." 784 ) else 785 raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") 786 fun process_lines [] = 787 () 788 | process_lines (l::ls) = ( 789 process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); 790 process_lines ls 791 ) 792 (* proof *) 793 val _ = process_lines proof_lines 794 val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." 795 in 796 SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) 797 end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE)) 798 | result => 799 result 800 end 801in 802 SAT_Solver.add_solver ("minisat_with_proofs", minisat_with_proofs) 803end; 804 805let 806 fun minisat fm = 807 let 808 val _ = if getenv "MINISAT_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else () 809 val serial_str = serial_string () 810 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) 811 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) 812 val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " > /dev/null" 813 fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) 814 fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT") 815 val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () 816 val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () 817 val result = SAT_Solver.make_external_solver cmd writefn readfn fm 818 val _ = try File.rm inpath 819 val _ = try File.rm outpath 820 in 821 result 822 end 823in 824 SAT_Solver.add_solver ("minisat", minisat) 825end; 826 827(* ------------------------------------------------------------------------- *) 828(* zChaff (https://www.princeton.edu/~chaff/zchaff.html) *) 829(* ------------------------------------------------------------------------- *) 830 831(* ------------------------------------------------------------------------- *) 832(* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if *) 833(* zChaff finds that the formula is unsatisfiable, a proof of this is read *) 834(* from a file "resolve_trace" that was generated by zChaff. See the code *) 835(* below for the expected format of the "resolve_trace" file. Aside from *) 836(* some basic syntactic checks, no verification of the proof is performed. *) 837(* ------------------------------------------------------------------------- *) 838 839(* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so *) 840(* that the latter is preferred by the "auto" solver *) 841 842let 843 exception INVALID_PROOF of string 844 fun zchaff_with_proofs fm = 845 case SAT_Solver.invoke_solver "zchaff" fm of 846 SAT_Solver.UNSATISFIABLE NONE => 847 (let 848 (* FIXME File.tmp_path (!?) *) 849 val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) 850 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" 851 fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = 852 cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 853 | cnf_number_of_clauses _ = 1 854 fun int_from_string s = ( 855 case Int.fromString s of 856 SOME i => i 857 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") 858 ) 859 (* parse the "resolve_trace" file *) 860 val clause_offset = Unsynchronized.ref ~1 861 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) 862 val empty_id = Unsynchronized.ref ~1 863 fun process_tokens [] = 864 () 865 | process_tokens (tok::toks) = 866 if tok="CL:" then ( 867 case toks of 868 id::sep::ids => 869 let 870 val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") 871 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") 872 val cid = int_from_string id 873 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") 874 val rs = map int_from_string ids 875 in 876 (* update clause table *) 877 clause_table := Inttab.update_new (cid, rs) (!clause_table) 878 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") 879 end 880 | _ => 881 raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." 882 ) else if tok="VAR:" then ( 883 case toks of 884 id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => 885 let 886 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") 887 (* set 'clause_offset' to the largest used clause ID *) 888 val _ = if !clause_offset = ~1 then clause_offset := 889 (case Inttab.max (!clause_table) of 890 SOME (id, _) => id 891 | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) 892 else 893 () 894 val vid = int_from_string id 895 val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") 896 val _ = int_from_string levid 897 val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") 898 val _ = int_from_string valid 899 val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") 900 val aid = int_from_string anteid 901 val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") 902 val ls = map int_from_string lits 903 (* convert the data provided by zChaff to our resolution-style proof format *) 904 (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) 905 (* given by the literals in the antecedent clause *) 906 (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) 907 val cid = !clause_offset + vid 908 (* the low bit of each literal gives its sign (positive/negative), therefore *) 909 (* we have to divide each literal by 2 to obtain the proper variable ID; then *) 910 (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) 911 val vids = filter (not_equal vid) (map (fn l => l div 2) ls) 912 val rs = aid :: map (fn v => !clause_offset + v) vids 913 in 914 (* update clause table *) 915 clause_table := Inttab.update_new (cid, rs) (!clause_table) 916 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") 917 end 918 | _ => 919 raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." 920 ) else if tok="CONF:" then ( 921 case toks of 922 id::sep::ids => 923 let 924 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." 925 val cid = int_from_string id 926 val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") 927 val ls = map int_from_string ids 928 (* the conflict clause must be resolved with the unit clauses *) 929 (* for its literals to obtain the empty clause *) 930 val vids = map (fn l => l div 2) ls 931 val rs = cid :: map (fn v => !clause_offset + v) vids 932 val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1 933 in 934 (* update clause table and conflict id *) 935 clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) 936 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); 937 empty_id := new_empty_id 938 end 939 | _ => 940 raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." 941 ) else 942 raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") 943 fun process_lines [] = 944 () 945 | process_lines (l::ls) = ( 946 process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); 947 process_lines ls 948 ) 949 (* proof *) 950 val _ = process_lines proof_lines 951 val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." 952 in 953 SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) 954 end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE)) 955 | result => 956 result 957in 958 SAT_Solver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) 959end; 960 961let 962 fun zchaff fm = 963 let 964 val _ = if getenv "ZCHAFF_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else () 965 val serial_str = serial_string () 966 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) 967 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) 968 val cmd = "\"$ZCHAFF_HOME/zchaff\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath 969 fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) 970 fun readfn () = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") 971 val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () 972 val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () 973 val result = SAT_Solver.make_external_solver cmd writefn readfn fm 974 val _ = try File.rm inpath 975 val _ = try File.rm outpath 976 in 977 result 978 end 979in 980 SAT_Solver.add_solver ("zchaff", zchaff) 981end; 982 983(* ------------------------------------------------------------------------- *) 984(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *) 985(* ------------------------------------------------------------------------- *) 986 987let 988 fun berkmin fm = 989 let 990 val _ = if (getenv "BERKMIN_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () 991 val serial_str = serial_string () 992 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) 993 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) 994 val cmd = "\"$BERKMIN_HOME/${BERKMIN_EXE:-BerkMin561}\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath 995 fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) 996 fun readfn () = SAT_Solver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") 997 val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () 998 val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () 999 val result = SAT_Solver.make_external_solver cmd writefn readfn fm 1000 val _ = try File.rm inpath 1001 val _ = try File.rm outpath 1002 in 1003 result 1004 end 1005in 1006 SAT_Solver.add_solver ("berkmin", berkmin) 1007end; 1008 1009(* ------------------------------------------------------------------------- *) 1010(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *) 1011(* ------------------------------------------------------------------------- *) 1012 1013let 1014 fun jerusat fm = 1015 let 1016 val _ = if (getenv "JERUSAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () 1017 val serial_str = serial_string () 1018 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) 1019 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) 1020 val cmd = "\"$JERUSAT_HOME/Jerusat1.3\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath 1021 fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) 1022 fun readfn () = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") 1023 val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () 1024 val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () 1025 val result = SAT_Solver.make_external_solver cmd writefn readfn fm 1026 val _ = try File.rm inpath 1027 val _ = try File.rm outpath 1028 in 1029 result 1030 end 1031in 1032 SAT_Solver.add_solver ("jerusat", jerusat) 1033end; 1034