Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / FuzzyALCReasoner.ml @ 48a72851

History | View | Annotate | Download (15.2 KB)

1
(*
2
 * vim: ts=2 sw=2
3
 *)
4

    
5
(*
6
 * This module implements the Lukasiewicz Fuzzy
7
 * ALC reasoner described in
8
 * http://ijcai.org/papers13/Papers/IJCAI13-147.pdf
9
 *)
10

    
11
open FuzzyALCABox
12
open Hashtbl
13
open Glpk
14
open HashConsing
15

    
16
let outputDebug s = () (*print_endline s*)
17

    
18
(*
19
 * We use two different forms for storing inequalities in this
20
 * module: First, the basic
21
 * (asst List) * int * (asst List)
22
 * where both sides are multisets of inequalities, represented as
23
 * lists, and second, during the solving process,
24
 * the ABox is saved in a map mapping
25
 * (AsstMultiSet.t * int * AsstMultiSet.t) to int
26
 * where the value is an integer that signals different flags relevant
27
 * to the solver routine and the key is the actual inequality,
28
 * using the AsstMultiSet documented below.
29
 *)
30

    
31
(*
32
 * Maps assertion to coefficient. Used as building block
33
 * to implement a multiset.
34
 *)
35
module AsstMap = Map.Make(
36
  struct
37
    type t = hcAsst
38
    let compare = compare
39
    (* If hash-consing works, then... *)
40
    (*
41
    let compare l r =
42
      match (l, r) with
43
      | (HCROLE(a1, b1, c1), HCROLE(a2, b2, c2)) ->
44
          if a1 != a2 then a1 - a2
45
          else if b1 != b2 then b1 - b2
46
          else if c1 != c2 then compare c1 c2
47
          else 0
48
      | (HCCONCEPT(a1, c1), HCCONCEPT(a2, c2)) ->
49
          if a1 != a2 then a1 - a2
50
          else if c1 != c2 then compare c1 c2
51
          else 0
52
      | (HCROLE(_, _, _), _) -> -1
53
      | (HCCONCEPT(_, _), _) -> +1
54
    *)
55
  end
56
)
57

    
58
(*
59
 * Implements a multiset of assertions. Provides a subset
60
 * of the normal set operations, with changed semantics:
61
 * Each element might exist multiple times in the multiset.
62
 * Iterating over a multiset might call the iterator function
63
 * multiple times for the same element, if it exists more than
64
 * once in the set.
65
 *)
66
module AsstMultiSet =
67
  struct
68
    type t = int AsstMap.t
69
    let empty = AsstMap.empty
70
    let compare a b =
71
      AsstMap.compare (fun x y -> x - y) a b
72
    let equal a b =
73
      AsstMap.equal (fun x y -> x == y) a b
74

    
75
    let add value t =
76
      if not (AsstMap.mem value t) then
77
        AsstMap.add value 1 t
78
      else
79
        AsstMap.add value ((AsstMap.find value t) + 1) t
80

    
81
    let remove value t =
82
      let old = AsstMap.find value t in
83
      if old = 1 then
84
        AsstMap.remove value t
85
      else
86
        AsstMap.add value (old - 1) t
87

    
88
    let iter f t =
89
      let iter_f key value =
90
        for i = 1 to value do
91
          f key
92
        done
93
      in
94
      AsstMap.iter iter_f t
95

    
96
    let for_all f t =
97
      AsstMap.for_all (fun key value -> f key) t
98

    
99
    let fold f t b =
100
      let foldN key value bb =
101
        if value = 0 then bb
102
        else (
103
          let ret = ref bb in
104
          for i = 1 to value do
105
            ret := f key !ret
106
          done;
107
          !ret
108
        )
109
      in
110
      AsstMap.fold foldN t b
111
  end
112

    
113
type inequality = AsstMultiSet.t * int * AsstMultiSet.t
114
(*
115
 * Flags associated with the inequalities while they are
116
 * being mangled by the solver. These will be expanded in
117
 * the future. Currently, the only flag signals whether
118
 * the (\exists L) rule has already be applied to this
119
 * inequality.
120
 *)
121
let emptyFlags = 0
122
let addExistsLeft i = i lor 1
123
let checkExistLeft i = (i land 1) > 0
124
(* 
125
 * A map used for storing the ABoxes in memory.
126
 * Maps the inequalities in the set to their flags
127
 * (ABoxes are _sets_ of inequalities)
128
 *)
129
module InequalitySet = Map.Make(
130
  struct
131
    type t = inequality
132
    let compare = compare
133
    let compare (l1, g1, r1) (l2, g2, r2) =
134
      if g1 != g2 then g1 - g2
135
      else if not (AsstMultiSet.equal l1 l2) then AsstMultiSet.compare l1 l2
136
      else if not (AsstMultiSet.equal r1 r2) then AsstMultiSet.compare r1 r2
137
      else 0
138
  end
139
)
140

    
141
(*
142
 * Converts from AsstMultiSet to list representation
143
 *)
