src/HOL/Tools/sat_solver.ML
author boehmes
Thu May 01 22:56:59 2014 +0200 (2014-05-01)
changeset 56815 848d507584db
parent 56147 9589605bcf41
child 56845 691da43fbdd4
permissions -rw-r--r--
added internal proof-producing SAT solver
     1 (*  Title:      HOL/Tools/sat_solver.ML
     2     Author:     Tjark Weber
     3     Copyright   2004-2009
     4 
     5 Interface to external SAT solvers, and (simple) built-in SAT solvers.
     6 
     7 Relevant 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 
    24 signature SAT_SOLVER =
    25 sig
    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 *)
    48 end;
    49 
    50 structure SatSolver : SAT_SOLVER =
    51 struct
    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            TextIO.output (out, string_of_int i))
   133         | write_formula (Not (BoolVar i)) =
   134           (TextIO.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            TextIO.output (out, " ");
   141            write_formula fm2)
   142         | write_formula (And (fm1, fm2)) =
   143           (write_formula fm1;
   144            TextIO.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       TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_cnf_file\n");
   151       TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^
   152                             string_of_int number_of_clauses ^ "\n");
   153       write_formula fm';
   154       TextIO.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           TextIO.output (out, "*()")
   173         | write_formula False =
   174           TextIO.output (out, "+()")
   175         | write_formula (BoolVar i) =
   176           (i>=1 orelse error "formula contains a variable index less than 1";
   177            TextIO.output (out, string_of_int i))
   178         | write_formula (Not (BoolVar i)) =
   179           (TextIO.output (out, "-");
   180            write_formula (BoolVar i))
   181         | write_formula (Not fm) =
   182           (TextIO.output (out, "-(");
   183            write_formula fm;
   184            TextIO.output (out, ")"))
   185         | write_formula (Or (fm1, fm2)) =
   186           (TextIO.output (out, "+(");
   187            write_formula_or fm1;
   188            TextIO.output (out, " ");
   189            write_formula_or fm2;
   190            TextIO.output (out, ")"))
   191         | write_formula (And (fm1, fm2)) =
   192           (TextIO.output (out, "*(");
   193            write_formula_and fm1;
   194            TextIO.output (out, " ");
   195            write_formula_and fm2;
   196            TextIO.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            TextIO.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            TextIO.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       TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_sat_file\n");
   213       TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n");
   214       TextIO.output (out, "(");
   215       write_formula fm;
   216       TextIO.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) = take_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 "SatSolver.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 
   379 end;  (* SatSolver *)
   380 
   381 
   382 (* ------------------------------------------------------------------------- *)
   383 (* Predefined SAT solvers                                                    *)
   384 (* ------------------------------------------------------------------------- *)
   385 
   386 (* ------------------------------------------------------------------------- *)
   387 (* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"'   *)
   388 (* -- simply enumerates assignments until a satisfying assignment is found   *)
   389 (* ------------------------------------------------------------------------- *)
   390 
   391 let
   392   fun enum_solver fm =
   393   let
   394     val indices = Prop_Logic.indices fm
   395     (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
   396     fun next_list _ ([]:int list) =
   397       NONE
   398       | next_list [] (y::ys) =
   399       SOME [y]
   400       | next_list (x::xs) (y::ys) =
   401       if x=y then
   402         (* reset the bit, continue *)
   403         next_list xs ys
   404       else
   405         (* set the lowest bit that wasn't set before, keep the higher bits *)
   406         SOME (y::x::xs)
   407     fun assignment_from_list xs i =
   408       member (op =) xs i
   409     fun solver_loop xs =
   410       if Prop_Logic.eval (assignment_from_list xs) fm then
   411         SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
   412       else
   413         (case next_list xs indices of
   414           SOME xs' => solver_loop xs'
   415         | NONE     => SatSolver.UNSATISFIABLE NONE)
   416   in
   417     (* start with the "first" assignment (all variables are interpreted as 'false') *)
   418     solver_loop []
   419   end
   420 in
   421   SatSolver.add_solver ("enumerate", enum_solver)
   422 end;
   423 
   424 (* ------------------------------------------------------------------------- *)
   425 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a   *)
   426 (* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
   427 (* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1).  *)
   428 (* ------------------------------------------------------------------------- *)
   429 
   430 let
   431   local
   432     open Prop_Logic
   433   in
   434     fun dpll_solver fm =
   435     let
   436       (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *)
   437       (* but that sometimes leads to worse performance due to the         *)
   438       (* introduction of additional variables.                            *)
   439       val fm' = Prop_Logic.nnf fm
   440       val indices = Prop_Logic.indices fm'
   441       fun partial_var_eval []      i = BoolVar i
   442         | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
   443       fun partial_eval xs True             = True
   444         | partial_eval xs False            = False
   445         | partial_eval xs (BoolVar i)      = partial_var_eval xs i
   446         | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
   447         | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
   448         | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
   449       fun forced_vars True              = []
   450         | forced_vars False             = []
   451         | forced_vars (BoolVar i)       = [i]
   452         | forced_vars (Not (BoolVar i)) = [~i]
   453         | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1) (forced_vars fm2)
   454         | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1) (forced_vars fm2)
   455         (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   456         (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   457         | forced_vars _                 = error "formula is not in negation normal form"
   458       fun eval_and_force xs fm =
   459       let
   460         val fm' = partial_eval xs fm
   461         val xs' = forced_vars fm'
   462       in
   463         if null xs' then
   464           (xs, fm')
   465         else
   466           eval_and_force (xs@xs') fm'  (* xs and xs' should be distinct, so '@' here should have *)
   467                                        (* the same effect as 'union_int'                         *)
   468       end
   469       fun fresh_var xs =
   470         find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
   471       (* partial assignment 'xs' *)
   472       fun dpll xs fm =
   473       let
   474         val (xs', fm') = eval_and_force xs fm
   475       in
   476         case fm' of
   477           True  => SOME xs'
   478         | False => NONE
   479         | _     =>
   480           let
   481             val x = the (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
   482           in
   483             case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
   484               SOME xs'' => SOME xs''
   485             | NONE      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
   486           end
   487       end
   488       fun assignment_from_list [] i =
   489         NONE  (* the DPLL procedure didn't provide a value for this variable *)
   490         | assignment_from_list (x::xs) i =
   491         if x=i then (SOME true)
   492         else if x=(~i) then (SOME false)
   493         else assignment_from_list xs i
   494     in
   495       (* initially, no variable is interpreted yet *)
   496       case dpll [] fm' of
   497         SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
   498       | NONE            => SatSolver.UNSATISFIABLE NONE
   499     end
   500   end  (* local *)
   501 in
   502   SatSolver.add_solver ("dpll", dpll_solver)
   503 end;
   504 
   505 (* ------------------------------------------------------------------------- *)
   506 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll_p"' --   *)
   507 (* a simple, slightly more efficient implementation of the DPLL algorithm    *)
   508 (* (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean Satisfiability  *)
   509 (* Solvers", July 2002, Fig. 2). In contrast to the other two ML solvers     *)
   510 (* above, this solver produces proof traces. *)
   511 (* ------------------------------------------------------------------------- *)
   512 
   513 let
   514   type clause = int list * int
   515   type value = bool option
   516   datatype reason = Decided | Implied of clause | Level0 of int
   517   type variable = bool option * reason * int * int
   518   type proofs = int * int list Inttab.table
   519   type state =
   520     int * int list * variable Inttab.table * clause list Inttab.table * proofs
   521   exception CONFLICT of clause * state
   522   exception UNSAT of clause * state
   523 
   524   fun neg i = ~i
   525 
   526   fun lit_value lit value = if lit > 0 then value else Option.map not value
   527 
   528   fun var_of vars lit: variable = the (Inttab.lookup vars (abs lit))
   529   fun value_of vars lit = lit_value lit (#1 (var_of vars lit))
   530   fun reason_of vars lit = #2 (var_of vars lit)
   531   fun level_of vars lit = #3 (var_of vars lit)
   532 
   533   fun is_true vars lit = (value_of vars lit = SOME true)
   534   fun is_false vars lit = (value_of vars lit = SOME false)
   535   fun is_unassigned vars lit = (value_of vars lit = NONE)
   536   fun assignment_of vars lit = the_default NONE (try (value_of vars) lit)
   537 
   538   fun put_var value reason level (_, _, _, rank) = (value, reason, level, rank)
   539   fun incr_rank (value, reason, level, rank) = (value, reason, level, rank + 1)
   540   fun update_var lit f = Inttab.map_entry (abs lit) f
   541   fun add_var lit = Inttab.update (abs lit, (NONE, Decided, ~1, 0))
   542 
   543   fun assign lit r l = update_var lit (put_var (SOME (lit > 0)) r l)
   544   fun unassign lit = update_var lit (put_var NONE Decided ~1)
   545 
   546   fun add_proof [] (idx, ptab) = (idx, (idx + 1, ptab))
   547     | add_proof ps (idx, ptab) = (idx, (idx + 1, Inttab.update (idx, ps) ptab))
   548 
   549   fun level0_proof_of (Level0 idx) = SOME idx
   550     | level0_proof_of _ = NONE
   551 
   552   fun level0_proofs_of vars = map_filter (level0_proof_of o reason_of vars)
   553   fun prems_of vars (lits, p) = p :: level0_proofs_of vars lits
   554   fun mk_proof vars cls proofs = add_proof (prems_of vars cls) proofs
   555 
   556   fun push lit cls (level, trail, vars, clss, proofs) =
   557     let
   558       val (reason, proofs) =
   559         if level = 0 then apfst Level0 (mk_proof vars cls proofs)
   560         else (Implied cls, proofs)
   561     in (level, lit :: trail, assign lit reason level vars, clss, proofs) end
   562 
   563   fun push_decided lit (level, trail, vars, clss, proofs) =
   564     let val vars' = assign lit Decided (level + 1) vars
   565     in (level + 1, lit :: 0 :: trail, vars', clss, proofs) end
   566 
   567   fun prop (cls as (lits, _)) (cx as (units, state as (level, _, vars, _, _))) =
   568     if exists (is_true vars) lits then cx
   569     else if forall (is_false vars) lits then
   570       if level = 0 then raise UNSAT (cls, state)
   571       else raise CONFLICT (cls, state)
   572     else
   573       (case filter (is_unassigned vars) lits of
   574         [lit] => (lit :: units, push lit cls state)
   575       | _ => cx)
   576 
   577   fun propagate units (state as (_, _, _, clss, _)) =
   578     (case fold (fold prop o Inttab.lookup_list clss) units ([], state) of
   579       ([], state') => (NONE, state')
   580     | (units', state') => propagate units' state')
   581     handle CONFLICT (cls, state') => (SOME cls, state')
   582 
   583   fun max_unassigned (v, (NONE, _, _, rank)) (x as (_, r)) =
   584         if rank > r then (SOME v, rank) else x
   585     | max_unassigned _  x = x
   586 
   587   fun decide (state as (_, _, vars, _, _)) =
   588     (case Inttab.fold max_unassigned vars (NONE, 0) of
   589       (SOME lit, _) => SOME (lit, push_decided lit state)
   590     | (NONE, _) => NONE)
   591 
   592   fun mark lit = Inttab.update (abs lit, true)
   593   fun marked ms lit = the_default false (Inttab.lookup ms (abs lit))
   594   fun ignore l ms lit = ((lit = l) orelse marked ms lit)
   595 
   596   fun first_lit _ [] = raise Empty
   597     | first_lit _ (0 :: _) = raise Empty
   598     | first_lit pred (lit :: lits) =
   599         if pred lit then (lit, lits) else first_lit pred lits
   600 
   601   fun reason_cls_of vars lit =
   602     (case reason_of vars lit of
   603       Implied cls => cls
   604     | _ => raise Option)
   605 
   606   fun analyze conflicting_cls (level, trail, vars, _, _) =
   607     let
   608       fun back i lit (lits, p) trail ms ls ps =
   609         let
   610           val (lits0, lits') = List.partition (equal 0 o level_of vars) lits
   611           val lits1 = filter_out (ignore lit ms) lits'
   612           val lits2 = filter_out (equal level o level_of vars) lits1
   613           val i' = length lits1 - length lits2 + i
   614           val ms' = fold mark lits1 ms
   615           val ls' = lits2 @ ls
   616           val ps' = level0_proofs_of vars lits0 @ (p :: ps)
   617           val (lit', trail') = first_lit (marked ms') trail
   618         in 
   619           if i' = 1 then (neg lit', ls', rev ps')
   620           else back (i' - 1) lit' (reason_cls_of vars lit') trail' ms' ls' ps'
   621         end
   622     in back 0 0 conflicting_cls trail Inttab.empty [] [] end
   623 
   624   fun keep_clause (cls as (lits, _)) (level, trail, vars, clss, proofs) =
   625     let
   626       val vars' = fold (fn lit => update_var lit incr_rank) lits vars
   627       val clss' = fold (fn lit => Inttab.cons_list (neg lit, cls)) lits clss
   628     in (level, trail, vars', clss', proofs) end
   629 
   630   fun learn (cls as (lits, _)) = (length lits <= 2) ? keep_clause cls
   631 
   632   fun backjump _ (state as (_, [], _, _, _)) = state 
   633     | backjump i (level, 0 :: trail, vars, clss, proofs) =
   634         (level - 1, trail, vars, clss, proofs) |> (i > 1) ? backjump (i - 1)
   635     | backjump i (level, lit :: trail, vars, clss, proofs) =
   636         backjump i (level, trail, unassign lit vars, clss, proofs)
   637 
   638   fun search units state =
   639     (case propagate units state of
   640       (NONE, state' as (_, _, vars, _, _)) =>
   641         (case decide state' of
   642           NONE => SatSolver.SATISFIABLE (assignment_of vars)
   643         | SOME (lit, state'') => search [lit] state'')
   644     | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) =>
   645         let 
   646           val (lit, lits, ps) = analyze conflicting_cls state'
   647           val (idx, proofs') = add_proof ps proofs
   648           val cls = (lit :: lits, idx)
   649         in
   650           (level, trail, vars, clss, proofs')
   651           |> backjump (level - fold (Integer.max o level_of vars) lits 0)
   652           |> learn cls
   653           |> push lit cls
   654           |> search [lit]
   655         end)
   656 
   657   fun has_opposing_lits [] = false
   658     | has_opposing_lits (lit :: lits) =
   659         member (op =) lits (neg lit) orelse has_opposing_lits lits
   660 
   661   fun add_clause (cls as ([_], _)) (units, state) =
   662         let val (units', state') = prop cls (units, state)
   663         in (units', state') end
   664     | add_clause (cls as (lits, _)) (cx as (units, state)) =
   665         if has_opposing_lits lits then cx
   666         else (units, keep_clause cls state)
   667 
   668   fun mk_clause lits proofs =
   669     apfst (pair (distinct (op =) lits)) (add_proof [] proofs)
   670 
   671   fun solve litss =
   672     let
   673       val (clss, proofs) = fold_map mk_clause litss (0, Inttab.empty)
   674       val vars = fold (fold add_var) litss Inttab.empty
   675       val state = (0, [], vars, Inttab.empty, proofs)
   676     in uncurry search (fold add_clause clss ([], state)) end
   677     handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) =>
   678       let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs
   679       in SatSolver.UNSATISFIABLE (SOME (ptab, idx)) end
   680 
   681   fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable"
   682     | variable_of (Prop_Logic.BoolVar i) = i
   683     | variable_of _ = error "expected formula in CNF"
   684   fun literal_of (Prop_Logic.Not fm) = neg (variable_of fm)
   685     | literal_of fm = variable_of fm
   686   fun clause_of (Prop_Logic.Or (fm1, fm2)) = clause_of fm1 @ clause_of fm2
   687     | clause_of fm = [literal_of fm]
   688   fun clauses_of (Prop_Logic.And (fm1, fm2)) = clauses_of fm1 @ clauses_of fm2
   689     | clauses_of Prop_Logic.True = [[1, ~1]]
   690     | clauses_of Prop_Logic.False = [[1], [~1]]
   691     | clauses_of fm = [clause_of fm]
   692 
   693   fun dpll_solver fm =
   694     let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm
   695     in solve (clauses_of fm') end
   696 in
   697   SatSolver.add_solver ("dpll_p", dpll_solver)
   698 end;
   699 
   700 (* ------------------------------------------------------------------------- *)
   701 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
   702 (* the last installed solver (other than "auto" itself) that does not raise  *)
   703 (* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
   704 (* ------------------------------------------------------------------------- *)
   705 
   706 let
   707   fun auto_solver fm =
   708   let
   709     fun loop [] =
   710       SatSolver.UNKNOWN
   711       | loop ((name, solver)::solvers) =
   712       if name="auto" then
   713         (* do not call solver "auto" from within "auto" *)
   714         loop solvers
   715       else (
   716         (* apply 'solver' to 'fm' *)
   717         solver fm
   718           handle SatSolver.NOT_CONFIGURED => loop solvers
   719       )
   720   in
   721     loop (SatSolver.get_solvers ())
   722   end
   723 in
   724   SatSolver.add_solver ("auto", auto_solver)
   725 end;
   726 
   727 (* ------------------------------------------------------------------------- *)
   728 (* MiniSat 1.14                                                              *)
   729 (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
   730 (* ------------------------------------------------------------------------- *)
   731 
   732 (* ------------------------------------------------------------------------- *)
   733 (* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
   734 (* Matthews, which can output ASCII proof traces.  Replaying binary proof    *)
   735 (* traces generated by MiniSat-p_v1.14 has _not_ been implemented.           *)
   736 (* ------------------------------------------------------------------------- *)
   737 
   738 (* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
   739 (* that the latter is preferred by the "auto" solver                         *)
   740 
   741 (* There is a complication that is dealt with in the code below: MiniSat     *)
   742 (* introduces IDs for original clauses in the proof trace.  It does not (in  *)
   743 (* general) follow the convention that the original clauses are numbered     *)
   744 (* from 0 to n-1 (where n is the number of clauses in the formula).          *)
   745 
   746 let
   747   exception INVALID_PROOF of string
   748   fun minisat_with_proofs fm =
   749   let
   750     val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   751     val serial_str = serial_string ()
   752     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   753     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   754     val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
   755     val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null"
   756     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   757     fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   758     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
   759     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
   760     val cnf        = Prop_Logic.defcnf fm
   761     val result     = SatSolver.make_external_solver cmd writefn readfn cnf
   762     val _          = try File.rm inpath
   763     val _          = try File.rm outpath
   764   in  case result of
   765     SatSolver.UNSATISFIABLE NONE =>
   766     (let
   767       val proof_lines = (split_lines o File.read) proofpath
   768         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
   769       (* representation of clauses as ordered lists of literals (with duplicates removed) *)
   770       fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) =
   771         Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
   772         | clause_to_lit_list (Prop_Logic.BoolVar i) =
   773         [i]
   774         | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) =
   775         [~i]
   776         | clause_to_lit_list _ =
   777         raise INVALID_PROOF "Error: invalid clause in CNF formula."
   778       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
   779         cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   780         | cnf_number_of_clauses _ =
   781         1
   782       val number_of_clauses = cnf_number_of_clauses cnf
   783       (* int list array *)
   784       val clauses = Array.array (number_of_clauses, [])
   785       (* initialize the 'clauses' array *)
   786       fun init_array (Prop_Logic.And (fm1, fm2), n) =
   787         init_array (fm2, init_array (fm1, n))
   788         | init_array (fm, n) =
   789         (Array.update (clauses, n, clause_to_lit_list fm); n+1)
   790       val _ = init_array (cnf, 0)
   791       (* optimization for the common case where MiniSat "R"s clauses in their *)
   792       (* original order:                                                      *)
   793       val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
   794       (* search the 'clauses' array for the given list of literals 'lits', *)
   795       (* starting at index '!last_ref_clause + 1'                          *)
   796       fun original_clause_id lits =
   797       let
   798         fun original_clause_id_from index =
   799           if index = number_of_clauses then
   800             (* search from beginning again *)
   801             original_clause_id_from 0
   802           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
   803           (* testing for equality should suffice -- barring duplicate literals     *)
   804           else if Array.sub (clauses, index) = lits then (
   805             (* success *)
   806             last_ref_clause := index;
   807             SOME index
   808           ) else if index = !last_ref_clause then
   809             (* failure *)
   810             NONE
   811           else
   812             (* continue search *)
   813             original_clause_id_from (index + 1)
   814       in
   815         original_clause_id_from (!last_ref_clause + 1)
   816       end
   817       fun int_from_string s =
   818         (case Int.fromString s of
   819           SOME i => i
   820         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered)."))
   821       (* parse the proof file *)
   822       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   823       val empty_id      = Unsynchronized.ref ~1
   824       (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
   825       (* our proof format, where original clauses are numbered starting from 0  *)
   826       val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
   827       fun sat_to_proof id = (
   828         case Inttab.lookup (!clause_id_map) id of
   829           SOME id' => id'
   830         | NONE     => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.")
   831       )
   832       val next_id = Unsynchronized.ref (number_of_clauses - 1)
   833       fun process_tokens [] =
   834         ()
   835         | process_tokens (tok::toks) =
   836         if tok="R" then (
   837           case toks of
   838             id::sep::lits =>
   839             let
   840               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   841               val cid      = int_from_string id
   842               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   843               val ls       = sort int_ord (map int_from_string lits)
   844               val proof_id = case original_clause_id ls of
   845                                SOME orig_id => orig_id
   846                              | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   847             in
   848               (* extend the mapping of clause IDs with this newly defined ID *)
   849               clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   850                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   851               (* the proof itself doesn't change *)
   852             end
   853           | _ =>
   854             raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
   855         ) else if tok="C" then (
   856           case toks of
   857             id::sep::ids =>
   858             let
   859               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   860               val cid      = int_from_string id
   861               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   862               (* ignore the pivot literals in MiniSat's trace *)
   863               fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
   864                 | unevens (x :: [])      = x :: []
   865                 | unevens (x :: _ :: xs) = x :: unevens xs
   866               val rs       = (map sat_to_proof o unevens o map int_from_string) ids
   867               (* extend the mapping of clause IDs with this newly defined ID *)
   868               val proof_id = Unsynchronized.inc next_id
   869               val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   870                                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   871             in
   872               (* update clause table *)
   873               clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
   874                 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
   875             end
   876           | _ =>
   877             raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
   878         ) else if tok="D" then (
   879           case toks of
   880             [id] =>
   881             let
   882               val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   883               val _ = sat_to_proof (int_from_string id)
   884             in
   885               (* simply ignore "D" *)
   886               ()
   887             end
   888           | _ =>
   889             raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
   890         ) else if tok="X" then (
   891           case toks of
   892             [id1, id2] =>
   893             let
   894               val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   895               val _            = sat_to_proof (int_from_string id1)
   896               val new_empty_id = sat_to_proof (int_from_string id2)
   897             in
   898               (* update conflict id *)
   899               empty_id := new_empty_id
   900             end
   901           | _ =>
   902             raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
   903         ) else
   904           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   905       fun process_lines [] =
   906         ()
   907         | process_lines (l::ls) = (
   908           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   909           process_lines ls
   910         )
   911       (* proof *)
   912       val _ = process_lines proof_lines
   913       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   914     in
   915       SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   916     end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   917   | result =>
   918     result
   919   end
   920 in
   921   SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
   922 end;
   923 
   924 let
   925   fun minisat fm =
   926   let
   927     val _          = if getenv "MINISAT_HOME" = "" then raise SatSolver.NOT_CONFIGURED else ()
   928     val serial_str = serial_string ()
   929     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   930     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   931     val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
   932     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   933     fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   934     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
   935     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
   936     val result     = SatSolver.make_external_solver cmd writefn readfn fm
   937     val _          = try File.rm inpath
   938     val _          = try File.rm outpath
   939   in
   940     result
   941   end
   942 in
   943   SatSolver.add_solver ("minisat", minisat)
   944 end;
   945 
   946 (* ------------------------------------------------------------------------- *)
   947 (* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
   948 (* ------------------------------------------------------------------------- *)
   949 
   950 (* ------------------------------------------------------------------------- *)
   951 (* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if     *)
   952 (* zChaff finds that the formula is unsatisfiable, a proof of this is read   *)
   953 (* from a file "resolve_trace" that was generated by zChaff.  See the code   *)
   954 (* below for the expected format of the "resolve_trace" file.  Aside from    *)
   955 (* some basic syntactic checks, no verification of the proof is performed.   *)
   956 (* ------------------------------------------------------------------------- *)
   957 
   958 (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so   *)
   959 (* that the latter is preferred by the "auto" solver                         *)
   960 
   961 let
   962   exception INVALID_PROOF of string
   963   fun zchaff_with_proofs fm =
   964   case SatSolver.invoke_solver "zchaff" fm of
   965     SatSolver.UNSATISFIABLE NONE =>
   966     (let
   967       (* FIXME File.tmp_path (!?) *)
   968       val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
   969         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   970       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
   971             cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   972         | cnf_number_of_clauses _ = 1
   973       fun int_from_string s = (
   974         case Int.fromString s of
   975           SOME i => i
   976         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   977       )
   978       (* parse the "resolve_trace" file *)
   979       val clause_offset = Unsynchronized.ref ~1
   980       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   981       val empty_id      = Unsynchronized.ref ~1
   982       fun process_tokens [] =
   983         ()
   984         | process_tokens (tok::toks) =
   985         if tok="CL:" then (
   986           case toks of
   987             id::sep::ids =>
   988             let
   989               val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
   990               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
   991               val cid = int_from_string id
   992               val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   993               val rs  = map int_from_string ids
   994             in
   995               (* update clause table *)
   996               clause_table := Inttab.update_new (cid, rs) (!clause_table)
   997                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
   998             end
   999           | _ =>
  1000             raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
  1001         ) else if tok="VAR:" then (
  1002           case toks of
  1003             id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
  1004             let
  1005               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
  1006               (* set 'clause_offset' to the largest used clause ID *)
  1007               val _   = if !clause_offset = ~1 then clause_offset :=
  1008                 (case Inttab.max (!clause_table) of
  1009                   SOME (id, _) => id
  1010                 | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
  1011                 else
  1012                   ()
  1013               val vid = int_from_string id
  1014               val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
  1015               val _   = int_from_string levid
  1016               val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
  1017               val _   = int_from_string valid
  1018               val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
  1019               val aid = int_from_string anteid
  1020               val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
  1021               val ls  = map int_from_string lits
  1022               (* convert the data provided by zChaff to our resolution-style proof format *)
  1023               (* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
  1024               (* given by the literals in the antecedent clause                           *)
  1025               (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
  1026               val cid = !clause_offset + vid
  1027               (* the low bit of each literal gives its sign (positive/negative), therefore  *)
  1028               (* we have to divide each literal by 2 to obtain the proper variable ID; then *)
  1029               (* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
  1030               val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
  1031               val rs   = aid :: map (fn v => !clause_offset + v) vids
  1032             in
  1033               (* update clause table *)
  1034               clause_table := Inttab.update_new (cid, rs) (!clause_table)
  1035                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
  1036             end
  1037           | _ =>
  1038             raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
  1039         ) else if tok="CONF:" then (
  1040           case toks of
  1041             id::sep::ids =>
  1042             let
  1043               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
  1044               val cid = int_from_string id
  1045               val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
  1046               val ls  = map int_from_string ids
  1047               (* the conflict clause must be resolved with the unit clauses *)
  1048               (* for its literals to obtain the empty clause                *)
  1049               val vids         = map (fn l => l div 2) ls
  1050               val rs           = cid :: map (fn v => !clause_offset + v) vids
  1051               val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1
  1052             in
  1053               (* update clause table and conflict id *)
  1054               clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
  1055                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
  1056               empty_id     := new_empty_id
  1057             end
  1058           | _ =>
  1059             raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
  1060         ) else
  1061           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
  1062       fun process_lines [] =
  1063         ()
  1064         | process_lines (l::ls) = (
  1065           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
  1066           process_lines ls
  1067         )
  1068       (* proof *)
  1069       val _ = process_lines proof_lines
  1070       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
  1071     in
  1072       SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
  1073     end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
  1074   | result =>
  1075     result
  1076 in
  1077   SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
  1078 end;
  1079 
  1080 let
  1081   fun zchaff fm =
  1082   let
  1083     val _          = if getenv "ZCHAFF_HOME" = "" then raise SatSolver.NOT_CONFIGURED else ()
  1084     val serial_str = serial_string ()
  1085     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
  1086     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
  1087     val cmd        = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
  1088     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
  1089     fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
  1090     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
  1091     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
  1092     val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1093     val _          = try File.rm inpath
  1094     val _          = try File.rm outpath
  1095   in
  1096     result
  1097   end
  1098 in
  1099   SatSolver.add_solver ("zchaff", zchaff)
  1100 end;
  1101 
  1102 (* ------------------------------------------------------------------------- *)
  1103 (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
  1104 (* ------------------------------------------------------------------------- *)
  1105 
  1106 let
  1107   fun berkmin fm =
  1108   let
  1109     val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1110     val serial_str = serial_string ()
  1111     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
  1112     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
  1113     val exec       = getenv "BERKMIN_EXE"
  1114     val cmd        = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
  1115     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
  1116     fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
  1117     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
  1118     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
  1119     val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1120     val _          = try File.rm inpath
  1121     val _          = try File.rm outpath
  1122   in
  1123     result
  1124   end
  1125 in
  1126   SatSolver.add_solver ("berkmin", berkmin)
  1127 end;
  1128 
  1129 (* ------------------------------------------------------------------------- *)
  1130 (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
  1131 (* ------------------------------------------------------------------------- *)
  1132 
  1133 let
  1134   fun jerusat fm =
  1135   let
  1136     val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1137     val serial_str = serial_string ()
  1138     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
  1139     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
  1140     val cmd        = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
  1141     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
  1142     fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
  1143     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
  1144     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
  1145     val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1146     val _          = try File.rm inpath
  1147     val _          = try File.rm outpath
  1148   in
  1149     result
  1150   end
  1151 in
  1152   SatSolver.add_solver ("jerusat", jerusat)
  1153 end;
  1154