glpk/minorlp/tame_table.ml

   1 (* ========================================================================== *)
   2 (* FLYSPECK - GLPK                                              *)
   3 (*                                                                            *)
   4 (* Linear Programming, AMPL format (non-formal)    *)
   5 (* Chapter:Tame Hypermap                          *)
   6 (* Lemma: KCBLRQC (Tame Table B) *)
   7 (* Author: Thomas C. Hales                                                    *)
   8 (* Date: 2010-06-14                            *)
   9 (* ========================================================================== *)
  10
  11 (*
  12
  13 The model considers nodes of type (p,q,0) and computes
  14 the constants b(p,q).
  15
  16 It also computes the constant a(5,0,1).
  17
  18 *)
  19
  20 flyspeck_needs "strictbuild.hl";;
  21 flyspeck_needs "../glpk/glpk_link.ml";;
  22 flyspeck_needs "../graph_generator/graph_control.hl";;
  23
  24 module Tame_table = struct
  25
  26   let squander_target = Graph_control.flyspeck_properties.Graph_control.squander_target;;
  27   let table_weight_d = Graph_control.flyspeck_properties.Graph_control.table_weight_d;;
  28   let table_weight_a = Graph_control.flyspeck_properties.Graph_control.table_weight_a;;
  29   let table_weight_b = Graph_control.flyspeck_properties.Graph_control.table_weight_b;;
  30   let node_card_max_at_exceptional_vertex = Graph_control.flyspeck_properties.Graph_control.node_card_max_at_exceptional_vertex;;
  31   let fl x = float_of_int x /. 10000.0;;
  32
  33 type lptype = Lp_unset
  34               | Lp_infeasible
  35               | Lp_value of float;;
  36
  37 let string_of_lptype t = match t with
  38     | Lp_infeasible -> "infeasible"
  39     | Lp_unset -> "unset"
  40     | Lp_value u -> Printf.sprintf "%3.3f" u;;
  41
  42 let rec cart b c = match b with
  43    [] -> []
  44   |b::bs -> (map (fun t -> (b,t)) c) @ cart bs c;;
  45
  46
  47 open Str;;
  48 open List;;
  49 open Glpk_link;;
  50
  51 let sprintf = Printf.sprintf;;
  52
  53 let glpk_dir = flyspeck_dir ^ "/../glpk";;
  54
  55 (* external files *)
  56 let model = glpk_dir^ "/minorlp/tame_table.mod";;
  57 let tmpfile = "/tmp/tame_table.dat";;
  58 let dumpfile = "/tmp/tmp.out";;
  59
  60 type node_type =
  61   {
  62     mutable lpvalue : lptype;
  63     p : int;
  64     q : int;
  65     r : int;
  66   };;
  67
  68 (* the initial configuration always has a quarter at 0 *)
  69 let mk_node p q r =
  70  {
  71   p = p;
  72   q = q;
  73   r = r;
  74   lpvalue = Lp_unset
  75  };;
  76
  77 let string_of_node t =
  78   Printf.sprintf "%d %d %d %s" t.p t.q t.r (string_of_lptype t.lpvalue);;
  79
  80 let ampl_of_nt outs nt =
  81   let pr = sprintf in
  82   let j = join_lines [
  83     pr"param p := %d;" nt.p;
  84     pr"param q := %d;" nt.q;
  85     pr"param r := %d;\n" nt.r;
  86    ] in
  87     Printf.fprintf outs "%s" j;;
  88
  89 let test() =
  90   let nt = mk_node 3 3 0 in
  91     display_ampl tmpfile ampl_of_nt nt;;
  92
  93 (* running of branch in glpsol *)
  94
  95 let set_lpvalue nt (f,r) = (* side effects *)
  96   let _ =
  97     if (List.length f > 0) then nt.lpvalue <- Lp_infeasible
  98     else if (List.length r = 1) then nt.lpvalue <- Lp_value  (float_of_string(hd r))
  99     else nt.lpvalue <- Lp_unset in
 100     nt;;
 101
 102 let init_lpvalue nt =
 103   let _ = match nt.lpvalue with
 104   | Lp_unset -> (set_lpvalue nt (solve_branch_f model dumpfile "tausum" ampl_of_nt nt))
 105   |  _ -> nt in
 106   let _ = report (string_of_node nt) in
 107     nt;;
 108
 109 (* display_ampl tmpfile ampl_of_nt (mk_node 5 0 0);; *)
 110
 111 let fpqr ((p,q),r) = init_lpvalue (mk_node p q r);;
 112
 113 let fpq (p,q) = fpqr((p,q),0);;
 114
 115 (* solve_branch_f model dumpfile "tausum" ampl_of_nt (mk_node 3 4 0);; *)
 116
 117 (* Each exception region contributes at least tame_table_d_5 *)
 118
 119 let filter1 =
 120   let target_ub = 1.542 in
 121   let _ = target_ub > fl squander_target or failwith "bad target value" in
 122   let tame_table_d_5 = 0.4818 in
 123   let _ = tame_table_d_5 < fl (List.nth table_weight_d 5) or failwith "bad d5 value" in
 124   filter (fun t -> match t.lpvalue with
 125               Lp_infeasible -> false
 126             | Lp_unset -> true
 127             | Lp_value s -> (s +. float_of_int t.r *. tame_table_d_5 < target_ub));;
 128
 129 let graph_control_unfound_b (t:node_type  ) = match (t.lpvalue) with
 130   | Lp_value u ->
 131       (try (
 132          let eps = 1.0e-10 in (* allow roundoff error *)
 133          let (_,_,v) = List.find (fun (a,b,_) -> (a=t.p && b = t.q)) table_weight_b in
 134            u +. eps <= fl v
 135       )
 136       with Not_found -> true)
 137   | _ -> true
 138   ;;
 139
 140 let filter2 = filter graph_control_unfound_b;;
 141
 142 (* The case (p,q,r) = (0,2,0) is rejected by the convexity hypothesis. *)
 143 (* The case (p,q,r) = (5,0,0) is done with calculation 4652969746 *)
 144
 145 let known_exceptions (t:node_type) =
 146   not((t.p = 0 && t.q = 2 && t.r = 0) or (t.p = 5 && t.q = 0 && t.r = 0));;
 147
 148 let filter3 = filter known_exceptions;;
 149
 150 let tame_table_lp_data() = (map fpq (cart  (0--10) (0--10)));;
 151
 152 let tame_table_b_info() =
 153   let n = filter3 (filter2 (filter1 (tame_table_lp_data()))) in
 154     if (List.length n = 0) then "All b table values have been accounted for in informal lp tests (ignoring 0,2,0 and 5,0,0)"
 155     else "Unaccounted for b values: \n" ^ join_lines (map string_of_node n);;
 156
 157 (* If r >= 4, then the dihedral sum is greater than 2 Pi *)
 158
 159 let pqrvalues  =
 160   let a =  (cart (cart  (0--6)  (0--6)) (1--3)) in
 161   filter (fun ((p,q),r) -> (p+q+r=6)) a;;
 162
 163
 164 let badvalues_a (t:node_type) = match (t.lpvalue) with
 165   | Lp_value u ->
 166       (try (
 167          let eps = 1.0e-10 in (* allow roundoff error *)
 168          let (_,v) = List.find (fun (a,_) -> (a=t.p && (6-a) = t.q + t.r)) table_weight_a in
 169            u +. eps <= fl v
 170       )
 171       with Not_found -> true)
 172   | _ -> true
 173   ;;
 174
 175 let filter_a = filter badvalues_a;;
 176
 177 let tame_table_a_info() =
 178   let n =  filter_a (filter1 (map fpqr pqrvalues )) in
 179     if (List.length n = 0) then "All a table values have been accounted for in informal lp tests"
 180     else "Unaccounted for a values: \n" ^ join_lines (map string_of_node n);;
 181
 182 let execute() =
 183   let s =   join_lines [tame_table_b_info();tame_table_a_info()] in
 184   let _ =   report s in
 185     s;;
 186
 187
 188
 189 end;;