projects_discrete_geom/fejestoth12/lipstick_ft.ml

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Linear Programs for Fejes Toth's Full Contact Conjecture *)
   5 (* Chapter: Further Results                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-05-19                                                           *)
   8 (* Guid: JKJNYAA (flypaper reference) *)
   9 (* ========================================================================== *)
  10
  11 (*
  12 needs new mktop on platforms that do not support dynamic loading of Str.
  13
  14 ocamlmktop unix.cma nums.cma str.cma -o ocampl
  15 ./ocampl
  16
  17 glpk needs to be installed, and glpsol needs to be found in the path.
  18
  19 *)
  20
  21 (*
  22 #directory "/Users/thomashales/Desktop/googlecode/flyspeck/glpk/";;
  23 #use  "glpk_link.ml";;
  24 *)
  25
  26 module Lipstick_ft = struct
  27
  28 open Glpk_link;;
  29
  30 (* external files. Edit for local system. *)
  31 (* let datapath = "/Users/thomashales/Desktop/googlecode/flyspeck/graph_generator/output/";; *)
  32 let datapath = "/tmp/";;
  33 let glpkpath = "/Users/thomashales/Desktop/googlecode/flyspeck/glpk/";;
  34
  35 (* let archiveraw = datapath ^ "fejesToth.txt";; (*read only *) *)
  36 let archiveraw = datapath ^ "graph_out.txt";; (*read only *)
  37 let model = ref (glpkpath^ "../projects_discrete_geom/fejestoth12/contact.mod");; (* read only *)
  38 let tmpfile = "/tmp/graph.dat";;  (* temporary output *)
  39 let dumpfile = "/tmp/graph.out";; (* temp output *)
  40
  41 (* type for holding the parameters for a linear program *)
  42
  43 type branchnbound =
  44   {
  45     hypermapid : string;
  46     mutable lpvalue : float option;
  47     std_faces : int list list;
  48     string_rep : string;
  49   };;
  50
  51 let mk_bb s =
  52   let (h,face1) = convert_to_list s in
  53  {hypermapid= h;
  54   lpvalue = None;
  55   string_rep=s;
  56   std_faces = face1;
  57  };;
  58
  59 let std_faces bb = bb.std_faces;;
  60
  61 let rec rangeA a i j  = if (i >= j) then a
  62    else rangeA ((j-1)::a) i (j-1);;
  63
  64 let upt =   rangeA [] 0;;
  65
  66 let triples w =
  67   let lw = List.length w in
  68   let r j = List.nth w (j mod lw)  in
  69   let triple i =
  70       [r i; r (i+1); r(i+2)] in
  71     map triple (upt lw);;
  72
  73 let cvertex bb =
  74   1+ maxlist0 (List.flatten (std_faces bb));;
  75
  76 let cface bb = List.length(std_faces bb);;
  77
  78 let std_face_of_size bb r=
  79   let f = std_faces bb in
  80   let z = enumerate f in
  81     fst(List.split (filter (function _,y -> List.length y=r) z));;
  82
  83 let ampl_of_bb outs bb =
  84   let fs = std_faces bb in
  85   let where3 = wheremod fs in
  86   let list_of = unsplit " " string_of_int in
  87   let edart_raw  =
  88     map triples fs in
  89   let edart =
  90     let edata_row (i,x) = (sprintf "(*,*,*,%d) " i)^(unsplit ", " list_of x) in
  91       unsplit "\n" edata_row (enumerate edart_raw) in
  92   let mk_dart xs = sprintf "%d %d" (hd xs) (where3 xs) in
  93   let mk_darts xs = (unsplit ", " mk_dart xs) in
  94   let p = sprintf in
  95   let j = join_lines [
  96     p"param hypermapID := %s;" bb.hypermapid ;
  97     p"param CFACE := %d;\n" (cface bb);
  98     p"set ITRIANGLE := %s;" (list_of (std_face_of_size bb 3)) ;
  99     p"set IQUAD := %s;" (list_of (std_face_of_size bb 4) );
 100     p"set IPENT := %s;" (list_of (std_face_of_size bb 5)) ;
 101     p"set IHEX := %s;\n" (list_of (std_face_of_size bb 6));
 102     p"set IHEPT := %s;\n" (list_of (std_face_of_size bb 7));
 103     p"set IOCT := %s;\n" (list_of (std_face_of_size bb 8));
 104     p"set EDART := \n%s;\n"  (edart);] in
 105     Printf.fprintf outs "%s" j;;
 106
 107 (* read in the hypermap archive as java style strings *)
 108
 109 (*
 110 let archive(raw) = strip_archive raw;;
 111 *)
 112
 113 (* 2013-01, added arch as an explicit argument *)
 114
 115 let bbn arch i = mk_bb (List.nth arch i);;
 116 let exec(arch) =
 117   map (fun i -> solve_branch_f (!model) dumpfile "optival" ampl_of_bb (bbn arch i)) (0-- (List.length arch - 1));;
 118
 119 (* - : string list list =
 120   [([], ["opt.val = 0"]); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []);
 121    ([], ["opt.val = 0"]); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []);
 122    (["PROBLEM HAS NO FEASIBLE SOLUTION"], []);
 123    (["PROBLEM HAS NO FEASIBLE SOLUTION"], []);
 124    (["PROBLEM HAS NO FEASIBLE SOLUTION"], []); ([], ["opt.val = 0"])]
 125
 126 First two HCP, FCC. Next five infeasible.
 127
 128 Last is ruled out by hexagons perimeter argument in text.
 129    We are done!
 130
 131 rerun on Sept 25, 2012.
 132 *)
 133
 134 end;;