Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

 open Dolmen
 open Lib
 
-(* A data structure to hold XOR clauses efficently: *)
+(** 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. *)
@@ -26,13 +26,22 @@ module Term : Dolmen_dimacs.Term
 
 end
 
-let to_model arr = 
+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
 
+let to_model arr = 
+  let res = ref [] in
+  for i = 1 to Array.length arr - 1 do
+    if arr.(i) then 
+      res := i::!res
+    else
+      res := (-i)::!res
+  done;
+  List.rev !res
 
 (* Replace every negative variable by it's negation *)
 (* and add or remove 1 to the clause. *)
@@ -42,15 +51,15 @@ let positify nb_var (b,l) =
   let rec aux = function
     | [] -> ()
     | h::l -> 
-        if h<0 then begin
-          one := not !one;
-          seen.(-h) <- not seen.(-h)
-        end else 
-          seen.(h) <- not seen.(h);
+      if h<0 then begin
+        one := not !one;
+        seen.(-h) <- not seen.(-h)
+      end else
+        seen.(h) <- not seen.(h);
       aux l
   in 
   aux l;
-  (!one, to_model seen)
+  (!one, to_list seen)
 
 
 module Statement(Term : Dolmen_dimacs.Term with type t = int) : Dolmen_dimacs.Statement
@@ -82,38 +91,34 @@ let stmt_to_string = print_list (fun (b,l) -> "("^(string_of_bool b)^","^print_l
 let flatten nb_var trace (l : (bool * int list) list) =
   let _ = nb_var in 
   let rec aux = function
-    | [] ->    []
+    | [] ->         []
     | (n,[])::l ->  (n,[])::(aux l)
-    | [l] ->   [l]
+    | [l] ->        [l]
     | (b,[x])::l -> 
-        (*if x is a negative literal, then it's equivalent to -x xor 1, so we can substitute x for 0 in all instances of the rest of the xnf,
-          which is equivalent to removing x*)
-        if b then 
-          (b,[x])::(List.map 
-            (fun (b,l) -> (b,List.filter (fun y -> x <> y) l)) 
-            (aux l))
-        else
-          (b,[x])::(aux l)
+      (*if x is a negative literal, then it's equivalent to x xor 1, so we can substitute x for 0 in all instances of the rest of the xnf,
+        which is equivalent to removing x*)
+      if not b then (b,[x])::(aux l) else (
+        trace := ("propagating "^(string_of_int x))::!trace;
+        (b,[x])::(List.map
+                    (fun (b,l) -> (b, List.filter (fun y -> x <> y) l))
+                    (aux l))
+      )
     | (b,h::not_t)::l -> (
-        let foo = 
-          aux 
+        let foo = aux
             (List.map
-              (fun (n,x) -> 
-                  positify nb_var
-                  ((if List.mem h x then b else false) <> n,
-                  List.flatten (List.map (fun x -> if x = h then not_t else [x]) x)))
-              l
-            ) in
-        trace := ("substituting "^(string_of_int h)^" with "^"("^(string_of_bool b)^","^print_list string_of_int not_t^") in "^(stmt_to_string l))::!trace;
-        trace := "found:"::!trace;
-        trace := (stmt_to_string foo)::!trace;
+               (fun (n, x) ->
+                  let bb = ref n in
+                  positify nb_var (n, List.flatten (List.map (fun x -> if x = h then (bb := b <> !bb; not_t) else [x]) x))
+               )
+               l) in
+        trace := ("substituting "^(string_of_int h)^" with "^"~("^(string_of_bool b)^","^print_list string_of_int not_t^") in "^(stmt_to_string l))::!trace;
         foo
       ) in
   aux l
 
 let add_state (trace : string list ref) (s : S.t) (stmt : M.statement list) =
   let buffer = Buffer.create 100 in
-  Buffer.add_string buffer "Checking :\n";
+  Buffer.add_string buffer "Checking:\n";
   Buffer.add_string buffer (stmt_to_string stmt);
   Buffer.add_string buffer "\n in model:\n";
   Buffer.add_string buffer (print_list string_of_int (List.of_seq (S.to_seq s)));
@@ -121,68 +126,45 @@ let add_state (trace : string list ref) (s : S.t) (stmt : M.statement list) =
 
 let add_unsat_duplicate (trace : string list ref) (x : int) =
   let buffer = Buffer.create 100 in
-  Buffer.add_string buffer "UNSAT\n Found duplicate variable :";
+  Buffer.add_string buffer "UNSAT\n Found duplicate variable:";
   Buffer.add_string buffer (string_of_int x);
   trace := (Buffer.contents buffer)::!trace
 
 let process (statements: M.statement list) =
   Printexc.record_backtrace true;
   let (_,[nb_var])::statements = statements in
-  let trace : string list ref = ref ["Formula to test :"] in
-  trace := (stmt_to_string statements)::!trace;
+  let trace : string list ref = ref [] in
   let l = statements |> List.map (positify nb_var)  in
-  trace := "Positified formula :"::!trace;
-  trace := (stmt_to_string l)::!trace;
-  let l = l |> flatten nb_var trace in
-  trace := "Flattened formula :"::!trace;
-  trace := (stmt_to_string l)::!trace;
+  let l2 = l |> flatten nb_var trace in
+  trace :=
+    ("Formula to test:\n"^(stmt_to_string statements)^
+     "\nPositified formula:\n"^(stmt_to_string l)^
+     "\nFlattened formula:\n"^(stmt_to_string l2)^"\n") :: !trace;
 
   (*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*)
+    - 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 model = Array.make (nb_var+1) false in
-  let rec aux = function
-    | [] -> (true,[])
-    | [b,t] ->
-        let fb = ref b in
-        let t = (List.filter 
-            (fun x -> 
-              if x<0 then
-                failwith "wtf"
-              else
-              if model.(abs x) then begin
-                fb := not !fb;
-                false
-              end else true
-            ) t) in
-        (!fb,t)
-    | (false,[])::_ -> 
-      trace := "Empty clause found"::!trace;
-        failwith "unsat"
-    | (true,[])::l -> 
-        aux l
-    | (false,[x])::l -> 
-        if x<0 then
-          failwith "something badbad happened"
-        else
-        model.(x) <- true;
-        aux l
-    | (_,_::_)::_ ->
-        failwith "something bad happened"
-
-    in
-  try
-    match aux l  with
-      | (true,[]) -> Ok(model |> to_model ,List.rev !trace)
-      | (false,[]) -> Error(List.rev !trace)
-      | (true,_::_) -> Ok(model |> to_model,List.rev !trace)
-      | (false,h::_) -> 
-          model.(h) <- true;
-          Ok(model |> to_model,List.rev !trace)
-    
-  with
-    _ -> Error (List.rev !trace)
+
+  let rec get_result = function
+    | [] -> true
+    | [(b,l)] ->
+      let bb = ref b in
+      let l = List.filter (fun x -> if model.(x) then (bb := not !bb; false) else true) l in
+      if !bb then true
+      else begin match l with
+        | [] -> false
+        | x::_ -> model.(x) <- true; true
+      end
+    | (false, [x])::l -> model.(x) <- true; get_result l
+    | (true, _)::l -> get_result l
+    | (false, [])::_ -> print_endline "haa"; false
+    | (_,h)::_ -> print_endline (print_list string_of_int h); failwith "cannot happen"
+  in
+  if get_result l2
+  then Ok(model |> to_model, !trace)
+  else Error(!trace)