2 Reductions from SAT and 3-colorability of graphs to separation
\r
3 of lambda-terms. Commented out the encoding from SAT.
\r
8 (* type cnf = int list list;;
\r
10 let (++) f g x = f (g x);;
\r
12 let maxvar : cnf -> int =
\r
13 let aux f = List.fold_left (fun acc x -> max acc (f x)) 0 in
\r
17 type graph = (int * int) list;;
\r
20 let arc x y = min x y, max x y;;
\r
21 let mem g x y = List.mem (arc x y) g;;
\r
23 (* let reduction_sat_3col p =
\r
24 let triangle a0 a1 a2 = [arc a0 a1; arc a0 a2; arc a1 a2] in
\r
25 let init0 = triangle 0 1 2 in
\r
26 (* 0false; 1true; 2base*)
\r
28 let init1 = Array.to_list (Array.mapi (fun i () -> triangle (2*i+1) (2*(i+1)) 2) (Array.make n ())) in
\r
29 let freshno = ref (2 * n + 3) in
\r
30 let mk_triangle () =
\r
32 freshno := i+3; i, i+1, i+2 in
\r
33 let rec translate = function
\r
34 | [] -> assert false
\r
35 | x::[] -> [triangle 0 2 x]
\r
37 let a,b,c = mk_triangle () in
\r
38 triangle a b c :: [arc x a; arc y b] :: translate (c::l) in
\r
39 let p = List.map (List.map (fun x ->
\r
40 if x = 0 then assert false
\r
41 else if x < 0 then 2 * (abs x + 1)
\r
44 let init2 = List.map (List.concat ++ translate) p in
\r
45 !freshno, init0 @ List.concat (init1 @ init2)
\r
48 let string_of_graph g =
\r
49 String.concat " " (List.map (fun (x,y) -> string_of_int x ^ "<>" ^ string_of_int y) g)
\r
53 let mv = maxvar p in
\r
54 prerr_endline (string_of_int mv);
\r
55 let _, g = reduction_sat_3col p in
\r
56 prerr_endline (string_of_graph g);
\r
59 prerr_endline (main[
\r
69 (* a, b endline separators *)
\r
73 let generate g n max =
\r
74 (* 0 <= n <= max+1 *)
\r
76 String.concat sep (List.map f [0;1;2]) in
\r
77 let rec aux' n m color =
\r
79 else aux' n (m-1) color ^
\r
81 (if List.mem (n,n) g then p_^p_^p_ (* cappio nel grafo *)
\r
82 else three (fun c -> if color = c then y_ else p_) "")
\r
83 else if n < m then y_^y_^y_
\r
84 else if List.mem (m,n) g then
\r
85 three (fun c -> if color = c then p_ else y_) ""
\r
90 if n < m then p_^p_^p_
\r
92 "(_." ^ three (aux' n max) "b) (_." ^ "b) "
\r
97 let generate2 g n max =
\r
101 if n < m then p_^p_^p_
\r
109 let encode_graph g =
\r
110 let g = List.map (fun (x,y) -> min x y, max x y) g in
\r
111 let mapi f a = Array.to_list (Array.mapi f a) in
\r
113 List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 in
\r
114 String.concat "\n" ("\n$ problem from 3-colorability" ::
\r
115 let no = nodex_no g in
\r
117 (if i = no+1 then "D " else "C ") ^ generate g i no
\r
118 ) (Array.make (no+2) ()) @
\r
120 "C " ^ generate2 g i no
\r
121 ) (Array.make (no+1) ());
\r
125 print_endline "Three example encodings:";;
\r
128 prerr_endline (encode_graph [0,1;]);;
\r
130 (* two imopssible problems *)
\r
132 encode_graph [0,1; 1,1]
\r
135 encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3]
\r
138 (******************************************************************************)
\r
140 print_endline "\nIt will now run some problems and decode the solutions";;
\r
141 print_endline "Press ENTER to continue.";;
\r
142 let _ = read_line ();;
\r
144 let strip_lambda_matches =
\r
145 let getvar = function
\r
147 | _ -> assert false in
\r
148 let rec aux n = function
\r
149 | `Lam(_,t) -> aux (n+1) t
\r
150 | `Match(_,_,_,bs,_) -> Some (n, List.map (getvar ++ snd) !bs)
\r
155 let next_candidates sigma cands =
\r
156 let sigma = Util.filter_map
\r
157 (fun x -> try Some (List.assoc x sigma) with Not_found -> None) cands in
\r
158 match Util.find_opt strip_lambda_matches sigma with
\r
163 let fix_numbers l =
\r
164 let rec aux n = function
\r
166 | x::xs -> (x - 2*n - 1) :: (aux (n+1) xs)
\r
170 let color (g:graph) =
\r
171 let p = encode_graph g in
\r
172 let (_, _, _, _, vars as p) = Parser.problem_of_string p in
\r
173 let _, result = Lambda4.solve (Lambda4.problem_of p) in
\r
175 | `Unseparable _ -> prerr_endline "Graph not colorable"; None
\r
176 | `Separable sigma -> (
\r
177 (* start from variable x *)
\r
178 let x = Util.index_of "x" vars in
\r
179 (* List.iter (fun x -> prerr_endline (string_of_int (fst x) ^ ":" ^ Num.print ~l:vars (snd x))) sigma; *)
\r
181 let n, x = f x in if x = [] then [] else n :: iter f x in
\r
182 let numbers = iter (next_candidates sigma) [x] in
\r
183 let numbers = fix_numbers numbers in
\r
184 (* display solution *)
\r
185 let colors = ["r"; "g"; "b"] in
\r
186 prerr_endline ("\nSolution found:\n " ^ String.concat "\n "
\r
187 (List.mapi (fun i x ->
\r
188 string_of_int i ^ " := " ^ List.nth colors x) numbers));
\r
189 assert (List.for_all (fun (a,b) -> List.nth numbers a <> List.nth numbers b) g);
\r
195 List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 g in
\r
196 let check x = if List.for_all (fun (a,b) -> List.nth x a <> List.nth x b) g
\r
197 then failwith "bruteforce: sat" in
\r
198 let rec guess l = prerr_string "+";
\r
199 if List.length l = nodes_no
\r
201 else (guess (0::l); guess (1::l); guess (2::l)) in
\r
203 prerr_endline "bruteforce: unsat"
\r
206 assert (color [0,1;0,2;1,2;2,3;3,0] <> None);;
\r
207 assert (color [0,1;0,2;1,2;2,3;3,0;0,4;4,2] <> None);;
\r
210 1,2; 1,4; 1,7; 1,9; 2,3; 2,6; 2,8; 3,5;
\r
211 3,7; 3,0; 4,5; 4,6; 4,0; 5,8; 5,9; 6,11;
\r
212 7,11; 8,11; 9,11; 0,11;
\r
215 (* https://turing.cs.hbg.psu.edu/txn131/file_instances/coloring/graph_color/queen5_5.col *)
\r
projects / fireball-separation.git / blob