144
let toAssertion ((lefts : AsstMultiSet.t), (gr : int), (rights : AsstMultiSet.t)) =
145
  let left = ref [] in
146
  let right = ref [] in
147
  let iter ret asst =
148
    ret := (toAsst asst)::(!ret)
149
  in
150
  AsstMultiSet.iter (iter left) lefts;
151
  AsstMultiSet.iter (iter right) rights;
152
  (!left, gr, !right)
153

    
154
(*
155
 * Checks whether an inequality consists of atomic assertions only.
156
 *
157
 * We also consider inequalities atomic that have (TODO: explain \exist R-problems)
158
 *)
159
let nodeAtomic (left, gr, right) =
160
  let asstAtomic s ignoreExists =
161
    let f x =
162
      match x with
163
      | HCCONCEPT (_, y) ->
164
          (match y.fml with
165
          | AP(_) -> true
166
          | EXISTS(_, _) when ignoreExists -> true
167
          | _ -> false)
168
      | HCROLE (_, _, _) -> true
169
    in
170
    AsstMultiSet.for_all f s
171
  in
172
  asstAtomic left false && asstAtomic right true
173

    
174
let maxrole = ref (0)
175

    
176
let freshIndividual =
177
  maxrole := (!maxrole) + 1;
178
  !maxrole
179

    
180
exception InternalReasonerError of string
181

    
182
let lpSolve assertions n =
183
  (* n = Number of variables in LP problem *)
184
  (* Coefficients of function being optimized. As we
185
   * only care for satisfiability of the LP problem, not
186
   * for an optimum, set them to 0. *)
187
  let coeff = Array.make n 0. in
188
  let matrix = Array.make_matrix (List.length assertions) n 0. in
189
  (* Auxiliary variables, i.e. row variables.
190
   * All rows will be of the form a + b - c - d + X > 0 *)
191
  let auxbound = Array.make (List.length assertions) (0., infinity) in
192
  (* Original variables, i.e. column variables *)
193
  let origbound = Array.make n (0., 1.) in
194
  (* Iterate over all rows and fill linear problem *)
195
  let f i (gr, left, right) =
196
    Array.set auxbound i (0.001 -. (float_of_int gr), infinity);
197
    (* Iterate over this row *)
198
    let g fac asstID =
199
      (*outputDebug ("Setting asstID " ^ string_of_int(asstID));*)
200
      let currow = Array.get matrix i in
201
      let newval = (Array.get currow asstID) +. fac in
202
      Array.set currow asstID newval
203
    in
204
    (*outputDebug (string_of_int i);*)
205
    List.iter (g    1.)  left;
206
    List.iter (g ~-.1.) right;
207
    i+1;
208
  in
209
  (* XXX *)
210
  if n == 0 then (
211
    outputDebug "Empty LP problem! (Not satisfiable)";
212
      false
213
  ) else (
214
    outputDebug ("Building LP problem for " ^ string_of_int (List.length assertions) ^ " ABox inequalities" ^ " and " ^ string_of_int n ^ " variables.");
215
    List.fold_left f 0 assertions;
216
    (*outputDebug "Solving!";*)
217
    let lp = make_problem Maximize coeff matrix auxbound origbound in
218
    simplex lp;
219
    if get_status lp then outputDebug "Satisfiable ABox!"
220
    else outputDebug "Unsatisfiable ABox!";
221
    get_status lp
222
  )
223

    
224
let rec ruleClash hcF input =
225
  let conceptIdTable = Hashtbl.create 3 in
226
  let roleIdTable = Hashtbl.create 3 in
227
  let counter = ref 0 in
228
  let getConceptId i s =
229
    (*outputDebug ("Finding ID for concept: " ^ (string_of_int i) ^ ", " ^ s);*)
230
    try Hashtbl.find conceptIdTable (i, s)
231
    with Not_found ->
232
      let x = !counter in
233
      incr counter;
234
      Hashtbl.add conceptIdTable (i, s) x;
235
      x;
236
  in
237
  let getRoleId i1 i2 s =
238
    (*outputDebug ("Finding ID for role: " ^ string_of_int(i1) ^ ", " ^ string_of_int(i2) ^ ", " ^ string_of_int(s));*)
239
    try Hashtbl.find roleIdTable (i1, i2, s)
240
    with Not_found ->
241
      let x = !counter in
242
      incr counter;
243
      Hashtbl.add roleIdTable (i1, i2, s) x;
244
      x;
245
  in
246
  let getAssts x ret =
247
    match x with
