Skip to content
Snippets Groups Projects

Resolve "add horn sat algorithm"

Merged aalbert requested to merge 5-add-horn-sat-algorithm into main
Compare and Show latest version
1 file
+ 67
5
Compare changes
  • Side-by-side
  • Inline
+ 67
5
@@ -63,6 +63,58 @@ let print_list print 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 remove_xor form = match form with
| Xor (a, b) -> 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)
| _ -> form
let rec to_cnf = function
| Neg (Var i) -> Var (-i)
| Neg (And (a,b)) -> to_cnf (Or(to_cnf (Neg a), to_cnf (Neg b)))
| Neg (Or (a,b)) -> And(to_cnf (Neg a), to_cnf (Neg b))
| Or (And (a,b), c) -> And (to_cnf (Or (a,c)), to_cnf (Or(b,c)))
| Or (c,And (a,b)) -> And (to_cnf (Or (a,c)), to_cnf (Or(b,c)))
| And (a,b) -> And (to_cnf a, to_cnf b)
| Or (a,b) -> to_cnf (Or (to_cnf a, to_cnf 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
@@ -77,23 +129,33 @@ 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
and type t = int list list
= struct
type location = Std.Loc.t
type term = int
type t = int list
type t = int list list
let p_cnf ?loc nb_var nb_clause =
let _ = loc in
[nb_var; nb_clause]
[[nb_var; nb_clause]]
let clause ?loc l =
let _ = loc in
l
cnf_to_int_list (to_cnf (List.fold_left (fun form x -> Xor (form,Var x)) (Var (List.hd l)) (List.tl l)))
end
module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
module S = Set.Make(struct type t = int let compare = compare end)
let convert_xorsat file =
match snd (M.parse_file file) with
| [[nb_var; nb_clause]] :: statements ->
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 "\n"
) (List.concat statements);
close_out oc
| _ -> failwith "cannot happen"
Loading