X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsat.ml;fp=ocaml%2Fsat.ml;h=0000000000000000000000000000000000000000;hb=21c829a0b518a725f4db3d21250ad00dcf3bb889;hp=01d739800b077ff5a6cd5170a3d79bfe0f8fd759;hpb=4c157f176c89dcb5633d60c5be8a444ae0529c29;p=fireball-separation.git

diff --git a/ocaml/sat.ml b/ocaml/sat.ml
deleted file mode 100644
index 01d7398..0000000
--- a/ocaml/sat.ml
+++ /dev/null
@@ -1,535 +0,0 @@
-(*
- Reductions from SAT and 3-colorability of graphs to separation
- of lambda-terms. Commented out the encoding from SAT.
-*)
-
-open Util;;
-
-(* 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;;
-type color = int;;
-
-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) ());
- )
-;;
-
-print_endline "Three example encodings:";;
-
-(* 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]
-);;
-
-(******************************************************************************)
-
-print_endline "\nIt will now run some problems and decode the solutions";;
-print_endline "Press ENTER to continue.";;
-let _ = read_line ();;
-
-let strip_lambda_matches =
- let getvar = function
-  | `Var(n,_) -> n
-  | _ -> assert false in
- let rec aux n = function
-  | `Lam(_,t) -> aux (n+1) t
-  | `Match(_,_,_,bs,_) -> Some (n, List.map (getvar ++ snd) !bs)
-  | _ -> None
- in aux 0
-;;
-
-let next_candidates sigma cands =
- let sigma = Util.filter_map
-  (fun x -> try Some (List.assoc x sigma) with Not_found -> None) cands in
- match Util.find_opt strip_lambda_matches sigma with
- | None -> -1, []
- | Some x -> x
-;;
-
-let fix_numbers l =
- let rec aux n = function
- | [] -> []
- | x::xs -> (x - 2*n - 1) :: (aux (n+1) xs)
- in aux 0 l
-;;
-
-let color (g:graph) =
- let p = encode_graph g in
- let (_, _, _, _, vars as p) = Parser.problem_of_string p in
- let _, result = Lambda4.solve (Lambda4.problem_of p) in
- match result with
- | `Unseparable _ -> prerr_endline "Graph not colorable"; None
- | `Separable sigma -> (
-  (* start from variable x *)
-  let x = Util.index_of "x" vars in
-  (* List.iter (fun x -> prerr_endline (string_of_int (fst x) ^ ":" ^ Num.print ~l:vars (snd x))) sigma; *)
-  let rec iter f x =
-   let n, x = f x in if x = [] then [] else n :: iter f x in
-  let numbers = iter (next_candidates sigma) [x] in
-  let numbers = fix_numbers numbers in
-  (* display solution *)
-  let colors = ["r"; "g"; "b"] in
-  prerr_endline ("\nSolution found:\n " ^ String.concat "\n "
-   (List.mapi (fun i x ->
-     string_of_int i ^ " := " ^ List.nth colors x) numbers));
-  assert (List.for_all (fun (a,b) -> List.nth numbers a <> List.nth numbers b) g);
-  Some numbers)
-;;
-
-let bruteforce g =
- let nodes_no = 1+
-  List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 g in
- let check x = if List.for_all (fun (a,b) -> List.nth x a <> List.nth x b) g
-  then failwith "bruteforce: sat" in
- let rec guess l = prerr_string "+";
-  if List.length l = nodes_no
-   then check l
-    else (guess (0::l); guess (1::l); guess (2::l)) in
- guess [];
- prerr_endline "bruteforce: unsat"
-;;
-
-assert (color [0,1;0,2;1,2;2,3;3,0] <> None);;
-assert (color [0,1;0,2;1,2;2,3;3,0;0,4;4,2] <> None);;
-
-(* assert (color [
- 1,2; 1,4; 1,7; 1,9; 2,3; 2,6; 2,8; 3,5;
- 3,7; 3,0; 4,5; 4,6; 4,0; 5,8; 5,9; 6,11;
- 7,11; 8,11; 9,11; 0,11;
-] = None);; *)
-
-(* https://turing.cs.hbg.psu.edu/txn131/file_instances/coloring/graph_color/queen5_5.col *)
-color [1,7
-; 1,13
-; 1,19
-; 1,25
-; 1,2
-; 1,3
-; 1,4
-; 1,5
-; 1,6
-; 1,11
-; 1,16
-; 1,21
-; 2,8
-; 2,14
-; 2,20
-; 2,6
-; 2,3
-; 2,4
-; 2,5
-; 2,7
-; 2,12
-; 2,17
-; 2,22
-; 2,1
-; 3,9
-; 3,15
-; 3,7
-; 3,11
-; 3,4
-; 3,5
-; 3,8
-; 3,13
-; 3,18
-; 3,23
-; 3,2
-; 3,1
-; 4,10
-; 4,8
-; 4,12
-; 4,16
-; 4,5
-; 4,9
-; 4,14
-; 4,19
-; 4,24
-; 4,3
-; 4,2
-; 4,1
-; 5,9
-; 5,13
-; 5,17
-; 5,21
-; 5,10
-; 5,15
-; 5,20
-; 5,25
-; 5,4
-; 5,3
-; 5,2
-; 5,1
-; 6,12
-; 6,18
-; 6,24
-; 6,7
-; 6,8
-; 6,9
-; 6,10
-; 6,11
-; 6,16
-; 6,21
-; 6,2
-; 6,1
-; 7,13
-; 7,19
-; 7,25
-; 7,11
-; 7,8
-; 7,9
-; 7,10
-; 7,12
-; 7,17
-; 7,22
-; 7,6
-; 7,3
-; 7,2
-; 7,1
-; 8,14
-; 8,20
-; 8,12
-; 8,16
-; 8,9
-; 8,10
-; 8,13
-; 8,18
-; 8,23
-; 8,7
-; 8,6
-; 8,4
-; 8,3
-; 8,2
-; 9,15
-; 9,13
-; 9,17
-; 9,21
-; 9,10
-; 9,14
-; 9,19
-; 9,24
-; 9,8
-; 9,7
-; 9,6
-; 9,5
-; 9,4
-; 9,3
-; 10,14
-; 10,18
-; 10,22
-; 10,15
-; 10,20
-; 10,25
-; 10,9
-; 10,8
-; 10,7
-; 10,6
-; 10,5
-; 10,4
-; 11,17
-; 11,23
-; 11,12
-; 11,13
-; 11,14
-; 11,15
-; 11,16
-; 11,21
-; 11,7
-; 11,6
-; 11,3
-; 11,1
-; 12,18
-; 12,24
-; 12,16
-; 12,13
-; 12,14
-; 12,15
-; 12,17
-; 12,22
-; 12,11
-; 12,8
-; 12,7
-; 12,6
-; 12,4
-; 12,2
-; 13,19
-; 13,25
-; 13,17
-; 13,21
-; 13,14
-; 13,15
-; 13,18
-; 13,23
-; 13,12
-; 13,11
-; 13,9
-; 13,8
-; 13,7
-; 13,5
-; 13,3
-; 13,1
-; 14,20
-; 14,18
-; 14,22
-; 14,15
-; 14,19
-; 14,24
-; 14,13
-; 14,12
-; 14,11
-; 14,10
-; 14,9
-; 14,8
-; 14,4
-; 14,2
-; 15,19
-; 15,23
-; 15,20
-; 15,25
-; 15,14
-; 15,13
-; 15,12
-; 15,11
-; 15,10
-; 15,9
-; 15,5
-; 15,3
-; 16,22
-; 16,17
-; 16,18
-; 16,19
-; 16,20
-; 16,21
-; 16,12
-; 16,11
-; 16,8
-; 16,6
-; 16,4
-; 16,1
-; 17,23
-; 17,21
-; 17,18
-; 17,19
-; 17,20
-; 17,22
-; 17,16
-; 17,13
-; 17,12
-; 17,11
-; 17,9
-; 17,7
-; 17,5
-; 17,2
-; 18,24
-; 18,22
-; 18,19
-; 18,20
-; 18,23
-; 18,17
-; 18,16
-; 18,14
-; 18,13
-; 18,12
-; 18,10
-; 18,8
-; 18,6
-; 18,3
-; 19,25
-; 19,23
-; 19,20
-; 19,24
-; 19,18
-; 19,17
-; 19,16
-; 19,15
-; 19,14
-; 19,13
-; 19,9
-; 19,7
-; 19,4
-; 19,1
-; 20,24
-; 20,25
-; 20,19
-; 20,18
-; 20,17
-; 20,16
-; 20,15
-; 20,14
-; 20,10
-; 20,8
-; 20,5
-; 20,2
-; 21,22
-; 21,23
-; 21,24
-; 21,25
-; 21,17
-; 21,16
-; 21,13
-; 21,11
-; 21,9
-; 21,6
-; 21,5
-; 21,1
-; 22,23
-; 22,24
-; 22,25
-; 22,21
-; 22,18
-; 22,17
-; 22,16
-; 22,14
-; 22,12
-; 22,10
-; 22,7
-; 22,2
-; 23,24
-; 23,25
-; 23,22
-; 23,21
-; 23,19
-; 23,18
-; 23,17
-; 23,15
-; 23,13
-; 23,11
-; 23,8
-; 23,3
-; 24,25
-; 24,23
-; 24,22
-; 24,21
-; 24,20
-; 24,19
-; 24,18
-; 24,14
-; 24,12
-; 24,9
-; 24,6
-; 24,4
-; 25,24
-; 25,23
-; 25,22
-; 25,21
-; 25,20
-; 25,19
-; 25,15
-; 25,13
-; 25,10
-; 25,7
-; 25,5
-; 25,1];;