### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / FuzzyALCReasoner.ml @ fa1727d2

 1 ```(* ``` ``` * vim: ts=2 sw=2 ``` ``` *) ``` ```(* ``` ``` * This module implements the Lukasiewicz Fuzzy ``` ``` * ALC reasoner described in ``` ``` * http://ijcai.org/papers13/Papers/IJCAI13-147.pdf ``` ``` *) ``` ```open FuzzyALCABox ``` ```open Hashtbl ``` ```open Glpk ``` ```open HashConsing ``` ```let outputDebug s = () (*print_endline s*) ``` ```(* ``` ``` * We use two different forms for storing inequalities in this ``` ``` * module: First, the basic ``` ``` * (asst List) * int * (asst List) ``` ``` * where both sides are multisets of inequalities, represented as ``` ``` * lists, and second, during the solving process, ``` ``` * the ABox is saved in a map mapping ``` ``` * (AsstMultiSet.t * int * AsstMultiSet.t) to int ``` ``` * where the value is an integer that signals different flags relevant ``` ``` * to the solver routine and the key is the actual inequality, ``` ``` * using the AsstMultiSet documented below. ``` ``` *) ``` ```(* ``` ``` * Maps assertion to coefficient. Used as building block ``` ``` * to implement a multiset. ``` ``` *) ``` ```module AsstMap = Map.Make( ``` ``` struct ``` ``` type t = hcAsst ``` ``` let compare = compare ``` ``` (* If hash-consing works, then... *) ``` ``` (* ``` ``` let compare l r = ``` ``` match (l, r) with ``` ``` | (HCROLE(a1, b1, c1), HCROLE(a2, b2, c2)) -> ``` ``` if a1 != a2 then a1 - a2 ``` ``` else if b1 != b2 then b1 - b2 ``` ``` else if c1 != c2 then compare c1 c2 ``` ``` else 0 ``` ``` | (HCCONCEPT(a1, c1), HCCONCEPT(a2, c2)) -> ``` ``` if a1 != a2 then a1 - a2 ``` ``` else if c1 != c2 then compare c1 c2 ``` ``` else 0 ``` ``` | (HCROLE(_, _, _), _) -> -1 ``` ``` | (HCCONCEPT(_, _), _) -> +1 ``` ``` *) ``` ``` end ``` ```) ``` ```(* ``` ``` * Implements a multiset of assertions. Provides a subset ``` ``` * of the normal set operations, with changed semantics: ``` ``` * Each element might exist multiple times in the multiset. ``` ``` * Iterating over a multiset might call the iterator function ``` ``` * multiple times for the same element, if it exists more than ``` ``` * once in the set. ``` ``` *) ``` ```module AsstMultiSet = ``` ``` struct ``` ``` type t = int AsstMap.t ``` ``` let empty = AsstMap.empty ``` ``` let compare a b = ``` ``` AsstMap.compare (fun x y -> x - y) a b ``` ``` let equal a b = ``` ``` AsstMap.equal (fun x y -> x == y) a b ``` ``` let add value t = ``` ``` if not (AsstMap.mem value t) then ``` ``` AsstMap.add value 1 t ``` ``` else ``` ``` AsstMap.add value ((AsstMap.find value t) + 1) t ``` ``` let remove value t = ``` ``` let old = AsstMap.find value t in ``` ``` if old = 1 then ``` ``` AsstMap.remove value t ``` ``` else ``` ``` AsstMap.add value (old - 1) t ``` ``` let iter f t = ``` ``` let iter_f key value = ``` ``` for i = 1 to value do ``` ``` f key ``` ``` done ``` ``` in ``` ``` AsstMap.iter iter_f t ``` ``` let for_all f t = ``` ``` AsstMap.for_all (fun key value -> f key) t ``` ``` let fold f t b = ``` ``` let foldN key value bb = ``` ``` if value = 0 then bb ``` ``` else ( ``` ``` let ret = ref bb in ``` ``` for i = 1 to value do ``` ``` ret := f key !ret ``` ``` done; ``` ``` !ret ``` ``` ) ``` ``` in ``` ``` AsstMap.fold foldN t b ``` ``` end ``` ```type inequality = AsstMultiSet.t * int * AsstMultiSet.t ``` ```(* ``` ``` * Flags associated with the inequalities while they are ``` ``` * being mangled by the solver. These will be expanded in ``` ``` * the future. Currently, the only flag signals whether ``` ``` * the (\exists L) rule has already be applied to this ``` ``` * inequality. ``` ``` *) ``` ```let emptyFlags = 0 ``` ```let addExistsLeft i = i lor 1 ``` ```let checkExistLeft i = (i land 1) > 0 ``` ```(* ``` ``` * A map used for storing the ABoxes in memory. ``` ``` * Maps the inequalities in the set to their flags ``` ``` * (ABoxes are _sets_ of inequalities) ``` ``` *) ``` ```module InequalitySet = Map.Make( ``` ``` struct ``` ``` type t = inequality ``` ``` let compare = compare ``` ``` let compare (l1, g1, r1) (l2, g2, r2) = ``` ``` if g1 != g2 then g1 - g2 ``` ``` else if not (AsstMultiSet.equal l1 l2) then AsstMultiSet.compare l1 l2 ``` ``` else if not (AsstMultiSet.equal r1 r2) then AsstMultiSet.compare r1 r2 ``` ``` else 0 ``` ``` end ``` ```) ``` ```(* ``` ``` * Converts from AsstMultiSet to list representation ``` ``` *) ``` ```let toAssertion ((lefts : AsstMultiSet.t), (gr : int), (rights : AsstMultiSet.t)) = ``` ``` let left = ref [] in ``` ``` let right = ref [] in ``` ``` let iter ret asst = ``` ``` ret := (toAsst asst)::(!ret) ``` ``` in ``` ``` AsstMultiSet.iter (iter left) lefts; ``` ``` AsstMultiSet.iter (iter right) rights; ``` ``` (!left, gr, !right) ``` ```(* ``` ``` * For debug reasons: Prints ABox to stdout ``` ``` *) ``` ```let printABox hcInput = ``` ``` outputDebug "-------------"; ``` ``` InequalitySet.iter (fun k flags -> outputDebug (printAssertion (toAssertion k))) !hcInput; ``` ``` outputDebug "-------------" ``` ```(* ``` ``` * Checks whether an inequality consists of atomic assertions only. ``` ``` * ``` ``` * We also consider inequalities atomic that have (TODO: explain \exist R-problems) ``` ``` *) ``` ```let nodeAtomic (left, gr, right) = ``` ``` let asstAtomic s ignoreExists = ``` ``` let f x = ``` ``` match x with ``` ``` | HCCONCEPT (_, y) -> ``` ``` (match y.fml with ``` ``` | AP(_) -> true ``` ``` | EXISTS(_, _) when ignoreExists -> true ``` ``` | _ -> false) ``` ``` | HCROLE (_, _, _) -> true ``` ``` in ``` ``` AsstMultiSet.for_all f s ``` ``` in ``` ``` asstAtomic left false && asstAtomic right true ``` ```let maxrole = ref (0) ``` ```let max (a : int) (b : int) = ``` ``` if a > b then a else b ``` ```let freshIndividual = ``` ``` maxrole := (!maxrole) + 1; ``` ``` !maxrole ``` ```exception InternalReasonerError of string ``` ```let lpSolve assertions n = ``` ``` (* n = Number of variables in LP problem *) ``` ``` (* Coefficients of function being optimized. As we ``` ``` * only care for satisfiability of the LP problem, not ``` ``` * for an optimum, set them to 0. *) ``` ``` let coeff = Array.make n 0. in ``` ``` let matrix = Array.make_matrix (List.length assertions) n 0. in ``` ``` (* Auxiliary variables, i.e. row variables. ``` ``` * All rows will be of the form a + b - c - d + X > 0 *) ``` ``` let auxbound = Array.make (List.length assertions) (0., infinity) in ``` ``` (* Original variables, i.e. column variables *) ``` ``` let origbound = Array.make n (0., 1.) in ``` ``` (* Iterate over all rows and fill linear problem *) ``` ``` let f i (gr, left, right) = ``` ``` Array.set auxbound i (0.001 -. (float_of_int gr), infinity); ``` ``` (* Iterate over this row *) ``` ``` let g fac asstID = ``` ``` (*outputDebug ("Setting asstID " ^ string_of_int(asstID));*) ``` ``` let currow = Array.get matrix i in ``` ``` let newval = (Array.get currow asstID) +. fac in ``` ``` Array.set currow asstID newval ``` ``` in ``` ``` (*outputDebug (string_of_int i);*) ``` ``` List.iter (g 1.) left; ``` ``` List.iter (g ~-.1.) right; ``` ``` i+1; ``` ``` in ``` ``` (* XXX *) ``` ``` if n == 0 then ( ``` ``` outputDebug "Empty LP problem! (Not satisfiable)"; ``` ``` false ``` ``` ) else ( ``` ``` outputDebug ("Building LP problem for " ^ string_of_int (List.length assertions) ^ " ABox inequalities" ^ " and " ^ string_of_int n ^ " variables."); ``` ``` List.fold_left f 0 assertions; ``` ``` (*outputDebug "Solving!";*) ``` ``` let lp = make_problem Maximize coeff matrix auxbound origbound in ``` ``` simplex lp; ``` ``` if get_status lp then outputDebug "Satisfiable ABox!" ``` ``` else outputDebug "Unsatisfiable ABox!"; ``` ``` get_status lp ``` ``` ) ``` ```let rec ruleClash hcF input = ``` ``` let conceptIdTable = Hashtbl.create 3 in ``` ``` let roleIdTable = Hashtbl.create 3 in ``` ``` let counter = ref 0 in ``` ``` let getConceptId i s = ``` ``` (*outputDebug ("Finding ID for concept: " ^ (string_of_int i) ^ ", " ^ s);*) ``` ``` try Hashtbl.find conceptIdTable (i, s) ``` ``` with Not_found -> ``` ``` let x = !counter in ``` ``` incr counter; ``` ``` Hashtbl.add conceptIdTable (i, s) x; ``` ``` x; ``` ``` in ``` ``` let getRoleId i1 i2 s = ``` ``` (*outputDebug ("Finding ID for role: " ^ string_of_int(i1) ^ ", " ^ string_of_int(i2) ^ ", " ^ string_of_int(s));*) ``` ``` try Hashtbl.find roleIdTable (i1, i2, s) ``` ``` with Not_found -> ``` ``` let x = !counter in ``` ``` incr counter; ``` ``` Hashtbl.add roleIdTable (i1, i2, s) x; ``` ``` x; ``` ``` in ``` ``` let getAssts x ret = ``` ``` match x with ``` ``` | HCROLE(i1, i2, s) -> (getRoleId i1 i2 s)::ret ``` ``` | HCCONCEPT(i, {fml = AP(s)}) -> (getConceptId i s)::ret ``` ``` | HCCONCEPT(i, {fml = EXISTS(_, _)}) -> ret ``` ``` | _ -> raise (InternalReasonerError "Invalid assertion given to getAssts") ``` ``` in ``` ``` let f (left, gr, right) value ret = ``` ``` (gr, AsstMultiSet.fold getAssts left [], AsstMultiSet.fold getAssts right [])::ret ``` ``` in ``` ``` (* Filter out atomic assertions in this ABox and map them to linear inequalities *) ``` ``` let atomics = InequalitySet.filter (fun key value -> nodeAtomic key) input in ``` ``` lpSolve (InequalitySet.fold f atomics []) !counter ``` ```let addInequality ref changed ineq flags = ``` ``` if not (InequalitySet.mem ineq !ref) then ( ``` ``` ref := InequalitySet.add ineq flags !ref; ``` ``` changed := true) ``` ```(************************************************************ ``` ``` * non-branching rules. We can always apply them ``` ``` ************************************************************) ``` ```(* ``` ``` * Applies negation elimination to both sides of the ``` ``` * inequality, left and right ``` ``` *) ``` ```let rec ruleNeg hcF ret changed = ``` ``` let iter ((left, gr, right) as ineq) flags = ``` ``` let iter_asst_left hcasst = ``` ``` match hcasst with ``` ``` | HCCONCEPT(a, {fml = NOT(y); _}) -> ``` ``` (*ret := InequalitySet.remove ineq !ret;*) ``` ``` addInequality ret changed (AsstMultiSet.remove hcasst left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) right) emptyFlags; ``` ``` | _ -> () ``` ``` in ``` ``` let iter_asst_right hcasst = ``` ``` match hcasst with ``` ``` | HCCONCEPT(a, {fml = NOT(y); _}) -> ``` ``` (*ret := InequalitySet.remove ineq !ret;*) ``` ``` addInequality ret changed (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) left, gr-1, AsstMultiSet.remove hcasst right) emptyFlags; ``` ``` | _ -> () ``` ``` in ``` ``` AsstMultiSet.iter iter_asst_left left; ``` ``` AsstMultiSet.iter iter_asst_right right; ``` ``` in ``` ``` InequalitySet.iter iter !ret ``` ```let rec ruleAndRight hcF ret changed = ``` ``` let iter (left, gr, right) flags = ``` ``` let f elem = ``` ``` match elem with ``` ``` | HCCONCEPT(a, {fml = AND(x, y); _}) -> ``` ``` let nr = AsstMultiSet.remove elem right in ``` ``` addInequality ret changed (left, gr, nr) emptyFlags; ``` ``` addInequality ret changed (left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) nr)) emptyFlags; ``` ``` | _ -> (); ``` ``` in ``` ``` AsstMultiSet.iter f right; ``` ``` in ``` ``` InequalitySet.iter iter !ret ``` ```let rec ruleExistsRight hcF ret changed = ``` ``` (* ``` ``` * We have to find pairs of inequalities. Iterate over all inequalities ``` ``` * two times (quadratic). First, find an inequality with a assertion ``` ``` * a:\exists R.C on the right side, then an inequality with a matching ``` ``` * role assertion on the left side. ``` ``` *) ``` ``` (* This function looks for (a,b):R on the left side and returns a list of ``` ``` * matching individuals b *) ``` ``` let fold1 na excl ((left, gr, right) as ineq) flags l1 = ``` ``` let f elem l2 = ``` ``` match elem with ``` ``` | HCROLE(a, b, c) when a = na -> ``` ``` b :: l2 ``` ``` | _ -> l2 ``` ``` in ``` ``` if excl == ineq then l1 ``` ``` else AsstMultiSet.fold f left l1 ``` ``` in ``` ``` (* This function looks for a:\exists R.C on the right side *) ``` ``` let iter1 ((left, gr, right) as ineq) flags = ``` ``` (* Find pairs of inequalities *) ``` ``` let f elem = ``` ``` match elem with ``` ``` (* Candidate for first inequality *) ``` ``` | HCCONCEPT(a, {fml = EXISTS(x, c)}) as r -> ``` ``` (* Get list of candidates for b *) ``` ``` let bs = InequalitySet.fold (fold1 a ineq) !ret [] in ``` ``` if List.length bs != 0 then ( ``` ``` addInequality ret changed (left, gr, AsstMultiSet.remove r right) emptyFlags; ``` ``` let addf () b = ``` ``` addInequality ret changed (left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(b, c))) (AsstMultiSet.add (toHcAsst hcF (ROLE(a, b, x))) (AsstMultiSet.remove r right))) emptyFlags ``` ``` in ``` ``` List.fold_left addf () bs; ``` ``` ) else ``` ``` (); ``` ``` | _ -> (); ``` ``` in ``` ``` AsstMultiSet.iter f right; ``` ``` in ``` ``` InequalitySet.iter iter1 !ret ``` ```(************************************************************* ``` ``` * Solver loop and branching rules (mutually recursive ``` ``` * with main solver routine) ``` ``` *************************************************************) ``` ```let rec internalSolve hcF input = ``` ``` let hcInput = ref input in ``` ``` let changed = ref true in ``` ``` outputDebug "Starting new branch with ABox:"; ``` ``` printABox hcInput; ``` ``` while !changed do ``` ``` changed := false; ``` ``` ruleNeg hcF hcInput changed; ``` ``` ruleAndRight hcF hcInput changed; ``` ``` ruleExistsRight hcF hcInput changed; ``` ``` printABox hcInput; ``` ``` outputDebug("Non-branching rules applied. Number of inequalities in result: " ^ string_of_int (InequalitySet.cardinal !hcInput)) ``` ``` done; ``` ``` outputDebug "No further linear expansion possible. Checking for branches."; ``` ``` (* XXX *) ``` ``` let ok = ref false in ``` ``` changed := false; ``` ``` ok := ruleExistsLeft hcF hcInput changed; ``` ``` if !changed then !ok else ( ``` ``` ok := ruleAndLeft hcF hcInput changed; ``` ``` if !changed then !ok else ( ``` ``` outputDebug("No branches possible. Checking if ABox clashes."); ``` ``` printABox hcInput; ``` ``` ruleClash hcF !hcInput ``` ``` ) ``` ``` ) ``` ```(************************************************************* ``` ``` * Branching rules ``` ``` * (They call the "internalSolve" function recursively) ``` ``` *************************************************************) ``` ```and ruleExistsLeft hcF ret changed = ``` ``` let ok = ref false in ``` ``` let iter ((left, gr, right) as ineq) flags = ``` ``` let f elem = ``` ``` match elem with ``` ``` (* ``` ``` * This rule may only be applied once to an inequality, successful ``` ``` * application is recorded in the flags field ``` ``` *) ``` ``` | HCCONCEPT(a, {fml = EXISTS(x, y); _}) when not (checkExistLeft flags) -> ``` ``` let nl = AsstMultiSet.remove elem left in ``` ``` let branch1 = (nl, gr, right) in ``` ``` let indiv = freshIndividual in ``` ``` let branch2 = (AsstMultiSet.add (toHcAsst hcF (ROLE(a, indiv, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(indiv, y))) nl), gr-1, right) in ``` ``` if (not (InequalitySet.mem branch1 !ret)) && (not (InequalitySet.mem branch2 !ret)) then ``` ``` ( ``` ``` changed := true; ``` ``` (* Override previous flags for the premiss *) ``` ``` ret := InequalitySet.add ineq (addExistsLeft flags) !ret; ``` ``` ok := !ok || ``` ``` internalSolve hcF (InequalitySet.add branch1 emptyFlags !ret) || ``` ``` internalSolve hcF (InequalitySet.add branch2 emptyFlags !ret); ``` ``` ) ``` ``` else ``` ``` () ``` ``` | _ -> (); ``` ``` in ``` ``` AsstMultiSet.iter f left; ``` ``` in ``` ``` InequalitySet.iter iter !ret; ``` ``` !ok ``` ```and ruleAndLeft hcF ret changed = ``` ``` let ok = ref false in ``` ``` let iter (left, gr, right) flags = ``` ``` let f elem = ``` ``` match elem with ``` ``` | HCCONCEPT(a, {fml = AND(x, y); _}) as con -> ``` ``` let nl = AsstMultiSet.remove elem left in ``` ``` let branch1 = (nl, gr, right) in ``` ``` let branch2 = (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) (AsstMultiSet.remove con left)), gr-1, right) in ``` ``` if (not (InequalitySet.mem branch1 !ret)) && (not (InequalitySet.mem branch2 !ret)) then ``` ``` ( ``` ``` changed := true; ``` ``` ok := !ok || ``` ``` internalSolve hcF (InequalitySet.add branch1 emptyFlags !ret) || ``` ``` internalSolve hcF (InequalitySet.add branch2 emptyFlags !ret); ``` ``` ) ``` ``` else ``` ``` () ``` ``` | _ -> (); ``` ``` in ``` ``` AsstMultiSet.iter f left; ``` ``` in ``` ``` InequalitySet.iter iter !ret; ``` ``` !ok ``` ```let rec fuzzyALCsat input = ``` ``` (* Create new HashCons table. Formulas don't have negation forms. *) ``` ``` let hcF = HcFormula.create false in ``` ``` (* Convert input formulae to hash-consed representation *) ``` ``` maxrole := (-1); ``` ``` let f ss (left, gr, right) = ``` ``` let g s asst = ``` ``` match asst with ``` ``` | ROLE(a, b, c) -> ``` ``` maxrole := max !maxrole (max a b); ``` ``` AsstMultiSet.add (HCROLE(a, b, c)) s ``` ``` | CONCEPT(a, c) -> ``` ``` maxrole := max !maxrole a; ``` ``` AsstMultiSet.add (HCCONCEPT(a, hc_formula hcF c)) s ``` ``` in ``` ``` InequalitySet.add (List.fold_left g AsstMultiSet.empty left, gr, List.fold_left g AsstMultiSet.empty right) emptyFlags ss ``` ``` in ``` ``` internalSolve hcF (List.fold_left f InequalitySet.empty input) ```