248
    | HCROLE(i1, i2, s) -> (getRoleId i1 i2 s)::ret
249
    | HCCONCEPT(i, {fml = AP(s)}) -> (getConceptId i s)::ret
250
    | HCCONCEPT(i, {fml = EXISTS(_, _)}) -> ret
251
    | _ -> raise (InternalReasonerError "Invalid assertion given to getAssts")
252
  in
253
  let f (left, gr, right) value ret =
254
    (gr, AsstMultiSet.fold getAssts left [], AsstMultiSet.fold getAssts right [])::ret
255
  in
256
  (* Filter out atomic assertions in this ABox and map them to linear inequalities *)
257
  let atomics = InequalitySet.filter (fun key value -> nodeAtomic key) input in
258
  lpSolve (InequalitySet.fold f atomics []) !counter
259

    
260
let addInequality ref changed ineq flags =
261
  if not (InequalitySet.mem ineq !ref) then (
262
    ref := InequalitySet.add ineq flags !ref;
263
    changed := true)
264

    
265
(************************************************************
266
 * non-branching rules. We can always apply them
267
 ************************************************************)
268

    
269
(*
270
 * Applies negation elimination to both sides of the
271
 * inequality, left and right
272
 *)
273
let rec ruleNeg hcF ret changed =
274
  let iter ((left, gr, right) as ineq) flags =
275
    let iter_asst_left hcasst =
276
      match hcasst with
277
      | HCCONCEPT(a, {fml = NOT(y); _}) ->
278
          (*ret := InequalitySet.remove ineq !ret;*)
279
          addInequality ret changed (AsstMultiSet.remove hcasst left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) right) emptyFlags;
280
      | _ -> ()
281
    in
282
    let iter_asst_right hcasst =
283
      match hcasst with
284
      | HCCONCEPT(a, {fml = NOT(y); _}) ->
285
          (*ret := InequalitySet.remove ineq !ret;*)
286
          addInequality ret changed (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) left, gr-1, AsstMultiSet.remove hcasst right) emptyFlags;
287
      | _ -> ()
288
    in
289
    AsstMultiSet.iter iter_asst_left left;
290
    AsstMultiSet.iter iter_asst_right right;
291
  in
292
  InequalitySet.iter iter !ret
293

    
294
let rec ruleAndRight hcF ret changed =
295
  let iter (left, gr, right) flags =
296
    let f elem =
297
      match elem with
298
      | HCCONCEPT(a, {fml = AND(x, y); _}) ->
299
          let nr = AsstMultiSet.remove elem right in
300
          addInequality ret changed (left, gr, nr) emptyFlags;
301
          addInequality ret changed (left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) nr)) emptyFlags;
302
      | _ -> ();
303
    in
304
    AsstMultiSet.iter f right;
305
  in
306
  InequalitySet.iter iter !ret
307

    
308
let rec ruleExistsRight hcF ret changed =
309
  (*
310
   * We have to find pairs of inequalities. Iterate over all inequalities
311
   * two times (quadratic). First, find an inequality with a assertion
312
   * a:\exists R.C on the right side, then an inequality with a matching
313
   * role assertion on the left side.
314
   *)
315
  (* This function looks for (a,b):R on the left side and returns a list of
316
   * matching individuals b *)
317
  let fold1 na excl ((left, gr, right) as ineq) flags l1 =
318
    let f elem l2 =
319
      match elem with
320
      | HCROLE(a, b, c) when a = na ->
321
          b :: l2
322
      | _ -> l2
323
    in
324
    if excl == ineq then l1
325
    else AsstMultiSet.fold f left l1
326
  in
327
  (* This function looks for a:\exists R.C on the right side *)
328
  let iter1 ((left, gr, right) as ineq) flags =
329
    (* Find pairs of inequalities *)
330
    let f elem =
331
      match elem with
332
      (* Candidate for first inequality *)
333
      | HCCONCEPT(a, {fml = EXISTS(x, c)}) as r ->
334
          (* Get list of candidates for b *)
335
          let bs = InequalitySet.fold (fold1 a ineq) !ret [] in
336
          if List.length bs != 0 then (
337
            addInequality ret changed (left, gr, AsstMultiSet.remove r right) emptyFlags;
338
            let addf () b =
339
              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
340
            in
341
            List.fold_left addf () bs;
342
          ) else
343
            ();
344
      | _ -> ();
345
    in
346
    AsstMultiSet.iter f right;
347
  in
348
  InequalitySet.iter iter1 !ret
349

    
350
let max (a : int) (b : int) =
351
  if a > b then a else b
352

    
353
(*************************************************************
354
 * Solver loop
355
 *************************************************************)
356

    
357
let printABox hcInput =
358
  outputDebug "-------------";
359
  InequalitySet.iter (fun k flags -> outputDebug (printAssertion (toAssertion k))) !hcInput;
