diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml index 1ab83ffd224fb5500f1dcc457d6374cb7c61cdae..c26417815e4001b0216718f96e7c9245737794b4 100644 --- a/CoAlgLogicUtils.ml +++ b/CoAlgLogicUtils.ml @@ -23,4 +23,57 @@ let disjointAgents sort a b = Array.iter f la; !res +(* Maximal Clique finding *) +(* Using algorithm implementation from + http://mancoosi.org/~abate/finding-maximal-cliques-and-independent-sets-undirected-graph-bron%E2%80%93kerbosch-algorithm + which implements http://en.wikipedia.org/wiki/Bron%E2%80%93Kerbosch_algorithm + *) + +module V = struct + type t = int + let compare = compare + let hash = Hashtbl.hash + let equal = (=) +end + +module UG = Persistent.Graph.Concrete(V) +module N = Oper.Neighbourhood(UG) +module S = N.Vertex_Set + +let rec bronKerbosch2 gr r p x = + let n v = N.set_from_vertex gr v in + if (S.is_empty p) && (S.is_empty x) then [r] + else + let u = S.choose (S.union p x) in + let (_,_,mxc) = + S.fold (fun v (p,x,acc) -> + let r' = S.union r (S.singleton v) in + let p' = S.inter p (n v) in + let x' = S.inter x (n v) in + (S.remove v p, S.add v x,(bronKerbosch2 gr r' p' x') @ acc) + ) (S.diff p (n u)) (p,x,[]) + in mxc + +(* thanks to stackoverflow for cartesian product of lists *) +let cartesian l l' = + List.concat (List.map (fun e -> List.map (fun e' -> (e,e')) l') l) + +let maxDisjoints sort (a: bset) : bset list = + let vl = bsetFold (fun x l -> (lfToInt x):: l) a [] in + let gr = List.fold_left (fun g v -> UG.add_vertex g v) UG.empty vl in + let edges = List.filter + (fun (x,y) -> disjointAgents sort (lfFromInt x) (lfFromInt y)) + (cartesian vl vl) + in + let gr = List.fold_left (fun g (x,y) -> UG.add_edge g x y) gr edges in + let r = S.empty in + let p = List.fold_right S.add vl S.empty in + let x = S.empty in + let intlist = bronKerbosch2 gr r p x in + let tmpf : bset -> int -> bset = + (fun bs f -> bsetAdd bs (lfFromInt f) ; bs) + in + List.map (List.fold_left tmpf (bsetMake ())) (List.map S.elements intlist) + + diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli index f0319a71fb34fde7d36db95803350ef436145484..747b5ef1155626e72f482b970e99d791fdb0d2a2 100644 --- a/CoAlgLogicUtils.mli +++ b/CoAlgLogicUtils.mli @@ -6,8 +6,9 @@ open CoAlgMisc -val disjointAgents : sort -> CoAlgMisc.localFormula -> CoAlgMisc.localFormula -> bool +val disjointAgents : sort -> localFormula -> localFormula -> bool +val maxDisjoints : sort -> bset -> bset list diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml index b95ee3410e2fafeaf015d333b02ac9a0daa63672..9671694788cc025abae7fac389d94d5d1b193003 100644 --- a/CoAlgLogics.ml +++ b/CoAlgLogics.ml @@ -179,21 +179,6 @@ let compatible sort (a: bset) formula1 = bsetIter f a; !res -(* -let maxDisjoints sort (a: bset) : bset list = - let f formula acc = - let g cc acc' = - if (compatible sort cc formula) - then let newcc = bsetCopy cc in - bsetAdd newcc formula; - (newcc)::acc' - else acc' - in - List.fold_right acc g acc - in - bsetFold a f [bsetMake ()] - *) - (* CoalitionLogic: tableau rules for satisfiability diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml index c3ec6e69a64ca3c1f4b47be9af874e7ddd3b2a57..a8e5d3083ed141b14b5053a0b9fcd5292d3756b8 100644 --- a/CoAlgMisc.ml +++ b/CoAlgMisc.ml @@ -488,6 +488,8 @@ let lfGetNeg sort f = if nf >= 0 then Some nf else None let lfGetAt (sort, nom) f = FHt.find !arrayAt.(sort).(f) nom +let lfToInt lf = lf +let lfFromInt num = num let atFormulaGetSubformula f = !arrayDest1.(0).(f) let atFormulaGetNominal f = diff --git a/CoAlgMisc.mli b/CoAlgMisc.mli index 1958b4fd3e58a14f0576c766070769494f18ecaf..51e86c5dff601ffc516ef4c44a7b3b7fa7aa9dc1 100644 --- a/CoAlgMisc.mli +++ b/CoAlgMisc.mli @@ -276,6 +276,8 @@ val lfGetDest3 : sort -> localFormula -> int val lfGetDestAg : sort -> localFormula -> int array val lfGetNeg : sort -> localFormula -> localFormula option val lfGetAt : nominal -> localFormula -> atFormula +val lfToInt : localFormula -> int +val lfFromInt : int -> localFormula val atFormulaGetSubformula : atFormula -> localFormula val atFormulaGetNominal : atFormula -> nominal