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
+ 114
− 146
Compare changes
  • Side-by-side
  • Inline
Files
2
project1/bin/xor.ml
+ 113
− 145
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. *)
(* 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,17 +25,51 @@ module Term : Dolmen_dimacs.Term
end
let to_list arr =
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
false, S.of_list l
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
let to_model arr =
(* convert an array into a SAT model *)
let to_model arr =
let res = ref [] in
for i = 1 to Array.length arr - 1 do
if arr.(i) then
if arr.(i) then
res := i::!res
else
res := (-i)::!res
@@ -45,153 +78,88 @@ let to_model arr =
(* 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 positify (b, s) =
let b2 = ref b in
let s2 = S.map (
fun x ->
if x<0 then b2 := not !b2;
abs x
) s
in
(!b2, s2)
(* 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 resolve model (b, s) =
let b2 = ref b in
let s2 = S.filter (fun x -> if model.(x) then (b2 := not !b2; false) else true) s in
if !b2 then true
else (
match S.choose_opt s2 with
| Some(x) -> model.(x) <- true; true
| None -> false
)
let get_result trace model (l : (bool * S.t) list) =
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);
| [] -> true
| (false, s)::_ when S.cardinal s = 0 -> false
| (true, s)::l when S.cardinal s = 0 -> aux l
| [cl] -> resolve model cl
| (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) <- true;
aux l
in
aux l;
(!one, to_list seen)
| (false, 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;
aux (List.map (fun (b, s2) -> (b, S.remove x s2)) l)
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)
= struct
| (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;
type location = Std.Loc.t
type term = int
type t = bool * (int list)
aux (List.map (fun (b2, s2) -> positify (b <> b2, S.union s_x (S.remove x s2))) l)
| None -> resolve model (b, s) && aux l
end
let p_cnf ?loc nb_var _ =
let _ = loc in
false,[nb_var]
in aux l
let clause ?loc l =
let _ = loc in
false,l
end
let process = function
| (_,hd)::tl ->
module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
let nb_var = S.choose hd in
let trace : string list ref = ref []
and s = List.map positify tl
and model = Array.make (nb_var+1) false in
let parse_file = fun x -> snd (M.parse_file x)
trace :=
("Formula to test:\n"^(stmt_to_string tl)^
"\nPositified formula:\n"^(stmt_to_string s)) :: !trace;
let stmt_to_string = print_list (fun (b,l) -> "("^(string_of_bool b)^","^print_list string_of_int l^")")
if get_result trace model s
then Ok(model |> to_model, !trace)
else Error(!trace)
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 b then
(b,[x])::(List.map
(fun (b,l) -> (b,List.filter (fun y -> x <> y) l))
(aux l))
else
(b,[x])::(aux l)
| (b,h::not_t)::l -> (
let foo =
aux
(List.map
(fun (n,x) ->
positify nb_var
((if b then n else if List.mem h x then not n else 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;
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 ["Formula to test :"] in
trace := (stmt_to_string statements)::!trace;
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;
(*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 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)
| _ -> failwith "cannot happen"