360
  outputDebug "-------------"
361

    
362
let rec internalSolve hcF input =
363
  let hcInput = ref input in
364
  let changed = ref true in
365
  outputDebug "Starting with ABox:";
366
  printABox hcInput;
367
  while !changed do
368
    changed := false;
369
    ruleNeg hcF hcInput changed;
370
    ruleAndRight hcF hcInput changed;
371
    ruleExistsRight hcF hcInput changed;
372
    printABox hcInput;
373
    outputDebug("Non-branching rules applied. Number of inequalities in result: " ^ string_of_int (InequalitySet.cardinal !hcInput))
374
  done;
375
  outputDebug "Non-branching rules applied, no further expansion possible.";
376
  (* XXX *)
377
  let ok = ref false in
378
  changed := false;
379
  ok := ruleExistsLeft hcF hcInput changed;
380
  if !changed then !ok else (
381
    ok := ruleAndLeft hcF hcInput changed;
382
    if !changed then !ok else (
383
      outputDebug("No branches possible. Checking if ABox clashes.");
384
      printABox hcInput;
385
      ruleClash hcF !hcInput
386
    )
387
  )
388
(*************************************************************
389
 * Branching rules
390
 * (They call the "internalSolve" function recursively)
391
 *************************************************************)
392
and ruleExistsLeft hcF ret changed =
393
  let ok = ref false in
394
  let iter ((left, gr, right) as ineq) flags =
395
    let f elem =
396
      match elem with
397
      (*
398
       * This rule may only be applied once to an inequality, successful
399
       * application is recorded in the flags field
400
       *)
401
      | HCCONCEPT(a, {fml = EXISTS(x, y); _}) when not (checkExistLeft flags) ->
402
          let nl = AsstMultiSet.remove elem left in
403
          let branch1 = (nl, gr, right) in
404
          let indiv = freshIndividual in
405
          let branch2 = (AsstMultiSet.add (toHcAsst hcF (ROLE(a, indiv, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(indiv, y))) nl), gr-1, right) in
406
          if (not (InequalitySet.mem branch1 !ret)) && (not (InequalitySet.mem branch2 !ret)) then
407
            (
408
              changed := true;
409
              (* Override previous flags for the premiss *)
410
              ret := InequalitySet.add ineq (addExistsLeft flags) !ret;
411
              ok := !ok ||
412
                internalSolve hcF (InequalitySet.add branch1 emptyFlags !ret) ||
413
                internalSolve hcF (InequalitySet.add branch2 emptyFlags !ret);
414
            )
415
          else
416
            ()
417
      | _ -> ();
418
    in
419
    AsstMultiSet.iter f left;
420
  in
421
  InequalitySet.iter iter !ret;
422
  !ok
423
and ruleAndLeft hcF ret changed =
424
  let ok = ref false in
425
  let iter (left, gr, right) flags =
426
    let f elem =
427
      match elem with
428
      | HCCONCEPT(a, {fml = AND(x, y); _}) as con ->
429
          let nl = AsstMultiSet.remove elem left in
430
          let branch1 = (nl, gr, right) in
431
          let branch2 = (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) (AsstMultiSet.remove con left)), gr-1, right) in
432
          if (not (InequalitySet.mem branch1 !ret)) && (not (InequalitySet.mem branch2 !ret)) then
433
            (
434
              changed := true;
435
              ok := !ok ||
436
                internalSolve hcF (InequalitySet.add branch1 emptyFlags !ret) ||
437
                internalSolve hcF (InequalitySet.add branch2 emptyFlags !ret);
438
            )
439
          else
440
            ()
441
      | _ -> ();
442
    in
443
    AsstMultiSet.iter f left;
444
  in
445
  InequalitySet.iter iter !ret;
446
  !ok
447

    
448
let rec fuzzyALCsat input =
449
  (* Create new HashCons table. Formulas don't have negation forms. *)
450
  let hcF = HcFormula.create false in
451
  (* Convert input formulae to hash-consed representation *)
452
  maxrole := (-1);
453
  let f ss (left, gr, right) =
454
    let g s asst =
455
      match asst with
456
      | ROLE(a, b, c) ->
457
          maxrole := max !maxrole (max a b);
458
          AsstMultiSet.add (HCROLE(a, b, c)) s
459
      | CONCEPT(a, c) ->
460
          maxrole := max !maxrole a;
461
          AsstMultiSet.add (HCCONCEPT(a, hc_formula hcF c)) s
462
    in
463
    InequalitySet.add (List.fold_left g AsstMultiSet.empty left, gr, List.fold_left g AsstMultiSet.empty right) emptyFlags ss
464
  in
465
  internalSolve hcF (List.fold_left f InequalitySet.empty input)