From 6221a61ff0f5e40674dfca60a481fe8235eed397 Mon Sep 17 00:00:00 2001 From: OCamlPro-Iguernlala Date: Wed, 9 Nov 2016 13:14:07 +0100 Subject: [PATCH] bugfix in maximiszation: Sometimes, the simplex says "unbounded" on trivially bounded problems: (TODO: => improve code) --- src/solveBounds.ml | 131 +++++++++++++++++++++++++++++++-------------- 1 file changed, 91 insertions(+), 40 deletions(-) diff --git a/src/solveBounds.ml b/src/solveBounds.ml index 37d084c..216c435 100644 --- a/src/solveBounds.ml +++ b/src/solveBounds.ml @@ -200,20 +200,35 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct with Exit -> !acc + type 'a maximiza_basic = + | Free + | Stuck + | Progress of 'a + + let basic_var_to_pivot_for_maximization = - let choose_best_pivot acc s si p c_px bnd is_min = - let tmp = if is_min then R2.sub si.value bnd else R2.sub bnd si.value in - let ratio = R2.div_by_const (R.abs c_px) tmp in - begin match !acc with - | None -> acc := Some (ratio, s, si, p, c_px, bnd, is_min) - | Some (r_old,_,_,_,_,_,_) -> - if R2.compare r_old ratio > 0 then - acc := Some (ratio, s, si, p, c_px, bnd, is_min) - end; - if R2.is_zero ratio then raise Exit (* in the case, the pivot is found *) + let choose_best_pivot acc s si p c_px bnd_opt is_min = + match bnd_opt with + | None -> + if !acc = Stuck then acc := Free (* !!! to check *) + + | Some bnd -> + let tmp = if is_min then R2.sub si.value bnd else R2.sub bnd si.value in + let ratio = R2.div_by_const (R.abs c_px) tmp in + begin + match !acc with + | Free | Stuck -> + acc := Progress (ratio, s, si, p, c_px, bnd, is_min) + + | Progress (r_old,_,_,_,_,_,_) -> + if R2.compare r_old ratio > 0 then + acc := Progress (ratio, s, si, p, c_px, bnd, is_min) + end; + if R2.is_zero ratio then raise Exit (* in the case, the pivot is found*) in fun {basic; _} x use_x should_incr_x -> - let acc = ref None in + (* Initially, we assume that we are stuck, unless, use_x is empty *) + let acc = ref (if SX.is_empty use_x then Free else Stuck) in try SX.iter (fun s -> @@ -222,50 +237,59 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct let sg = R.sign c_px in assert (sg <> 0); match should_incr_x, sg > 0, si.mini, si.maxi with - | true , true , _, Some mx -> + | true , true , _, mx_opt -> (* by increasing x, s will increase and max(s) <> +infty *) - choose_best_pivot acc s si p c_px mx false + choose_best_pivot acc s si p c_px mx_opt false - | true , false, Some mn, _ -> + | true , false, mn_opt, _ -> (* by increasing x, s will decrease and min(s) <> -infty *) - choose_best_pivot acc s si p c_px mn true + choose_best_pivot acc s si p c_px mn_opt true - | false, true , Some mn, _ -> + | false, true , mn_opt, _ -> (* by decreasing x, s will decreease and min(s) <> -infty *) - choose_best_pivot acc s si p c_px mn true + choose_best_pivot acc s si p c_px mn_opt true - | false, false, _, Some mx -> + | false, false, _, mx_opt -> (* by decreasning x, s will increase and max(s) <> +infty *) - choose_best_pivot acc s si p c_px mx false + choose_best_pivot acc s si p c_px mx_opt false - | true, true, _, None + (*| true, true, _, None | true, false, None, _ | false, true, None, _ | false, false, _, None -> (* for the cases where max or max = infty, we keep acc unchanged. if acc = None at the end, the problem is unbounded *) () + *) )use_x; !acc with Exit -> !acc - let can_fix_valuation_without_pivot should_incr xi ratio = + let can_fix_valuation_without_pivot should_incr xi ratio_opt = if should_incr then - match xi.maxi with - | None -> None - | Some bnd -> + match xi.maxi, ratio_opt with + | None, _ -> None + | Some bnd, Some ratio -> let diff = R2.sub bnd xi.value in if R2.compare diff ratio < 0 then Some ({xi with value = bnd}, diff) else None + + | Some bnd, None -> + let diff = R2.sub bnd xi.value in + Some ({xi with value = bnd}, diff) + else - match xi.mini with - | None -> None - | Some bnd -> + match xi.mini, ratio_opt with + | None, _ -> None + | Some bnd, Some ratio -> let diff = R2.sub xi.value bnd in if R2.compare diff ratio < 0 then Some ({xi with value = bnd}, diff) else None + | Some bnd, None -> + let diff = R2.sub xi.value bnd in + Some ({xi with value = bnd}, diff) let update_valuation_without_pivot @@ -286,29 +310,55 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct {env with basic; non_basic} let rec maximize_rec env opt rnd = - if false then + if env.debug > 1 then Format.eprintf "[maximize_rec] round %d // OPT = %a@." rnd P.print opt; Core.debug (Format.sprintf "[maximize_rec] round %d" rnd) env (Result.get None); Core.check_invariants env (Result.get None); match non_basic_to_maximize env opt with | None -> - if false then Format.eprintf "max reached@."; + if env.debug > 1 then Format.eprintf "max reached@."; rnd, env, Some (opt, true) (* max reached *) + | Some (_x, _c, _xi, _use_x, _should_incr) -> - if false then Format.eprintf "pivot non basic var %a ?@." Var.print _x; + if env.debug > 1 then + Format.eprintf "pivot non basic var %a ?@." Var.print _x; match basic_var_to_pivot_for_maximization env _x _use_x _should_incr with - | None -> - if false then + | Free -> + if env.debug > 1 then + Format.eprintf + "non basic %a not constrained by basic vars: Set it to max@." + Var.print _x; + begin + match can_fix_valuation_without_pivot _should_incr _xi None with + | Some (new_xi, diff) -> + if env.debug > 1 then + Format.eprintf + "No --> I can set value of %a to min/max WO pivot@." + Var.print _x; + let env, opt = + update_valuation_without_pivot + env _x _use_x new_xi diff _should_incr, opt + in + maximize_rec env opt (rnd + 1) + | None -> + if env.debug > 1 then + Format.eprintf "no pivot finally(no upper bnd), pb unbounded@."; + rnd, env, Some (opt, false) (* unbounded *) + end + | Stuck -> + if env.debug > 1 then Format.eprintf "no pivot finally, pb unbounded@."; rnd, env, Some (opt, false) (* unbounded *) - | Some (ratio, s, si, p, c_px, bnd, _is_min) -> - if false then + + | Progress (ratio, s, si, p, c_px, bnd, _is_min) -> + if env.debug > 1 then Format.eprintf "pivot with basic var %a ?@." Var.print s; let env, opt = - match can_fix_valuation_without_pivot _should_incr _xi ratio with + match + can_fix_valuation_without_pivot _should_incr _xi (Some ratio) with | Some (new_xi, diff) -> - if false then + if env.debug > 1 then Format.eprintf "No --> I can set value of %a to min/max WO pivot@." Var.print _x; @@ -414,7 +464,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct | UNK -> assert false | UNSAT _ -> env, None | SAT -> - if false then + if env.debug > 1 then Format.eprintf "[maximize] pb SAT! try to maximize %a@." P.print opt0; let {basic; non_basic; _} = env in let unbnd = ref false in @@ -432,13 +482,14 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct if !unbnd then env, Some (opt, false) (* unbounded *) else begin - if false then Format.eprintf "start maximization@."; + if env.debug > 1 then Format.eprintf "start maximization@."; let rnd, env, is_max = maximize_rec env opt 1 in Core.check_invariants env (Result.get is_max); - if false then + if env.debug > 1 then Format.eprintf "[maximize] pb SAT! Max found ? %b for %a == %a@." (is_max != None) P.print opt0 P.print opt; - if false then Format.eprintf "maximization done after %d steps@." rnd; + if env.debug > 1 then + Format.eprintf "maximization done after %d steps@." rnd; env, is_max end