From 9dadb67fc97c84334019c345d776d3a1c219ab8f Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 16 Jul 2016 15:55:26 +0200 Subject: [PATCH] [bugfix] Sort false atoms by levels in new clauses When a new clauses is added and it is a conflict (i.e all atoms are false), one must take care of which literals to watch. In order to work, the watched literals must be those with the higher decision levels, or else the watched literals might not react when needed. This is fixed by sorting the literals in decreasing order of decision level when adding a new clause which happens to be false in the current trail. --- solver/internal.ml | 67 ++++++++++++++++++------------------- solver/res.ml | 9 +++-- solver/solver_types.ml | 13 +++---- solver/solver_types_intf.ml | 3 +- 4 files changed, 42 insertions(+), 50 deletions(-) diff --git a/solver/internal.ml b/solver/internal.ml index 8a79bea4..716581b6 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -304,7 +304,8 @@ module Make let partition atoms = (* Parittion litterals for new clauses *) let rec partition_aux trues unassigned falses history = function - | [] -> trues @ unassigned @ falses, history + | [] -> + trues @ unassigned @ falses, history | a :: r -> if a.is_true then if a.var.v_level = 0 then raise Trivial @@ -352,27 +353,18 @@ module Make (* Adding/removing clauses *) let attach_clause c = if not c.attached then begin + Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c); c.attached <- true; Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c; - if c.learnt then - env.learnts_literals <- env.learnts_literals + Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals + Vec.size c.atoms end let detach_clause c = if c.attached then begin c.attached <- false; Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c); - (* Not necessary, cleanup is done during propagation - Vec.remove (Vec.get c.atoms 0).neg.watched c; - Vec.remove (Vec.get c.atoms 1).neg.watched c; - *) - if c.learnt then - env.learnts_literals <- env.learnts_literals - Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals - Vec.size c.atoms + Vec.remove (Vec.get c.atoms 0).neg.watched c; + Vec.remove (Vec.get c.atoms 1).neg.watched c; end let remove_clause c = detach_clause c @@ -383,6 +375,7 @@ module Make (* cancel down to [lvl] excluded *) let cancel_until lvl = if decision_level () > lvl then begin + Log.debugf 5 "Backtracking to lvl %d" (fun k -> k lvl); env.elt_head <- Vec.get env.elt_levels lvl; env.th_head <- env.elt_head; for c = env.elt_head to Vec.size env.elt_queue - 1 do @@ -424,10 +417,8 @@ module Make begin match l with | [ a ] -> if history = [] then r - else begin - let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in - Bcp tmp_cl - end + else + Bcp (make_clause (fresh_tname ()) l 1 (History (cl :: history))) | _ -> assert false end | r -> r @@ -522,7 +513,8 @@ module Make end done; assert false with Exit -> - let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in + let learnt = List.fast_sort ( + fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in let blevel = backtrack_lvl !is_uip learnt in blevel, learnt, List.rev !history, !is_uip @@ -542,7 +534,10 @@ module Make let history = ref [] in assert (decision_level () > 0); while !cond do - if !c.learnt then clause_bump_activity !c; + begin match !c.cpremise with + | History _ -> clause_bump_activity !c + | Hyp _ | Lemma _ -> () + end; history := !c :: !history; (* visit the current predecessors *) for j = 0 to Vec.size !c.atoms - 1 do @@ -601,13 +596,13 @@ module Make report_unsat confl else begin let name = fresh_lname () in - let uclause = make_clause name learnt (List.length learnt) true history in + let uclause = make_clause name learnt (List.length learnt) history in Vec.push env.clauses_learnt uclause; enqueue_bool fuip 0 (Bcp uclause) end | fuip :: _ -> let name = fresh_lname () in - let lclause = make_clause name learnt (List.length learnt) true history in + let lclause = make_clause name learnt (List.length learnt) history in Vec.push env.clauses_learnt lclause; attach_clause lclause; clause_bump_activity lclause; @@ -643,7 +638,7 @@ module Make let clause = if history = [] then init else make_clause ?tag:init.tag (fresh_name ()) - atoms size true (History (init :: history)) + atoms size (History (init :: history)) in Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); Vec.push vec clause; @@ -651,15 +646,18 @@ module Make | [] -> report_unsat clause | a::b::_ -> - attach_clause clause; if a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in - cancel_until lvl; - add_boolean_conflict clause - end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in - cancel_until lvl; - enqueue_bool a lvl (Bcp clause) + Vec.sort clause.atoms (fun a b -> + compare b.var.v_level a.var.v_level); + attach_clause clause; + add_boolean_conflict init + end else begin + attach_clause clause; + if b.neg.is_true && not a.is_true && not a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in + cancel_until lvl; + enqueue_bool a lvl (Bcp clause) + end end | [a] -> Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); @@ -681,8 +679,7 @@ module Make (* true clause, keep it in watched *) Vec.set watched !new_sz c; incr new_sz; - end - else + end else try (* look for another watch lit *) for k = 2 to Vec.size atoms - 1 do let ak = Vec.get atoms k in @@ -743,7 +740,7 @@ module Make let atoms = List.rev_map (fun x -> new_atom x) l in Iheap.grow_to_by_double env.order (St.nb_elt ()); List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms; - let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) in + let c = make_clause (fresh_tname ()) atoms (List.length atoms) (Lemma lemma) in add_clause c let slice_propagate f lvl = @@ -781,7 +778,7 @@ module Make let l = List.rev_map new_atom l in Iheap.grow_to_by_double env.order (St.nb_elt ()); List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; - let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in + let c = St.make_clause (St.fresh_tname ()) l (List.length l) (Lemma p) in Some c end @@ -963,7 +960,7 @@ module Make let add_clauses ?tag cnf = let aux cl = let c = make_clause ?tag (fresh_hname ()) - cl (List.length cl) false (Hyp (current_level ())) in + cl (List.length cl) (Hyp (current_level ())) in add_clause c; (* Clauses can be added after search has begun (and thus we are not at level 0, so better not do anything at this point. diff --git a/solver/res.ml b/solver/res.ml index 2195ef0d..b74a0cc9 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -83,7 +83,7 @@ module Make(St : Solver_types.S) = struct cmp_cl (to_list c) (to_list d) let prove conclusion = - assert St.(conclusion.learnt || conclusion.cpremise <> History []); + assert St.(conclusion.cpremise <> History []); conclusion let prove_unsat c = @@ -93,7 +93,7 @@ module Make(St : Solver_types.S) = struct | Some St.Bcp d -> d | _ -> assert false) l in - St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l)) + St.make_clause (fresh_pcl_name ()) [] 0 (St.History (c :: l)) let prove_atom a = if St.(a.is_true && a.var.v_level = 0) then begin @@ -126,8 +126,8 @@ module Make(St : Solver_types.S) = struct begin match r with | [] -> (l, c, d, a) | _ -> - let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true - (St.History [c; d]) in + let new_clause = St.make_clause (fresh_pcl_name ()) + l (List.length l) (St.History [c; d]) in chain_res (new_clause, l) r end | _ -> assert false @@ -140,7 +140,6 @@ module Make(St : Solver_types.S) = struct | St.Lemma l -> {conclusion; step = Lemma l; } | St.Hyp _ -> - assert (not conclusion.St.learnt); { conclusion; step = Hypothesis; } | St.History [] -> assert false diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 524d08f6..76894b3a 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -58,7 +58,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct name : string; tag : int option; atoms : atom Vec.t; - learnt : bool; c_level : int; mutable cpremise : premise; mutable activity : float; @@ -106,7 +105,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct activity = -1.; attached = false; c_level = -1; - learnt = false; visited = false; cpremise = History [] } @@ -182,7 +180,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let var, negated = make_boolean_var lit in if negated then var.na else var.pa - let make_clause ?tag name ali sz_ali is_learnt premise = + let make_clause ?tag name ali sz_ali premise = let atoms = Vec.from_list ali sz_ali dummy_atom in let level = match premise with @@ -195,12 +193,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct atoms = atoms; attached = false; visited = false; - learnt = is_learnt; c_level = level; activity = 0.; cpremise = premise} - let empty_clause = make_clause "Empty" [] 0 false (History []) + let empty_clause = make_clause "Empty" [] 0 (History []) (* Decisions & propagations *) type t = (lit, atom) Either.t @@ -298,9 +295,9 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let pp_atoms_vec out vec = Vec.print ~sep:"" pp_atom out vec - let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} = - Format.fprintf out "%s%s@[{@[%a@]}@ cpremise={@[%a@]}@]" - name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp + let pp_clause out {name=name; atoms=arr; cpremise=cp; } = + Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" + name pp_atoms_vec arr pp_premise cp end diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index 740ee05d..619558f4 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -53,7 +53,6 @@ module type S = sig name : string; tag : int option; atoms : atom Vec.t; - learnt : bool; c_level : int; mutable cpremise : premise; mutable activity : float; @@ -117,7 +116,7 @@ module type S = sig val empty_clause : clause (** The empty clause *) - val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause + val make_clause : ?tag:int -> string -> atom list -> int -> premise -> clause (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) (** {2 Clause names} *)