Resolve "add horn sat algorithm"

Closes #5 (closed) Closes #4 (closed)

project1/lib/lib.ml

+open Dolmen
+open Printf
+
+(* generate dimacs files *)
+let generate_dimacs oc horn variables clauses =
+  Random.self_init ();
+  fprintf oc "p cnf %d %d\n" variables clauses;
+  for _ = 1 to clauses do
+
+    let nb_var = 1 + Random.int variables in
+
+    if horn then (
+      for _ = 1 to nb_var - 1 do
+        let var = 1 + Random.int variables in
+        fprintf oc "%d " (- var)
+      done;
+      let concl = Random.int 5 in
+      if concl != 0 || nb_var == 1 then
+        let var = 1 + Random.int variables in
+        fprintf oc "%d " var
+
+    ) else (
+      for _ = 1 to nb_var do
+        let var = 1 + Random.int variables in
+        let sign = 2 * (Random.int 2) - 1 in
+        fprintf oc "%d " (sign * var)
+      done
+    );
+
+    fprintf oc "0\n"
+  done
+
+(* open and print the content of a file *)
+let print_file name =
+  print_endline name;
+  let ic = open_in name in
+  try
+    while true do
+      print_endline (input_line ic)
+    done
+  with End_of_file ->
+    close_in ic
+
+(* polymorphic function to remove duplicates from lists *)
+let remove_duplicates (type a) (l: a list) =
+  let module S = Set.Make(struct type t = a let compare = compare end) in
+  let rec remove acc seen_set = function
+    | [] -> List.rev acc
+    | a :: rest when S.mem a seen_set -> remove acc seen_set rest
+    | a :: rest -> remove (a::acc) (S.add a seen_set) rest in
+  remove [] S.empty l
+
+(* print a list *)
+let print_list print l =
+  let buffer = Buffer.create 100 in
+  Buffer.add_char buffer '[';
+  let rec aux  = function
+    |[] -> Buffer.add_char buffer ']'
+    |[x] ->  Buffer.add_string buffer (print x); Buffer.add_char buffer ']'
+    |x::l -> Buffer.add_string buffer (print x);Buffer.add_char buffer ';'; aux l
+  in 
+  aux l;
+  Buffer.contents buffer
+
+(** naive XOR to cnf formula conversion **)
+type formula = Neg of formula
+             | Or of formula * formula
+             | And of formula * formula
+             | Var of int
+             | Xor of formula * formula
+
+let rec print_formula = function
+  | Neg f ->
+    print_string "~(";
+    print_formula f;
+    print_string ")"
+  | Or (a,b) ->
+    print_string "(";
+    print_formula a;
+    print_string " or ";
+    print_formula b;
+    print_string ")"
+  | And (a,b) ->
+    print_string "(";
+    print_formula a;
+    print_string " and ";
+    print_formula b;
+    print_string ")"
+  | Xor (a,b) ->
+    print_string "(";
+    print_formula a;
+    print_string " xor ";
+    print_formula b;
+    print_string ")"
+  | Var x ->
+    print_int x
+
+let rec remove_xor = function
+  | Xor (a, b) ->
+    let a = remove_xor a
+    and b = remove_xor b in
+    (And (Or (a,b), Or (Neg a, Neg b)))
+  | Or (a,b) -> Or (remove_xor a, remove_xor b)
+  | And (a,b) -> And (remove_xor a, remove_xor b)
+  | Neg a -> Neg (remove_xor a)
+  | Var x -> Var x
+
+let rec to_cnf = function
+  | Neg (Var i) -> Var (-i)
+  | Neg (Neg (a)) -> to_cnf a
+  | Neg (And (a,b)) -> to_cnf (Or (Neg a, Neg b))
+  | Neg (Or (a,b)) -> to_cnf (And (Neg a, Neg b))
+  | Or (And (a,b), c) -> to_cnf (And (Or (a,c), Or(b,c)))
+  | Or (c, And (a,b)) -> to_cnf (And (Or (a,c), Or(b,c)))
+  | And (a,b) -> And (to_cnf a, to_cnf b)
+  | Or (a,b) ->
+    let a = to_cnf a
+    and b = to_cnf b in
+    (match (a,b) with
+     | And _, _ | _, And _ -> to_cnf (Or (a,b))
+     | _ -> Or (a,b)
+    )
+  | Var i -> Var i
+  | _ -> failwith "cannot happen"
+
+let cnf_to_int_list form =
+  let res = ref [] in
+
+  let rec clause c = function
+    | Or (a,b) ->
+      clause c a;
+      clause c b
+    | Var i ->
+      c :=  i :: !c
+    | _ -> failwith "cannot happen"
+  in
+
+  let rec conjonction = function
+    | And (a,b) ->
+      conjonction a;
+      conjonction b
+    | Or (a,b) ->
+      let c = ref [] in
+      clause c a;
+      clause c b;
+      res := !c :: !res
+    | Var i ->
+      res := [i] :: !res
+    | _ -> failwith "cannot happen"
+  in
+
+  conjonction form;
+  !res
+
+module Term : Dolmen_dimacs.Term
+  with type location =  Std.Loc.t
+   and type t = int
+= struct
+
+  type location = Std.Loc.t
+  type t = int
+  let atom ?loc x = let _ = loc in x
+
+end
+
+module Statement(Term : Dolmen_dimacs.Term with type t = int) : Dolmen_dimacs.Statement
+  with type location =  Std.Loc.t
+   and type term = Term.t
+   and type t = int list
+= struct
+
+  type location = Std.Loc.t
+  type term = int
+  type t = int list
+
+  let p_cnf ?loc nb_var nb_clause =
+    let _ = loc in
+    [nb_var; nb_clause]
+
+  let clause ?loc l =
+    let _ = loc in
+    l
+
+end
+
+module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
+
+let convert_xorsat file =
+  match snd (M.parse_file file) with
+  | [nb_var; nb_clause] :: statements ->
+
+    let statements = List.concat_map (fun l ->
+        cnf_to_int_list (
+          to_cnf (
+            remove_xor (
+              (List.fold_left
+                 (fun form x -> Xor (form,Var x))
+                 (Var (List.hd l)) (List.tl l))))))
+        statements
+    in
+
+    let oc = open_out "conversion.cnf" in
+    Printf.fprintf oc "p cnf %d %d\n" nb_var nb_clause;
+    List.iter (fun clause ->
+        List.iter (fun x -> Printf.fprintf oc "%d " x) clause;
+        Printf.fprintf oc "0\n"
+      ) statements;
+    close_out oc
+  | _ -> failwith "cannot happen"