(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Linear Programs for Fejes Toth's Full Contact Conjecture *) (* Chapter: Further Results *) (* Author: Thomas C. Hales *) (* Date: 2010-05-19 *) (* Guid: JKJNYAA (flypaper reference) *) (* ========================================================================== *) (* needs new mktop on platforms that do not support dynamic loading of Str. ocamlmktop unix.cma nums.cma str.cma -o ocampl ./ocampl glpk needs to be installed, and glpsol needs to be found in the path. *) (* #directory "/Users/thomashales/Desktop/googlecode/flyspeck/glpk/";; #use "glpk_link.ml";; *) module Lipstick_ft = struct open Glpk_link;; (* external files. Edit for local system. *) (* let datapath = "/Users/thomashales/Desktop/googlecode/flyspeck/graph_generator/output/";; *) let datapath = "/tmp/";; let glpkpath = "/Users/thomashales/Desktop/googlecode/flyspeck/glpk/";; (* let archiveraw = datapath ^ "fejesToth.txt";; (*read only *) *) let archiveraw = datapath ^ "graph_out.txt";; (*read only *) let model = ref (glpkpath^ "../projects_discrete_geom/fejestoth12/contact.mod");; (* read only *) let tmpfile = "/tmp/graph.dat";; (* temporary output *) let dumpfile = "/tmp/graph.out";; (* temp output *) (* type for holding the parameters for a linear program *) type branchnbound = { hypermapid : string; mutable lpvalue : float option; std_faces : int list list; string_rep : string; };; let mk_bb s = let (h,face1) = convert_to_list s in {hypermapid= h; lpvalue = None; string_rep=s; std_faces = face1; };; let std_faces bb = bb.std_faces;; let rec rangeA a i j = if (i >= j) then a else rangeA ((j-1)::a) i (j-1);; let upt = rangeA [] 0;; let triples w = let lw = List.length w in let r j = List.nth w (j mod lw) in let triple i = [r i; r (i+1); r(i+2)] in map triple (upt lw);; let cvertex bb = 1+ maxlist0 (List.flatten (std_faces bb));; let cface bb = List.length(std_faces bb);; let std_face_of_size bb r= let f = std_faces bb in let z = enumerate f in fst(List.split (filter (function _,y -> List.length y=r) z));; let ampl_of_bb outs bb = let fs = std_faces bb in let where3 = wheremod fs in let list_of = unsplit " " string_of_int in let edart_raw = map triples fs in let edart = let edata_row (i,x) = (sprintf "(*,*,*,%d) " i)^(unsplit ", " list_of x) in unsplit "\n" edata_row (enumerate edart_raw) in let mk_dart xs = sprintf "%d %d" (hd xs) (where3 xs) in let mk_darts xs = (unsplit ", " mk_dart xs) in let p = sprintf in let j = join_lines [ p"param hypermapID := %s;" bb.hypermapid ; p"param CFACE := %d;\n" (cface bb); p"set ITRIANGLE := %s;" (list_of (std_face_of_size bb 3)) ; p"set IQUAD := %s;" (list_of (std_face_of_size bb 4) ); p"set IPENT := %s;" (list_of (std_face_of_size bb 5)) ; p"set IHEX := %s;\n" (list_of (std_face_of_size bb 6)); p"set IHEPT := %s;\n" (list_of (std_face_of_size bb 7)); p"set IOCT := %s;\n" (list_of (std_face_of_size bb 8)); p"set EDART := \n%s;\n" (edart);] in Printf.fprintf outs "%s" j;; (* read in the hypermap archive as java style strings *) (* let archive(raw) = strip_archive raw;; *) (* 2013-01, added arch as an explicit argument *) let bbn arch i = mk_bb (List.nth arch i);; let exec(arch) = map (fun i -> solve_branch_f (!model) dumpfile "optival" ampl_of_bb (bbn arch i)) (0-- (List.length arch - 1));; (* - : string list list = [([], ["opt.val = 0"]); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []); ([], ["opt.val = 0"]); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []); (["PROBLEM HAS NO FEASIBLE SOLUTION"], []); ([], ["opt.val = 0"])] First two HCP, FCC. Next five infeasible. Last is ruled out by hexagons perimeter argument in text. We are done! rerun on Sept 25, 2012. *) end;;