Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

-let process clauses = Ok ([List.length clauses]) (*TODO*)
+open Dolmen
+open Lib
+
+(** A data structure to hold XOR clauses efficently: *)
+
+(* Clauses are manipulated in order to never have negative variables occurences: *)
+(* if necessary, is added or remove from the clause. *)
+(* The clauses are thus represented by couples (boolean, array of boolean) *)
+(* ex : (p1 + p2) /\ ~p3 is represented as [(false, [0,2]),(true, [3])] *)
+
+(* The algorithm is as follows: *)
+(* - flatten the using the fact that (p + G) /\ F ≅ F[~G/p], this leaves us with a single big clause as well as singleton clauses *)
+(* - once flattened, check if a variable appears more than once with the same sign *)
+
+module S = Set.Make(struct type t = int let compare = compare end)
+
+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 = bool * S.t
+= struct
+
+  type location = Std.Loc.t
+  type term = int
+  type t = bool * S.t
+
+  let p_cnf ?loc nb_var _ =
+    let _ = loc in
+    false, S.singleton nb_var
+
+  let clause ?loc l =
+    let _ = loc in
+    let b2 = ref false in
+    let occ = Hashtbl.create (List.length l) in
+    List.iter (
+      fun x ->
+        if x<0 then b2 := not !b2;
+        let x = abs x in
+        if Hashtbl.mem occ x
+        then Hashtbl.remove occ x
+        else Hashtbl.add occ (abs x) ();
+    ) l;
+    let s2 = ref S.empty in
+    Hashtbl.iter (fun x _ -> s2 := S.add x !s2) occ;
+    (!b2, !s2)
+
+end
+
+module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
+
+let parse_file = fun x -> snd (M.parse_file x)
+
+let string_of_set f s =
+  let res = ref "" in
+  S.iter (fun x -> res := !res ^ " " ^ f x) s;
+  !res
+
+let stmt_to_string =
+  print_list (fun (b,s) -> "("^(string_of_bool b)^","^(string_of_set string_of_int s)^")")
+
+(* convert an array into a list *)
+let to_list arr =
+  let res = ref [] in
+  for i = 0 to Array.length arr - 1 do
+    if arr.(i) then res := i::!res
+  done;
+  !res
+
+(* convert an array into a SAT model *)
+let to_model arr =
+  let res = ref [] in
+  for i = 1 to Array.length arr - 1 do
+    match arr.(i) with
+    | Some(true) -> res := i::!res
+    | _ -> res := (-i)::!res
+  done;
+  List.rev !res
+
+(* We do as such:
+   - add all singleton variables in the model represented as an array
+   - Once we reach the last big clause, we search through the clause, and we remove all occurences of known variable while flipping the bool each time
+   - We're left with a bool and a clause with "unbound" variables:
+   - If there's at least 1 unbound variable, then the problem is sat
+   - if there's none, it's sat iff the bool is set to 1 *)
+
+let intersect s =
+  List.find_map (fun (_, s2) -> S.choose_opt (S.inter s s2))
+
+let contain x s =
+  match S.find_opt x s with
+  | Some _ -> true
+  | None -> false
+
+let resolve trace model (b, s) =
+  trace := ("resolving "^(stmt_to_string [(b,s)]))::!trace;
+  let b2 = ref b in
+  let s2 = S.filter (
+      fun x -> match model.(x) with
+        | Some(true) ->
+          b2 := not !b2;
+          false
+        | Some(false) -> false
+        | None -> true) s in
+  if !b2 then true
+  else (
+    match S.choose_opt s2 with
+    | Some(x) -> model.(x) <- Some(true); true
+    | None -> false
+  )
+
+let get_result trace (model : bool option array) (l : (bool * S.t) list) =
+
+  let constraints = ref [] in
+
+  let rec aux = function
+
+    | [] ->
+      trace := ("checking constraints "^(print_list (fun (x,(b,s)) -> (string_of_int x)^"<>"^(stmt_to_string [(b,s)])) !constraints))::!trace;
+      List.fold_left (fun acc (x, (b,c_x)) ->
+          acc && (
+            let count = S.cardinal (S.filter (fun x -> model.(x) = Some(true)) c_x) in
+            let value = b <> ((count mod 2) = 1) in
+            match model.(x) with
+            | Some(v) when v = value -> false
+            | None -> model.(x) <- Some(not value); true
+            | _ -> true
+          )
+        ) true !constraints
+
+    | (false, s)::_ when S.cardinal s = 0 -> false
+
+    | (true,  s)::l when S.cardinal s = 0 -> aux l
+
+    | [cl] -> resolve trace model cl && aux []
+
+    | (false, s)::l when S.cardinal s = 1 ->
+      let x = S.choose s in
+      trace := ("propagating "^(string_of_int x)^" to true")::!trace;
+      let conflict = model.(x) = Some(false) in
+      model.(x) <- Some true;
+      (not conflict) && aux l
+
+    | (true, s)::l when S.cardinal s = 1 ->
+      let x = S.choose s in
+      trace := ("propagating "^(string_of_int x)^" to false in "^(stmt_to_string l))::!trace;
+      let conflict = model.(x) = Some(true) in
+      model.(x) <- Some false;
+      (not conflict) && aux (List.map (fun (b, s2) -> (b, S.remove x s2)) l)
+
+    | (b, s)::l ->
+      begin match intersect s l with
+        | Some(x) ->
+          let s_x = S.remove x s in
+          trace := ("substituting "^(string_of_int x)^
+                    " with "^"~("^(string_of_bool b)^
+                    ","^(string_of_set string_of_int s_x)^
+                    ") in "^(stmt_to_string l))::!trace;
+
+          constraints := (x,(b,s_x)) :: !constraints;
+
+          aux (List.map (fun (b2, s2) ->
+
+              if contain x s2
+              then
+                let b3 = (b = b2) in
+                let s3 = S.remove x s2 in
+                let s4 = S.inter s_x s3 in
+                let s5 = S.union (S.diff s3 s4) (S.diff s_x s4) in
+                (b3, s5)
+              else
+                (b2, s2)
+            ) l)
+        | None -> resolve trace model (b, s) && aux l
+      end
+
+  in aux l
+
+
+let process = function
+  | (_,hd)::tl ->
+
+    let nb_var = S.choose hd in
+    let trace : string list ref = ref []
+    and model = Array.make (nb_var+1) None in
+
+    trace := ("Formula to test:\n"^(stmt_to_string tl))::!trace;
+
+    if get_result trace model tl
+    then Ok(model |> to_model, List.rev !trace)
+    else Error(List.rev !trace)
+
+  | _ -> failwith "cannot happen"