1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Linear Programs for Fejes Toth's Full Contact Conjecture *)
5 (* Chapter: Further Results *)
6 (* Author: Thomas C. Hales *)
8 (* Guid: JKJNYAA (flypaper reference) *)
9 (* ========================================================================== *)
12 needs new mktop on platforms that do not support dynamic loading of Str.
14 ocamlmktop unix.cma nums.cma str.cma -o ocampl
17 glpk needs to be installed, and glpsol needs to be found in the path.
22 #directory "/Users/thomashales/Desktop/googlecode/flyspeck/glpk/";;
26 module Lipstick_ft = struct
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/";;
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 *)
41 (* type for holding the parameters for a linear program *)
46 mutable lpvalue : float option;
47 std_faces : int list list;
52 let (h,face1) = convert_to_list s in
59 let std_faces bb = bb.std_faces;;
61 let rec rangeA a i j = if (i >= j) then a
62 else rangeA ((j-1)::a) i (j-1);;
64 let upt = rangeA [] 0;;
67 let lw = List.length w in
68 let r j = List.nth w (j mod lw) in
70 [r i; r (i+1); r(i+2)] in
74 1+ maxlist0 (List.flatten (std_faces bb));;
76 let cface bb = List.length(std_faces bb);;
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));;
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
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
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;;
107 (* read in the hypermap archive as java style strings *)
110 let archive(raw) = strip_archive raw;;
113 (* 2013-01, added arch as an explicit argument *)
115 let bbn arch i = mk_bb (List.nth arch i);;
117 map (fun i -> solve_branch_f (!model) dumpfile "optival" ampl_of_bb (bbn arch i)) (0-- (List.length arch - 1));;
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"])]
126 First two HCP, FCC. Next five infeasible.
128 Last is ruled out by hexagons perimeter argument in text.
131 rerun on Sept 25, 2012.