Encoding of SAT problems and 3-colorability of graphs

diff --git a/ocaml/Makefile b/ocaml/Makefile
index 430f1596fa5f6c5c529f15c4a32c3350276913c9..0f00f1457f7a1adef14ca1a6c6c85b477c627931 100644 (file)
--- 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 (file)
index 0000000..ceb90ca
--- /dev/null
+++ b/ocaml/sat.ml
@@ -0,0 +1,131 @@
+(*\r
+ Reductions from SAT and 3-colorability of graphs to separation\r
+ of lambda-terms. Commented out the encoding from SAT.\r
+*)\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
+\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
+(* 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

diff --git a/ocaml/sat.mli b/ocaml/sat.mli
new file mode 100644 (file)
index 0000000..77f0239
--- /dev/null
+++ b/ocaml/sat.mli
@@ -0,0 +1,3 @@
+type graph = (int * int) list\r
+\r
+val encode_graph : graph -> string\r