ocaml/sat.ml

   1 (*\r
   2  Reductions from SAT and 3-colorability of graphs to separation\r
   3  of lambda-terms. Commented out the encoding from SAT.\r
   4 *)\r
   5 \r
   6 (* type cnf = int list list;;\r
   7 \r
   8 let (++) f g x = f (g x);;\r
   9 \r
  10 let maxvar : cnf -> int =\r
  11  let aux f = List.fold_left (fun acc x -> max acc (f x)) 0 in\r
  12  aux (aux abs)\r
  13 ;; *)\r
  14 \r
  15 type graph = (int * int) list;;\r
  16 \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
  19 \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
  24  let n = maxvar p in\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
  28   let i = !freshno in\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
  33  | x::y::l ->\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
  39     else 2 * x + 1\r
  40   )) p in\r
  41  let init2 = List.map (List.concat ++ translate) p in\r
  42  !freshno, init0 @ List.concat (init1 @ init2)\r
  43 ;;\r
  44 \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
  47 ;; *)\r
  48 \r
  49 (* let main p =\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
  54  generate ;;\r
  55 \r
  56 prerr_endline (main[\r
  57  [1; -2; 3];\r
  58  [2; 4; -5]\r
  59 ]);; *)\r
  60 \r
  61 let p_ = "BOMB ";;\r
  62 let x_ = "x ";;\r
  63 (* y, z dummies *)\r
  64 let y_ = "y ";;\r
  65 let z_ = "z ";;\r
  66 (* a, b endline separators *)\r
  67 let a_ = "a ";;\r
  68 let b_ = "b ";;\r
  69 \r
  70 let generate g n max =\r
  71  (* 0 <= n <= max+1 *)\r
  72  let three f sep =\r
  73   String.concat sep (List.map f [0;1;2]) in\r
  74  let rec aux' n m color =\r
  75   if m = -1 then x_\r
  76   else aux' n (m-1) color ^\r
  77    if n = m then\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
  83    else y_^y_^y_ in\r
  84  let rec aux m =\r
  85   if m = -1 then x_\r
  86    else aux (m-1) ^\r
  87     if n < m then p_^p_^p_\r
  88     else if n = m then\r
  89       "(_." ^ three (aux' n max) "b) (_." ^ "b) "\r
  90     else y_^y_^y_\r
  91  in aux max ^ a_\r
  92 ;;\r
  93 \r
  94 let generate2 g n max =\r
  95  let rec aux m =\r
  96   if m = -1 then x_\r
  97    else aux (m-1) ^\r
  98     if n < m then p_^p_^p_\r
  99     else if n = m\r
 100     then z_^z_^z_\r
 101     else y_^y_^y_\r
 102  in aux max ^ p_\r
 103 ;;\r
 104 \r
 105 \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
 109  let nodex_no =\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
 113   mapi (fun i () ->\r
 114     (if i = no+1 then "D " else "C ") ^ generate g i no\r
 115   ) (Array.make (no+2) ()) @\r
 116   mapi (fun i () ->\r
 117     "C " ^ generate2 g i no\r
 118   ) (Array.make (no+1) ());\r
 119  )\r
 120 ;;\r
 121 \r
 122 (* easy one *)\r
 123 prerr_endline (encode_graph [0,1;]);;\r
 124 \r
 125 (* two imopssible problems *)\r
 126 prerr_endline (\r
 127  encode_graph [0,1; 1,1]\r
 128 );;\r
 129 prerr_endline (\r
 130  encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3]\r
 131 );;\r