2 Reductions from SAT and 3-colorability of graphs to separation
\r
3 of lambda-terms. Commented out the encoding from SAT.
\r
6 (* type cnf = int list list;;
\r
8 let (++) f g x = f (g x);;
\r
10 let maxvar : cnf -> int =
\r
11 let aux f = List.fold_left (fun acc x -> max acc (f x)) 0 in
\r
15 type graph = (int * int) list;;
\r
17 let arc x y = min x y, max x y;;
\r
18 let mem g x y = List.mem (arc x y) g;;
\r
20 (* let reduction_sat_3col p =
\r
21 let triangle a0 a1 a2 = [arc a0 a1; arc a0 a2; arc a1 a2] in
\r
22 let init0 = triangle 0 1 2 in
\r
23 (* 0false; 1true; 2base*)
\r
25 let init1 = Array.to_list (Array.mapi (fun i () -> triangle (2*i+1) (2*(i+1)) 2) (Array.make n ())) in
\r
26 let freshno = ref (2 * n + 3) in
\r
27 let mk_triangle () =
\r
29 freshno := i+3; i, i+1, i+2 in
\r
30 let rec translate = function
\r
31 | [] -> assert false
\r
32 | x::[] -> [triangle 0 2 x]
\r
34 let a,b,c = mk_triangle () in
\r
35 triangle a b c :: [arc x a; arc y b] :: translate (c::l) in
\r
36 let p = List.map (List.map (fun x ->
\r
37 if x = 0 then assert false
\r
38 else if x < 0 then 2 * (abs x + 1)
\r
41 let init2 = List.map (List.concat ++ translate) p in
\r
42 !freshno, init0 @ List.concat (init1 @ init2)
\r
45 let string_of_graph g =
\r
46 String.concat " " (List.map (fun (x,y) -> string_of_int x ^ "<>" ^ string_of_int y) g)
\r
50 let mv = maxvar p in
\r
51 prerr_endline (string_of_int mv);
\r
52 let _, g = reduction_sat_3col p in
\r
53 prerr_endline (string_of_graph g);
\r
56 prerr_endline (main[
\r
66 (* a, b endline separators *)
\r
70 let generate g n max =
\r
71 (* 0 <= n <= max+1 *)
\r
73 String.concat sep (List.map f [0;1;2]) in
\r
74 let rec aux' n m color =
\r
76 else aux' n (m-1) color ^
\r
78 (if List.mem (n,n) g then p_^p_^p_ (* cappio nel grafo *)
\r
79 else three (fun c -> if color = c then y_ else p_) "")
\r
80 else if n < m then y_^y_^y_
\r
81 else if List.mem (m,n) g then
\r
82 three (fun c -> if color = c then p_ else y_) ""
\r
87 if n < m then p_^p_^p_
\r
89 "(_." ^ three (aux' n max) "b) (_." ^ "b) "
\r
94 let generate2 g n max =
\r
98 if n < m then p_^p_^p_
\r
106 let encode_graph g =
\r
107 let g = List.map (fun (x,y) -> min x y, max x y) g in
\r
108 let mapi f a = Array.to_list (Array.mapi f a) in
\r
110 List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 in
\r
111 String.concat "\n" ("\n$ problem from 3-colorability" ::
\r
112 let no = nodex_no g in
\r
114 (if i = no+1 then "D " else "C ") ^ generate g i no
\r
115 ) (Array.make (no+2) ()) @
\r
117 "C " ^ generate2 g i no
\r
118 ) (Array.make (no+1) ());
\r
123 prerr_endline (encode_graph [0,1;]);;
\r
125 (* two imopssible problems *)
\r
127 encode_graph [0,1; 1,1]
\r
130 encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3]
\r