Skip to content
Snippets Groups Projects

Resolve "add horn sat algorithm"

Merged Resolve "add horn sat algorithm"
5-add-horn-sat-algorithm into main
Merged aalbert requested to merge 5-add-horn-sat-algorithm into main
Compare
and
Show latest version
2 files
+ 156
− 125
Compare changes
  • Side-by-side
  • Inline
Files
2
project1/bin/xor.ml
+ 153
− 122
@@ -5,8 +5,8 @@ open Lib
(* 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, list of positive interger) *)
(* ex : (p1 + p2) /\ ~p3 is represented as [(false, [1,2]),(true, [3])] *)
(* 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 *)
@@ -14,7 +14,6 @@ open Lib
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
@@ -26,59 +25,35 @@ module Term : Dolmen_dimacs.Term
end
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. *)
let positify nb_var (b,l) =
let one = ref b in
let seen = Array.make (nb_var +1) false in
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);
aux l
in
aux l;
(!one, to_list seen)
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 * (int list)
and type t = bool * S.t
= struct
type location = Std.Loc.t
type term = int
type t = bool * (int list)
type t = bool * S.t
let p_cnf ?loc nb_var _ =
let _ = loc in
false,[nb_var]
false, S.singleton nb_var
let clause ?loc l =
let _ = loc in
false,l
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
@@ -86,85 +61,141 @@ module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
let parse_file = fun x -> snd (M.parse_file x)
let stmt_to_string = print_list (fun (b,l) -> "("^(string_of_bool b)^","^print_list string_of_int l^")")
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 flatten nb_var trace (l : (bool * int list) list) =
let _ = nb_var in
let rec aux = function
| [] -> []
| (n,[])::l -> (n,[])::(aux 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 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
(List.map
(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 (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)));
trace := Buffer.contents buffer::!trace
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 (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 [] in
let l = statements |> List.map (positify nb_var) in
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*)
let model = Array.make (nb_var+1) false in
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
| [] ->
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;
model.(x) <- Some true;
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;
model.(x) <- Some false;
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
| (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)
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"