diff --git a/sat/res.ml b/sat/res.ml index a12da3a7..5712d6e9 100644 --- a/sat/res.ml +++ b/sat/res.ml @@ -6,163 +6,257 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make(St : Solver_types.S)(Proof : sig type t end) = struct +module Make(St : Solver_types.S)(Proof : sig type proof end) = struct - (* Type definitions *) - type lemma = Proof.t - type clause = St.clause - type atom = St.atom - type int_cl = St.atom list + (* Type definitions *) + type lemma = Proof.proof + type clause = St.clause + type atom = St.atom + type int_cl = clause * St.atom list - type node = - | Assumption - | Lemma of lemma - | Resolution of atom * int_cl * int_cl - (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) + type node = + | Assumption + | Lemma of lemma + | Resolution of atom * int_cl * int_cl + (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) - exception Tautology - exception Resolution_error of string + exception Resolution_error of string - (* Proof graph *) - module H = Hashtbl.Make(struct - type t = St.atom list - let hash= Hashtbl.hash - let equal = List.for_all2 (==) + (* Proof graph *) + let hash_cl cl = + Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl) + + let equal_cl cl_c cl_d = + try + List.for_all2 (==) cl_c cl_d + with Invalid_argument _ -> + false + + module H = Hashtbl.Make(struct + type t = St.atom list + let hash = hash_cl + let equal = equal_cl end) - let proof : node H.t = H.create 1007;; + let proof : node H.t = H.create 1007;; - (* Misc functions *) - let compare_atoms a b = - Pervasives.compare St.(a.aid) St.(b.aid) + (* Misc functions *) + let equal_atoms a b = St.(a.aid) = St.(b.aid) + let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - let equal_atoms a b = St.(a.aid) = St.(b.aid) + (* Compute resolution of 2 clauses *) + let resolve l = + let rec aux resolved acc = function + | [] -> resolved, acc + | [a] -> resolved, a :: acc + | a :: b :: r -> + if equal_atoms a b then + aux resolved (a :: acc) r + else if equal_atoms St.(a.neg) b then + aux (St.(a.var.pa) :: resolved) acc r + else + aux resolved (a :: acc) (b :: r) + in + let resolved, new_clause = aux [] [] l in + resolved, List.rev new_clause + let to_list c = + let v = St.(c.atoms) in + let l = ref [] in + for i = 0 to Vec.size v - 1 do + l := (Vec.get v i) :: !l + done; + let l, res = resolve (List.sort_uniq compare_atoms !l) in + if l <> [] then + raise (Resolution_error "Input cause is a tautology"); + res - (* Compute resolution of 2 clauses *) - let resolve l = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms St.(a.neg) b then - aux (St.(a.var.pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause + (* Adding new proven clauses *) + let is_proved c = H.mem proof c + let is_proven c = is_proved (to_list c) - let to_list c = - let v = St.(c.atoms) in - let l = ref [] in - for i = 0 to Vec.size v - 1 do - l := (Vec.get v i) :: !l - done; - let l, res = resolve (List.sort_uniq compare_atoms !l) in - if l <> [] then - raise (Resolution_error "Input cause is a tautology"); - res + let add_res (c, cl_c) (d, cl_d) = + Log.debug 7 "Resolving clauses :"; + Log.debug 7 " %a" St.pp_clause c; + Log.debug 7 " %a" St.pp_clause d; + let l = List.merge compare_atoms cl_c cl_d in + let resolved, new_clause = resolve l in + match resolved with + | [] -> raise (Resolution_error "No literal to resolve over") + | [a] -> + H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); + let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in + Log.debug 5 "New clause : %a" St.pp_clause new_c; + new_c, new_clause + | _ -> raise (Resolution_error "Resolved to a tautology") - (* Adding new proven clauses *) - let is_proved c = H.mem proof c + let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *) + match l with + | a :: ((_ :: _) as r) -> + let new_c, new_cl = List.fold_left add_res a r in + assert (equal_cl cl new_cl) + | _ -> assert false - let rec add_res c d = - add_clause c; - add_clause d; - let cl_c = to_list c in - let cl_d = to_list d in - let l = List.merge compare_atoms cl_c cl_d in - let resolved, new_clause = resolve l in - match resolved with - | [] -> raise (Resolution_error "No literal to resolve over") - | [a] -> - H.add proof new_clause (Resolution (a, cl_c, cl_d)); - new_clause - | _ -> raise (Resolution_error "Resolved to a tautology") + let need_clause (c, cl) = + if is_proved cl then + [] + else if not St.(c.learnt) then begin + Log.debug 8 "Adding to hyps : %a" St.pp_clause c; + H.add proof cl Assumption; + [] + end else + St.(c.cpremise) - and add_clause c = - let cl = to_list c in - if is_proved cl then - () - else if not St.(c.learnt) then - H.add proof cl Assumption - else begin - let history = St.(c.cpremise) in - () - (* TODO - match history with - | a :: (_ :: _) as r -> - List.fold_left add_res a r - *) - end + let rec do_clause = function + | [] -> () + | c :: r -> + let cl = to_list c in + let l = need_clause (c, cl) in + if l = [] then (* c is either an asusmption, or already proved *) + do_clause r + else + let l' = List.rev_map (fun c -> c, to_list c) l in + let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in + let to_prove = List.rev_map fst to_prove in + if to_prove = [] then begin + (* See wether we can prove c right now *) + add_clause cl l'; + do_clause r + end else + (* Or if we have to prove some other clauses first *) + do_clause (to_prove @ (c :: r)) - (* Print proof graph *) - let _i = ref 0 - let new_id () = incr _i; "id_" ^ (string_of_int !_i) + let prove c = + Log.debug 3 "Proving : %a" St.pp_clause c; + do_clause [c]; + Log.debug 3 "Proved : %a" St.pp_clause c - let ids : (bool * string) H.t = H.create 1007;; - let cl_id c = - try - snd (H.find ids c) - with Not_found -> - let id = new_id () in - H.add ids c (false, id); - id + let clause_unit a = St.( + let l = if a.is_true then [a] else [a.neg] in + make_clause (fresh_name ()) l 1 true a.var.vpremise + ) - let is_drawn c = - try - fst (H.find ids c) - with Not_found -> - false + let rec prove_unsat_cl (c, cl) = match cl with + | [] -> true + | a :: r -> + try + Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; + let d = match St.(a.var.level, a.var.reason) with + | 0, Some d -> d + | 0, None -> clause_unit a + | _ -> raise Exit + in + prove d; + let cl_d = to_list d in + prove_unsat_cl (add_res (c, cl) (d, cl_d)) + with Exit -> false - let has_drawn c = - assert (H.mem ids c); - let b, id = H.find ids c in - assert (not b); - H.replace ids c (true, id) + exception Cannot + let assert_can_prove_unsat c = + Log.debug 1 "=================== Proof ====================="; + prove c; + if not (prove_unsat_cl (c, to_list c)) then raise Cannot - let print_atom fmt a = - Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1) + (* Interface exposed *) + type proof_node = { + conclusion : clause; + step : step; + } + and proof = unit -> proof_node + and step = + | Hypothesis + | Lemma of lemma + | Resolution of proof * proof * atom - let rec print_clause fmt = function - | [] -> Format.fprintf fmt "[]" - | [a] -> print_atom fmt a - | a :: (_ :: _) as r -> Format.fprintf fmt "%a \\/ %a" print_atom a print_clause r + let rec return_proof (c, cl) () = + Log.debug 8 "Returning proof for : %a" St.pp_clause c; + let st = match H.find proof cl with + | Assumption -> Hypothesis + | Lemma l -> Lemma l + | Resolution (a, cl_c, cl_d) -> + Resolution (return_proof cl_c, return_proof cl_d, a) + in + { conclusion = c; step = st } - let print_dot_rule f arg fmt cl = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - (cl_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\">" f arg + let prove_unsat c = + assert_can_prove_unsat c; + return_proof (St.empty_clause, []) - let print_dot_edge c fmt d = - Format.fprintf fmt "%s -> %s;@\n" (cl_id c) (cl_id d) + (* Print proof graph *) + let _i = ref 0 + let new_id () = incr _i; "id_" ^ (string_of_int !_i) - let print_dot_proof fmt cl = - match H.find proof cl with - | Assumption -> - let aux fmt () = - Format.fprintf fmt "%a" print_clause cl - in - print_dot_rule aux () fmt cl - | Lemma _ -> - let aux fmt () = - Format.fprintf fmt "%ato prove ..." print_clause cl - in - print_dot_rule aux () fmt cl - | Resolution (r, c, d) -> - let aux fmt () = - Format.fprintf fmt "%a%a" - print_clause cl print_atom r - in - Format.fprintf fmt "%a%a%a" - (print_dot_rule aux ()) cl - (print_dot_edge cl) c - (print_dot_edge cl) d + let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; + let c_id c = + try + snd (Hashtbl.find ids c) + with Not_found -> + let id = new_id () in + Hashtbl.add ids c (false, id); + id - let print_dot fmt cl = - assert (is_proved cl); - Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof cl + let clear_ids () = + Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids + + let is_drawn c = + try + fst (Hashtbl.find ids c) + with Not_found -> + false + + let has_drawn c = + assert (Hashtbl.mem ids c); + let b, id = Hashtbl.find ids c in + assert (not b); + Hashtbl.replace ids c (true, id) + + let print_atom fmt a = + Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1) + + let rec print_cl fmt = function + | [] -> Format.fprintf fmt "[]" + | [a] -> print_atom fmt a + | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r + + let print_clause fmt c = print_cl fmt (to_list c) + + let print_dot_rule f arg fmt cl = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg + + let print_dot_edge c fmt d = + Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d) + + let rec print_dot_proof fmt p = + match p.step with + | Hypothesis -> + let aux fmt () = + Format.fprintf fmt "%a" + print_clause p.conclusion + in + print_dot_rule aux () fmt p.conclusion + | Lemma _ -> + let aux fmt () = + Format.fprintf fmt "%ato prove ..." + print_clause p.conclusion + in + print_dot_rule aux () fmt p.conclusion + | Resolution (proof1, proof2, a) -> + let aux fmt () = + Format.fprintf fmt "%a%a" + print_clause p.conclusion print_atom a + in + let p1 = proof1 () in + let p2 = proof2 () in + Format.fprintf fmt "%a%a%a%a%a" + (print_dot_rule aux ()) p.conclusion + (print_dot_edge p.conclusion) p1.conclusion + (print_dot_edge p.conclusion) p2.conclusion + print_dot_proof p1 + print_dot_proof p2 + + let print_dot fmt proof = + clear_ids (); + Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ()) end diff --git a/sat/res.mli b/sat/res.mli index 5d3fbf14..e8e9d0ab 100644 --- a/sat/res.mli +++ b/sat/res.mli @@ -6,5 +6,5 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : functor (St : Solver_types.S)(Proof : sig type t end) - -> S with type clause = St.clause and type lemma = Proof.t +module Make : functor (St : Solver_types.S)(Proof : sig type proof end) + -> S with type atom= St.atom and type clause = St.clause and type lemma = Proof.proof diff --git a/sat/res_intf.ml b/sat/res_intf.ml index 5e732ab7..4f245ee9 100644 --- a/sat/res_intf.ml +++ b/sat/res_intf.ml @@ -1,7 +1,33 @@ (* Copyright 2014 Guillaume Bury *) module type S = sig + + type atom type clause type lemma + val is_proven : clause -> bool + (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *) + + exception Cannot + val assert_can_prove_unsat : clause -> unit + (** [prove_unsat c] tries and prove the empty clause from [c]. + @raise Cannot if it is impossible. *) + + type proof_node = { + conclusion : clause; + step : step; + } + and proof = unit -> proof_node + and step = + | Hypothesis + | Lemma of lemma + | Resolution of proof * proof * atom + + val prove_unsat : clause -> proof + (** Given a conflict clause [c], returns a proof of the empty clause. *) + + val print_dot : Format.formatter -> proof -> unit + (** Print the given proof in dot format on the given formatter. *) + end diff --git a/sat/sat.ml b/sat/sat.ml index 57092e98..ec73246d 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -75,14 +75,15 @@ module Make(Dummy : sig end) = struct exception Bad_atom + type atom = Fsat.t + type proof = SatSolver.Proof.proof + type res = | Sat | Unsat let _i = ref 0 - type atom = Fsat.t - let new_atom () = try Fsat.create () @@ -117,4 +118,12 @@ module Make(Dummy : sig end) = struct with SatSolver.Unsat _ -> () let eval = SatSolver.eval + + let get_proof () = + match SatSolver.unsat_conflict () with + | None -> assert false + | Some c -> SatSolver.Proof.prove_unsat c + + let print_proof = SatSolver.Proof.print_dot + end diff --git a/sat/sat.mli b/sat/sat.mli index bf3bc55f..2f7b61d3 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -9,6 +9,9 @@ module Make(Dummy: sig end) : sig type atom = private int (** Type for atoms, i.e boolean literals. *) + type proof + (** Abstract type for resolution proofs *) + type res = Sat | Unsat (** Type of results returned by the solve function. *) @@ -44,5 +47,11 @@ module Make(Dummy: sig end) : sig val assume : atom list list -> unit (** Add a list of clauses to the set of assumptions. *) + val get_proof : unit -> proof + (** Returns the resolution proof found, if [solve] returned [Unsat]. *) + + val print_proof : Format.formatter -> proof -> unit + (** Print the given proof in dot format. *) + end diff --git a/sat/solver.ml b/sat/solver.ml index 26729ebf..5238440e 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -16,6 +16,7 @@ module Make (F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) = struct open St + module Proof = Res.Make(St)(Th) exception Sat exception Unsat of clause list @@ -31,6 +32,9 @@ module Make (F : Formula_intf.S) mutable unsat_core : clause list; (* clauses that imply false, if any *) + mutable unsat_conflict : clause option; + (* conflict clause at decision level 0, if any *) + clauses : clause Vec.t; (* all currently active clauses *) @@ -116,6 +120,7 @@ module Make (F : Formula_intf.S) let env = { is_unsat = false; unsat_core = [] ; + unsat_conflict = None; clauses = Vec.make 0 dummy_clause; (*updated during parsing*) learnts = Vec.make 0 dummy_clause; (*updated during parsing*) clause_inc = 1.; @@ -559,6 +564,7 @@ module Make (F : Formula_intf.S) *) env.is_unsat <- true; env.unsat_core <- unsat_core; + env.unsat_conflict <- Some confl; raise (Unsat unsat_core) @@ -908,6 +914,9 @@ module Make (F : Formula_intf.S) let truth = var.pa.is_true in if negated then not truth else truth + + let unsat_conflict () = env.unsat_conflict + type level = int let base_level = 0 diff --git a/sat/solver.mli b/sat/solver.mli index 792530f5..ea651928 100644 --- a/sat/solver.mli +++ b/sat/solver.mli @@ -21,6 +21,11 @@ sig exception Unsat of St.clause list + module Proof : Res.S with + type atom = St.atom and + type clause = St.clause and + type lemma = Th.proof + val solve : unit -> unit (** Try and solves the current set of assumptions. @return () if the current set of clauses is satisfiable @@ -35,6 +40,10 @@ sig (** Returns the valuation of a formula in the current state of the sat solver. *) + val unsat_conflict : unit -> St.clause option + (** Returns the unsat clause found at the toplevel, if it exists (i.e if + [solve] has raised [Unsat]) *) + type level (** Abstract notion of assumption level. *) diff --git a/sat/solver_types.ml b/sat/solver_types.ml index ba810c41..0a8c5412 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -140,6 +140,8 @@ module Make (F : Formula_intf.S) = struct activity = 0.; cpremise = premise} + let empty_clause = make_clause "Empty" [] 0 false [] + let fresh_lname = let cpt = ref 0 in fun () -> incr cpt; "L" ^ (string_of_int !cpt) diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml index 6f2b2fc3..bcb22161 100644 --- a/sat/solver_types_intf.ml +++ b/sat/solver_types_intf.ml @@ -56,6 +56,7 @@ module type S = sig val dummy_var : var val dummy_atom : atom val dummy_clause : clause + val empty_clause : clause val make_var : formula -> var * bool diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 27ee05d9..1d9af7b4 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -7,6 +7,7 @@ exception Out_of_space (* Arguments parsing *) let file = ref "" let p_assign = ref false +let p_proof = ref false let time_limit = ref 300. let size_limit = ref 1000_000_000. @@ -40,16 +41,20 @@ let setup_gc_stat () = let input_file = fun s -> file := s let usage = "Usage : main [options] " let argspec = Arg.align [ - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - "-t", Arg.String (int_arg time_limit), - "[smhd] Sets the time limit for the sat solver"; - "-s", Arg.String (int_arg size_limit), - "[kMGT] Sets the size limit for the sat solver"; - "-model", Arg.Set p_assign, - " Outputs the boolean model found if sat"; + "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true), + " Enable stack traces"; "-gc", Arg.Unit setup_gc_stat, " Outputs statistics about the GC"; + "-model", Arg.Set p_assign, + " Outputs the boolean model found if sat"; + "-p", Arg.Set p_proof, + " Outputs the proof found (in dot format) if unsat"; + "-s", Arg.String (int_arg size_limit), + "[kMGT] Sets the size limit for the sat solver"; + "-t", Arg.String (int_arg time_limit), + "[smhd] Sets the time limit for the sat solver"; + "-v", Arg.Int (fun i -> Log.set_debug i), + " Sets the debug verbose level"; ] (* Limits alarm *) @@ -102,7 +107,11 @@ let main () = if !p_assign then print_assign Format.std_formatter () | S.Unsat -> - Format.printf "Unsat@." + Format.printf "Unsat@."; + if !p_proof then begin + let p = S.get_proof () in + S.print_proof Format.std_formatter p + end let () = try