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
\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
;;\r
\r
+print_endline "Three example encodings:";;\r
+\r
(* easy one *)\r
prerr_endline (encode_graph [0,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 / commitdiff