solver.ml 11.2 KB
 Erwan Jahier committed Mar 17, 2010 1 2 3 4 5 6 7 8 9 10 ``````(*----------------------------------------------------------------------- ** Copyright (C) 2001 - Verimag. ** This file may only be copied under the terms of the GNU Library General ** Public License **----------------------------------------------------------------------- ** ** File: solver.ml ** Main author: jahier@imag.fr *) `````` Erwan Jahier committed Mar 17, 2010 11 ``````open List `````` Erwan Jahier committed Mar 17, 2010 12 ``````open Formula `````` Erwan Jahier committed Mar 17, 2010 13 ``````open Env_state `````` Erwan Jahier committed Mar 17, 2010 14 `````` `````` Erwan Jahier committed Mar 17, 2010 15 16 ``````(****************************************************************************) (****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 17 18 19 `````` `````` Erwan Jahier committed Mar 17, 2010 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 ``````(****************************************************************************) type sol_nb = (float * int) (** This type is used to represent the number of solutions of a bdd. The idea is to approximate this number of solutions by [a.2**n] where [a] is null or a float inside the interval [[1, 2[], and [n] a positive integer. The reason for that logarithmic encoding is that the number of solutions of a formula is exponential in the number of variables; this means that number of solutions is likely to trigger overflow errors. In order to compute the [sol_nb] of a bdd using the ones of its sub-branches, we take advantage of the following equality: (1) [a.2**(n+p) + b.2**n = 2**(-k).(a+b.2**(-p)).2**(n+p+k)] where [k] is the smallest integer such that: [2**(-k).(a+b.2**(-p)) < 2]. *) let rec (add_sol_nb: sol_nb -> sol_nb -> sol_nb) = fun (a, n) (b, m) -> (** Adds two [sol_nb] [(a, n)] and [(b, m)] using the formula (1) above. *) if a = 0. then (b, m) else if b = 0. then (a, n) else let _ = assert ((a >= 1.) && (a < 2.) && (b >= 1.) && (b < 2.)) in if (n > m) then add_sol_nb (b, m) (a, n) else let p = m - n in let temp = a +. b *. ((2.0)**((float_of_int (-p)))) in let k = (int_of_float (floor ((log temp) /. (log 2.0)))) in let new_cst = temp *. (2.0)**((float_of_int (-k))) in let _ = assert (((1.0 <= new_cst) && (new_cst < 2.0)) || new_cst = 0.) in (new_cst, (n+k)) let _ = assert ((add_sol_nb (1., 0) (1., 0)) = (1., 1)) let _ = assert ((add_sol_nb (1., 1) (1., 1)) = (1., 2)) let _ = assert ((add_sol_nb (1., 5) (1., 5)) = (1., 6)) (* 2^2+2^3 = 12 = 0.75 * 2^4 *) let _ = assert ((add_sol_nb (1., 2) (1., 3)) = (1.5, 2)) let _ = assert ((add_sol_nb (1., 0) (0., 1)) = (1., 0)) let _ = assert ((add_sol_nb (1.453, 45) (0., 1)) = (1.453, 45)) `````` Erwan Jahier committed Mar 17, 2010 67 68 `````` (****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 `````` type var = int (** In the following, we call a comb the bdd of a conjunction of litterals (var). They provide the ordering in which litterals appear in the bdds we manipulate. *) let rec (split_comb: Bdd.t -> var -> var list * var list) = fun comb v -> (* Splits [comb] into two list vars; the first one (resp the second one) contains variables appearing before [v] (resp after) in [comb]. [v] should appear in [comb]. *) let _ = assert (List.mem v (Bdd.int_of_support comb)) in let top = Bdd.topvar comb in let combt = (Bdd.dthen comb) in if v = top then ([], (Bdd.int_of_support combt)) else let (vars_before, vars_after) = split_comb combt v in (top::vars_before, vars_after) let (get_vars_between: var -> var -> Bdd.t -> var list) = fun v1 v2 support -> (* Returns the variables between (strictly) [v1] and [v2]. [v1] ougth to be strictly smaller than [v2]. *) let _ = assert ((Dd.var_of_level v1) < (Dd.var_of_level v2)) in let (_, vars1) = split_comb support v1 in let (vars2, _) = split_comb support v2 in Util.list_intersec vars1 vars2 let (get_remaining_vars: var -> Bdd.t -> var list) = fun v support -> (* Returns the list of variables greater than [v]. *) let (_, vars) = split_comb support v in vars `````` Erwan Jahier committed Mar 17, 2010 112 113 ``````(****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 114 115 116 117 118 119 120 121 ``````type sol_nb_table = (Bdd.t, sol_nb * sol_nb) Hashtbl.t (* ** Associates to a bdd its number of solutions in its lhs (then) and ** rhs (else) branches. *) let zero_sol = (0.0, 1) `````` Erwan Jahier committed Mar 17, 2010 122 123 124 `````` (* XXX La refaire en parcourant le peigne en parallele comme j'ai fait pour le tirage. *) `````` Erwan Jahier committed Mar 17, 2010 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 ``````let rec (build_sol_nb_table: Bdd.t -> sol_nb_table -> Bdd.t -> sol_nb * sol_nb) = fun bdd snt support -> (** Returns the number of solutions of [bdd] and the ones of its negation. Also udpadtes the solution number table [snt] for for [bdd] and its negation, and recursively for all its sub-bdd. *) if Bdd.is_cst bdd then if (Bdd.is_true bdd) then ((1.0, 0), zero_sol) else (zero_sol, (1.0, 0)) else let var = Bdd.topvar bdd and bddt = (Bdd.dthen bdd) and bdde = (Bdd.delse bdd) in let ((a, n), (not_a, not_n)) = build_sol_nb_table bddt snt support in let ((b, m), (not_b, not_m)) = build_sol_nb_table bdde snt support in (* [n] and [m] correspond to the relative number of solutions in the then and else branches. We need to multiply this relative number of solutions by 2 to the power of the number of missing variables (the unconstraint ones) between the topvar of the current bdd and the one of its respective child. Ditto for the negation of [bdd]. *) let nt = if Bdd.is_cst bddt then List.length (get_remaining_vars var support) else List.length (get_vars_between var (Bdd.topvar bddt) support) and ne = if Bdd.is_cst bdde then List.length (get_remaining_vars var support) else List.length (get_vars_between var (Bdd.topvar bdde) support) in let n1 = n + nt and m1 = m + ne and not_n1 = not_n + nt and not_m1 = not_m + ne in let sol_nb = add_sol_nb (a,n1) (b,m1) and not_sol_nb = add_sol_nb (not_a, not_n1) (not_b, not_m1) in let _ = (Bdd.dnot bdd) in Hashtbl.add snt bdd ((a, n1), (b, m1)); Hashtbl.add snt (Bdd.dnot bdd) ((not_b, not_m1), (not_a, not_n1)); (sol_nb, not_sol_nb) (****************************************************************************) let (formula_list_to_conj: formula list -> formula) = `````` Erwan Jahier committed Mar 17, 2010 179 `````` fun fl -> `````` Erwan Jahier committed Mar 17, 2010 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 `````` (** Transform a (non-empty) list of formula to the conjunction made of those formula. *) match fl with [] -> assert false | f::[] -> f | f1::f2::tail -> List.fold_left (fun x y -> And(x, y)) (And(f1, f2)) tail let rec (formula_to_bdd : formula -> Bdd.t) = fun f -> (** Transform the formula [f] into a bdd. Also tabulates the result in the [bdd_tbl] field of [env_state] because the translation is very expensive. *) (* XXX Should I rather store only toplevel formula in this table ??? (which would simply require to remove the following 4 lines, because is_satiafiable already performs the check) ==> I should time profile both! *) if Hashtbl.mem env_state.bdd_tbl f then Hashtbl.find env_state.bdd_tbl f else let bdd = match f with Not(f) -> Bdd.dnot (formula_to_bdd f) | Or(f1, f2) -> Bdd.dor (formula_to_bdd f1) (formula_to_bdd f2) | And(f1, f2) -> Bdd.dand (formula_to_bdd f1) (formula_to_bdd f2) | True -> Bdd.dtrue () | False -> Bdd.dfalse () | Bvar(vn) -> Bdd.var (Env_state.vn_to_index vn) | Eq(e1, e2) -> assert false (* XXX FIX US !!! *) | Ge(e1, e2) -> assert false (* XXX FIX US !!! *) | G(e1, e2) -> assert false (* XXX FIX US !!! *) in let _ = match f with Not(nf) -> Hashtbl.add env_state.bdd_tbl nf (Bdd.dnot bdd) | _ -> Hashtbl.add env_state.bdd_tbl (Not(f)) (Bdd.dnot bdd) in Hashtbl.add env_state.bdd_tbl f bdd; bdd (****************************************************************************) (****************************************************************************) let (toss_up_one_var: var -> var * bool) = fun var -> let ran = Random.float 1. in if (ran < 0.5) then (var, true) else (var, false) `````` Erwan Jahier committed Mar 17, 2010 235 236 `````` `````` Erwan Jahier committed Mar 17, 2010 237 238 239 240 241 242 ``````let rec (draw_in_bdd: Bdd.t -> sol_nb_table -> Bdd.t -> (var * bool) list) = fun bdd snt support -> (** Returns a draw of the variables from the topvar of [bdd] to the end (according to the ordering of the support). *) let _ = assert (not (Bdd.is_cst bdd)) in `````` Erwan Jahier committed Mar 17, 2010 243 244 245 246 `````` let bddvar = Bdd.topvar bdd in let suppvar = Bdd.topvar support in if bddvar = suppvar `````` Erwan Jahier committed Mar 17, 2010 247 `````` then `````` Erwan Jahier committed Mar 17, 2010 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 `````` let ((a, n), (b, m)) = Hashtbl.find snt bdd in let t = a +. b *. 2.**(float_of_int (m-n)) in let (bool, newbdd) = (* we draw [true] with the probability [a / a + b * 2**(m-n)]. *) if (b = 0.) then (true, (Bdd.dthen bdd)) else if (a = 0.) || (t = infinity) then (false, (Bdd.delse bdd)) else let ran = Random.float 1. in if ran < (a /. t) then (true, (Bdd.dthen bdd)) else (false, (Bdd.delse bdd)) in if Bdd.is_cst newbdd then if Bdd.is_false newbdd then assert false (* a branch with no solution should not have been drawn ! *) else (* Bdd.is_true newbdd; we toss up constraint vars *) (bddvar, bool)::(List.map toss_up_one_var (Bdd.int_of_support (Bdd.dthen support))) else (* bddnew is not a constant *) (bddvar, bool)::(draw_in_bdd newbdd snt (Bdd.dthen support)) `````` Erwan Jahier committed Mar 17, 2010 270 `````` else `````` Erwan Jahier committed Mar 17, 2010 271 `````` (* bddvar <> suppvar *) `````` Erwan Jahier committed Mar 17, 2010 272 `````` (toss_up_one_var suppvar)::(draw_in_bdd bdd snt (Bdd.dthen support)) `````` Erwan Jahier committed Mar 17, 2010 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 `````` (****************************************************************************) (****************************************************************************) (* Exported *) let rec (is_satisfiable: formula list -> bool) = (* As a side effect, also updates the [bdd_tbl] field of [env_state] with the bbd of [fl] (so that the expensive formula to bdd transcrition can be reused in [solve_formula]). *) fun fl -> let f = formula_list_to_conj fl in let bdd = if Hashtbl.mem env_state.bdd_tbl f then Hashtbl.find env_state.bdd_tbl f else let bdd0 = formula_to_bdd f in Hashtbl.add env_state.bdd_tbl f bdd0 ; bdd0 in not (Bdd.is_false bdd) `````` Erwan Jahier committed Mar 17, 2010 298 `````` `````` Erwan Jahier committed Mar 17, 2010 299 300 301 `````` (* Exported *) let (solve_formula: int -> formula list -> var_name list -> (subst list * subst list) list) = `````` Erwan Jahier committed Mar 17, 2010 302 `````` fun p fl vars_to_gen -> `````` Erwan Jahier committed Mar 17, 2010 303 304 305 306 `````` let support = List.fold_left (fun acc vn -> (Bdd.dand (Bdd.var (vn_to_index vn)) acc)) (Bdd.dtrue ()) `````` Erwan Jahier committed Mar 17, 2010 307 `````` vars_to_gen `````` Erwan Jahier committed Mar 17, 2010 308 309 310 311 312 `````` in let (draw_and_split : Bdd.t * sol_nb_table -> subst list * subst list) = fun (bdd, snt) -> (* Draw values in the bdd *) let var_index_bool_l = draw_in_bdd bdd snt support in `````` Erwan Jahier committed Mar 17, 2010 313 314 315 316 317 318 319 320 321 322 323 324 325 `````` let subst_l = List.map (fun (i, b) -> (* Replace the indexes by the corresponding var names, and booleans by atomic_expr. *) ((Env_state.index_to_vn i), Formula.Bool(b))) var_index_bool_l in let _ = assert ( (* Checks that the generated variables are indeed the ones that should have been generated... *) let (gen_vars, _) = split subst_l in (sort (compare) gen_vars) = (sort (compare) vars_to_gen) ) `````` Erwan Jahier committed Mar 17, 2010 326 `````` in `````` Erwan Jahier committed Mar 17, 2010 327 328 `````` let (out_vars, _) = List.split (Env_state.out_env_unsorted ()) in (* Splits output and local vars. *) `````` Erwan Jahier committed Mar 17, 2010 329 330 331 332 333 `````` List.partition (fun (vn, _) -> List.mem vn out_vars) subst_l in let f = formula_list_to_conj fl in let bdd = Hashtbl.find env_state.bdd_tbl f in let snt = (Hashtbl.create 1) in `````` Erwan Jahier committed Mar 17, 2010 334 `````` let _ = build_sol_nb_table bdd snt support in `````` Erwan Jahier committed Mar 17, 2010 335 336 `````` Util.unfold (draw_and_split) (bdd, snt) p ``````