From 48099a8d17ed96681087fa7e7c507dc2ec209125 Mon Sep 17 00:00:00 2001 From: acondolu Date: Sat, 15 Jul 2017 15:31:50 +0200 Subject: [PATCH] Encoding of SAT problems and 3-colorability of graphs --- ocaml/Makefile | 3 ++ ocaml/sat.ml | 131 +++++++++++++++++++++++++++++++++++++++++++++++++ ocaml/sat.mli | 3 ++ 3 files changed, 137 insertions(+) create mode 100644 ocaml/sat.ml create mode 100644 ocaml/sat.mli diff --git a/ocaml/Makefile b/ocaml/Makefile index 430f159..0f00f14 100644 --- a/ocaml/Makefile +++ b/ocaml/Makefile @@ -13,6 +13,9 @@ a.out: $(UTILS) lambda4.cmx problems.cmx # test.out: $(UTILS) lambda3.cmx test1.ml # $(OCAMLC) -o test.out $(LIB) $^ + +sat.out: $(UTILS) lambda4.cmx sat.ml + $(OCAMLC) -o sat.out $(LIB) $^ # test4.out: $(UTILS) lambda4.cmx test.ml $(OCAMLC) -o test4.out $(LIB) $^ diff --git a/ocaml/sat.ml b/ocaml/sat.ml new file mode 100644 index 0000000..ceb90ca --- /dev/null +++ b/ocaml/sat.ml @@ -0,0 +1,131 @@ +(* + Reductions from SAT and 3-colorability of graphs to separation + of lambda-terms. Commented out the encoding from SAT. +*) + +(* type cnf = int list list;; + +let (++) f g x = f (g x);; + +let maxvar : cnf -> int = + let aux f = List.fold_left (fun acc x -> max acc (f x)) 0 in + aux (aux abs) +;; *) + +type graph = (int * int) list;; + +let arc x y = min x y, max x y;; +let mem g x y = List.mem (arc x y) g;; + +(* let reduction_sat_3col p = + let triangle a0 a1 a2 = [arc a0 a1; arc a0 a2; arc a1 a2] in + let init0 = triangle 0 1 2 in + (* 0false; 1true; 2base*) + let n = maxvar p in + let init1 = Array.to_list (Array.mapi (fun i () -> triangle (2*i+1) (2*(i+1)) 2) (Array.make n ())) in + let freshno = ref (2 * n + 3) in + let mk_triangle () = + let i = !freshno in + freshno := i+3; i, i+1, i+2 in + let rec translate = function + | [] -> assert false + | x::[] -> [triangle 0 2 x] + | x::y::l -> + let a,b,c = mk_triangle () in + triangle a b c :: [arc x a; arc y b] :: translate (c::l) in + let p = List.map (List.map (fun x -> + if x = 0 then assert false + else if x < 0 then 2 * (abs x + 1) + else 2 * x + 1 + )) p in + let init2 = List.map (List.concat ++ translate) p in + !freshno, init0 @ List.concat (init1 @ init2) +;; + +let string_of_graph g = + String.concat " " (List.map (fun (x,y) -> string_of_int x ^ "<>" ^ string_of_int y) g) +;; *) + +(* let main p = + let mv = maxvar p in + prerr_endline (string_of_int mv); + let _, g = reduction_sat_3col p in + prerr_endline (string_of_graph g); + generate ;; + +prerr_endline (main[ + [1; -2; 3]; + [2; 4; -5] +]);; *) + +let p_ = "BOMB ";; +let x_ = "x ";; +(* y, z dummies *) +let y_ = "y ";; +let z_ = "z ";; +(* a, b endline separators *) +let a_ = "a ";; +let b_ = "b ";; + +let generate g n max = + (* 0 <= n <= max+1 *) + let three f sep = + String.concat sep (List.map f [0;1;2]) in + let rec aux' n m color = + if m = -1 then x_ + else aux' n (m-1) color ^ + if n = m then + (if List.mem (n,n) g then p_^p_^p_ (* cappio nel grafo *) + else three (fun c -> if color = c then y_ else p_) "") + else if n < m then y_^y_^y_ + else if List.mem (m,n) g then + three (fun c -> if color = c then p_ else y_) "" + else y_^y_^y_ in + let rec aux m = + if m = -1 then x_ + else aux (m-1) ^ + if n < m then p_^p_^p_ + else if n = m then + "(_." ^ three (aux' n max) "b) (_." ^ "b) " + else y_^y_^y_ + in aux max ^ a_ +;; + +let generate2 g n max = + let rec aux m = + if m = -1 then x_ + else aux (m-1) ^ + if n < m then p_^p_^p_ + else if n = m + then z_^z_^z_ + else y_^y_^y_ + in aux max ^ p_ +;; + + +let encode_graph g = + let g = List.map (fun (x,y) -> min x y, max x y) g in + let mapi f a = Array.to_list (Array.mapi f a) in + let nodex_no = + List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 in + String.concat "\n" ("\n$ problem from 3-colorability" :: + let no = nodex_no g in + mapi (fun i () -> + (if i = no+1 then "D " else "C ") ^ generate g i no + ) (Array.make (no+2) ()) @ + mapi (fun i () -> + "C " ^ generate2 g i no + ) (Array.make (no+1) ()); + ) +;; + +(* easy one *) +prerr_endline (encode_graph [0,1;]);; + +(* two imopssible problems *) +prerr_endline ( + encode_graph [0,1; 1,1] +);; +prerr_endline ( + encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3] +);; diff --git a/ocaml/sat.mli b/ocaml/sat.mli new file mode 100644 index 0000000..77f0239 --- /dev/null +++ b/ocaml/sat.mli @@ -0,0 +1,3 @@ +type graph = (int * int) list + +val encode_graph : graph -> string -- 2.39.2