+++ /dev/null
-(*\r
- Reductions from SAT and 3-colorability of graphs to separation\r
- of lambda-terms. Commented out the encoding from SAT.\r
-*)\r
-\r
-open Util;;\r
-\r
-(* type cnf = int list list;;\r
-\r
-let (++) f g x = f (g x);;\r
-\r
-let maxvar : cnf -> int =\r
- let aux f = List.fold_left (fun acc x -> max acc (f x)) 0 in\r
- aux (aux abs)\r
-;; *)\r
-\r
-type graph = (int * int) list;;\r
-type color = int;;\r
-\r
-let arc x y = min x y, max x y;;\r
-let mem g x y = List.mem (arc x y) g;;\r
-\r
-(* let reduction_sat_3col p =\r
- let triangle a0 a1 a2 = [arc a0 a1; arc a0 a2; arc a1 a2] in\r
- let init0 = triangle 0 1 2 in\r
- (* 0false; 1true; 2base*)\r
- let n = maxvar p in\r
- let init1 = Array.to_list (Array.mapi (fun i () -> triangle (2*i+1) (2*(i+1)) 2) (Array.make n ())) in\r
- let freshno = ref (2 * n + 3) in\r
- let mk_triangle () =\r
- let i = !freshno in\r
- freshno := i+3; i, i+1, i+2 in\r
- let rec translate = function\r
- | [] -> assert false\r
- | x::[] -> [triangle 0 2 x]\r
- | x::y::l ->\r
- let a,b,c = mk_triangle () in\r
- triangle a b c :: [arc x a; arc y b] :: translate (c::l) in\r
- let p = List.map (List.map (fun x ->\r
- if x = 0 then assert false\r
- else if x < 0 then 2 * (abs x + 1)\r
- else 2 * x + 1\r
- )) p in\r
- let init2 = List.map (List.concat ++ translate) p in\r
- !freshno, init0 @ List.concat (init1 @ init2)\r
-;;\r
-\r
-let string_of_graph g =\r
- String.concat " " (List.map (fun (x,y) -> string_of_int x ^ "<>" ^ string_of_int y) g)\r
-;; *)\r
-\r
-(* let main p =\r
- let mv = maxvar p in\r
- prerr_endline (string_of_int mv);\r
- let _, g = reduction_sat_3col p in\r
- prerr_endline (string_of_graph g);\r
- generate ;;\r
-\r
-prerr_endline (main[\r
- [1; -2; 3];\r
- [2; 4; -5]\r
-]);; *)\r
-\r
-let p_ = "BOMB ";;\r
-let x_ = "x ";;\r
-(* y, z dummies *)\r
-let y_ = "y ";;\r
-let z_ = "z ";;\r
-(* a, b endline separators *)\r
-let a_ = "a ";;\r
-let b_ = "b ";;\r
-\r
-let generate g n max =\r
- (* 0 <= n <= max+1 *)\r
- let three f sep =\r
- String.concat sep (List.map f [0;1;2]) in\r
- let rec aux' n m color =\r
- if m = -1 then x_\r
- else aux' n (m-1) color ^\r
- if n = m then\r
- (if List.mem (n,n) g then p_^p_^p_ (* cappio nel grafo *)\r
- else three (fun c -> if color = c then y_ else p_) "")\r
- else if n < m then y_^y_^y_\r
- else if List.mem (m,n) g then\r
- three (fun c -> if color = c then p_ else y_) ""\r
- else y_^y_^y_ in\r
- let rec aux m =\r
- if m = -1 then x_\r
- else aux (m-1) ^\r
- if n < m then p_^p_^p_\r
- else if n = m then\r
- "(_." ^ three (aux' n max) "b) (_." ^ "b) "\r
- else y_^y_^y_\r
- in aux max ^ a_\r
-;;\r
-\r
-let generate2 g n max =\r
- let rec aux m =\r
- if m = -1 then x_\r
- else aux (m-1) ^\r
- if n < m then p_^p_^p_\r
- else if n = m\r
- then z_^z_^z_\r
- else y_^y_^y_\r
- in aux max ^ p_\r
-;;\r
-\r
-\r
-let encode_graph g =\r
- let g = List.map (fun (x,y) -> min x y, max x y) g in\r
- let mapi f a = Array.to_list (Array.mapi f a) in\r
- let nodex_no =\r
- List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 in\r
- String.concat "\n" ("\n$ problem from 3-colorability" ::\r
- let no = nodex_no g in\r
- mapi (fun i () ->\r
- (if i = no+1 then "D " else "C ") ^ generate g i no\r
- ) (Array.make (no+2) ()) @\r
- mapi (fun i () ->\r
- "C " ^ generate2 g i no\r
- ) (Array.make (no+1) ());\r
- )\r
-;;\r
-\r
-print_endline "Three example encodings:";;\r
-\r
-(* easy one *)\r
-prerr_endline (encode_graph [0,1;]);;\r
-\r
-(* two imopssible problems *)\r
-prerr_endline (\r
- encode_graph [0,1; 1,1]\r
-);;\r
-prerr_endline (\r
- encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3]\r
-);;\r
-\r
-(******************************************************************************)\r
-\r
-print_endline "\nIt will now run some problems and decode the solutions";;\r
-print_endline "Press ENTER to continue.";;\r
-let _ = read_line ();;\r
-\r
-let strip_lambda_matches =\r
- let getvar = function\r
- | `Var(n,_) -> n\r
- | _ -> assert false in\r
- let rec aux n = function\r
- | `Lam(_,t) -> aux (n+1) t\r
- | `Match(_,_,_,bs,_) -> Some (n, List.map (getvar ++ snd) !bs)\r
- | _ -> None\r
- in aux 0\r
-;;\r
-\r
-let next_candidates sigma cands =\r
- let sigma = Util.filter_map\r
- (fun x -> try Some (List.assoc x sigma) with Not_found -> None) cands in\r
- match Util.find_opt strip_lambda_matches sigma with\r
- | None -> -1, []\r
- | Some x -> x\r
-;;\r
-\r
-let fix_numbers l =\r
- let rec aux n = function\r
- | [] -> []\r
- | x::xs -> (x - 2*n - 1) :: (aux (n+1) xs)\r
- in aux 0 l\r
-;;\r
-\r
-let color (g:graph) =\r
- let p = encode_graph g in\r
- let (_, _, _, _, vars as p) = Parser.problem_of_string p in\r
- let _, result = Lambda4.solve (Lambda4.problem_of p) in\r
- match result with\r
- | `Unseparable _ -> prerr_endline "Graph not colorable"; None\r
- | `Separable sigma -> (\r
- (* start from variable x *)\r
- let x = Util.index_of "x" vars in\r
- (* List.iter (fun x -> prerr_endline (string_of_int (fst x) ^ ":" ^ Num.print ~l:vars (snd x))) sigma; *)\r
- let rec iter f x =\r
- let n, x = f x in if x = [] then [] else n :: iter f x in\r
- let numbers = iter (next_candidates sigma) [x] in\r
- let numbers = fix_numbers numbers in\r
- (* display solution *)\r
- let colors = ["r"; "g"; "b"] in\r
- prerr_endline ("\nSolution found:\n " ^ String.concat "\n "\r
- (List.mapi (fun i x ->\r
- string_of_int i ^ " := " ^ List.nth colors x) numbers));\r
- assert (List.for_all (fun (a,b) -> List.nth numbers a <> List.nth numbers b) g);\r
- Some numbers)\r
-;;\r
-\r
-let bruteforce g =\r
- let nodes_no = 1+\r
- List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 g in\r
- let check x = if List.for_all (fun (a,b) -> List.nth x a <> List.nth x b) g\r
- then failwith "bruteforce: sat" in\r
- let rec guess l = prerr_string "+";\r
- if List.length l = nodes_no\r
- then check l\r
- else (guess (0::l); guess (1::l); guess (2::l)) in\r
- guess [];\r
- prerr_endline "bruteforce: unsat"\r
-;;\r
-\r
-assert (color [0,1;0,2;1,2;2,3;3,0] <> None);;\r
-assert (color [0,1;0,2;1,2;2,3;3,0;0,4;4,2] <> None);;\r
-\r
-(* assert (color [\r
- 1,2; 1,4; 1,7; 1,9; 2,3; 2,6; 2,8; 3,5;\r
- 3,7; 3,0; 4,5; 4,6; 4,0; 5,8; 5,9; 6,11;\r
- 7,11; 8,11; 9,11; 0,11;\r
-] = None);; *)\r
-\r
-(* https://turing.cs.hbg.psu.edu/txn131/file_instances/coloring/graph_color/queen5_5.col *)\r
-color [1,7\r
-; 1,13\r
-; 1,19\r
-; 1,25\r
-; 1,2\r
-; 1,3\r
-; 1,4\r
-; 1,5\r
-; 1,6\r
-; 1,11\r
-; 1,16\r
-; 1,21\r
-; 2,8\r
-; 2,14\r
-; 2,20\r
-; 2,6\r
-; 2,3\r
-; 2,4\r
-; 2,5\r
-; 2,7\r
-; 2,12\r
-; 2,17\r
-; 2,22\r
-; 2,1\r
-; 3,9\r
-; 3,15\r
-; 3,7\r
-; 3,11\r
-; 3,4\r
-; 3,5\r
-; 3,8\r
-; 3,13\r
-; 3,18\r
-; 3,23\r
-; 3,2\r
-; 3,1\r
-; 4,10\r
-; 4,8\r
-; 4,12\r
-; 4,16\r
-; 4,5\r
-; 4,9\r
-; 4,14\r
-; 4,19\r
-; 4,24\r
-; 4,3\r
-; 4,2\r
-; 4,1\r
-; 5,9\r
-; 5,13\r
-; 5,17\r
-; 5,21\r
-; 5,10\r
-; 5,15\r
-; 5,20\r
-; 5,25\r
-; 5,4\r
-; 5,3\r
-; 5,2\r
-; 5,1\r
-; 6,12\r
-; 6,18\r
-; 6,24\r
-; 6,7\r
-; 6,8\r
-; 6,9\r
-; 6,10\r
-; 6,11\r
-; 6,16\r
-; 6,21\r
-; 6,2\r
-; 6,1\r
-; 7,13\r
-; 7,19\r
-; 7,25\r
-; 7,11\r
-; 7,8\r
-; 7,9\r
-; 7,10\r
-; 7,12\r
-; 7,17\r
-; 7,22\r
-; 7,6\r
-; 7,3\r
-; 7,2\r
-; 7,1\r
-; 8,14\r
-; 8,20\r
-; 8,12\r
-; 8,16\r
-; 8,9\r
-; 8,10\r
-; 8,13\r
-; 8,18\r
-; 8,23\r
-; 8,7\r
-; 8,6\r
-; 8,4\r
-; 8,3\r
-; 8,2\r
-; 9,15\r
-; 9,13\r
-; 9,17\r
-; 9,21\r
-; 9,10\r
-; 9,14\r
-; 9,19\r
-; 9,24\r
-; 9,8\r
-; 9,7\r
-; 9,6\r
-; 9,5\r
-; 9,4\r
-; 9,3\r
-; 10,14\r
-; 10,18\r
-; 10,22\r
-; 10,15\r
-; 10,20\r
-; 10,25\r
-; 10,9\r
-; 10,8\r
-; 10,7\r
-; 10,6\r
-; 10,5\r
-; 10,4\r
-; 11,17\r
-; 11,23\r
-; 11,12\r
-; 11,13\r
-; 11,14\r
-; 11,15\r
-; 11,16\r
-; 11,21\r
-; 11,7\r
-; 11,6\r
-; 11,3\r
-; 11,1\r
-; 12,18\r
-; 12,24\r
-; 12,16\r
-; 12,13\r
-; 12,14\r
-; 12,15\r
-; 12,17\r
-; 12,22\r
-; 12,11\r
-; 12,8\r
-; 12,7\r
-; 12,6\r
-; 12,4\r
-; 12,2\r
-; 13,19\r
-; 13,25\r
-; 13,17\r
-; 13,21\r
-; 13,14\r
-; 13,15\r
-; 13,18\r
-; 13,23\r
-; 13,12\r
-; 13,11\r
-; 13,9\r
-; 13,8\r
-; 13,7\r
-; 13,5\r
-; 13,3\r
-; 13,1\r
-; 14,20\r
-; 14,18\r
-; 14,22\r
-; 14,15\r
-; 14,19\r
-; 14,24\r
-; 14,13\r
-; 14,12\r
-; 14,11\r
-; 14,10\r
-; 14,9\r
-; 14,8\r
-; 14,4\r
-; 14,2\r
-; 15,19\r
-; 15,23\r
-; 15,20\r
-; 15,25\r
-; 15,14\r
-; 15,13\r
-; 15,12\r
-; 15,11\r
-; 15,10\r
-; 15,9\r
-; 15,5\r
-; 15,3\r
-; 16,22\r
-; 16,17\r
-; 16,18\r
-; 16,19\r
-; 16,20\r
-; 16,21\r
-; 16,12\r
-; 16,11\r
-; 16,8\r
-; 16,6\r
-; 16,4\r
-; 16,1\r
-; 17,23\r
-; 17,21\r
-; 17,18\r
-; 17,19\r
-; 17,20\r
-; 17,22\r
-; 17,16\r
-; 17,13\r
-; 17,12\r
-; 17,11\r
-; 17,9\r
-; 17,7\r
-; 17,5\r
-; 17,2\r
-; 18,24\r
-; 18,22\r
-; 18,19\r
-; 18,20\r
-; 18,23\r
-; 18,17\r
-; 18,16\r
-; 18,14\r
-; 18,13\r
-; 18,12\r
-; 18,10\r
-; 18,8\r
-; 18,6\r
-; 18,3\r
-; 19,25\r
-; 19,23\r
-; 19,20\r
-; 19,24\r
-; 19,18\r
-; 19,17\r
-; 19,16\r
-; 19,15\r
-; 19,14\r
-; 19,13\r
-; 19,9\r
-; 19,7\r
-; 19,4\r
-; 19,1\r
-; 20,24\r
-; 20,25\r
-; 20,19\r
-; 20,18\r
-; 20,17\r
-; 20,16\r
-; 20,15\r
-; 20,14\r
-; 20,10\r
-; 20,8\r
-; 20,5\r
-; 20,2\r
-; 21,22\r
-; 21,23\r
-; 21,24\r
-; 21,25\r
-; 21,17\r
-; 21,16\r
-; 21,13\r
-; 21,11\r
-; 21,9\r
-; 21,6\r
-; 21,5\r
-; 21,1\r
-; 22,23\r
-; 22,24\r
-; 22,25\r
-; 22,21\r
-; 22,18\r
-; 22,17\r
-; 22,16\r
-; 22,14\r
-; 22,12\r
-; 22,10\r
-; 22,7\r
-; 22,2\r
-; 23,24\r
-; 23,25\r
-; 23,22\r
-; 23,21\r
-; 23,19\r
-; 23,18\r
-; 23,17\r
-; 23,15\r
-; 23,13\r
-; 23,11\r
-; 23,8\r
-; 23,3\r
-; 24,25\r
-; 24,23\r
-; 24,22\r
-; 24,21\r
-; 24,20\r
-; 24,19\r
-; 24,18\r
-; 24,14\r
-; 24,12\r
-; 24,9\r
-; 24,6\r
-; 24,4\r
-; 25,24\r
-; 25,23\r
-; 25,22\r
-; 25,21\r
-; 25,20\r
-; 25,19\r
-; 25,15\r
-; 25,13\r
-; 25,10\r
-; 25,7\r
-; 25,5\r
-; 25,1];;\r
projects / fireball-separation.git / blobdiff