Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / FuzzyALCReasoner.ml @ a0ad2fd9

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 false else (
211
  outputDebug ("Building LP problem for " ^ string_of_int (List.length assertions) ^ " ABox inequalities" ^ " and " ^ string_of_int n ^ " variables.");
212
  List.fold_left f 0 assertions;
213
  (*outputDebug "Solving!";*)
214
  let lp = make_problem Maximize coeff matrix auxbound origbound in
215
  simplex lp;
216
  if get_status lp then outputDebug "Satisfiable ABox!"
217
  else outputDebug "Unsatisfiable ABox!";
218
  get_status lp )
219

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

    
256
let addInequality ref changed ineq flags =
257
  if not (InequalitySet.mem ineq !ref) then (
258
    ref := InequalitySet.add ineq flags !ref;
259
    changed := true)
260

    
261
(************************************************************
262
 * non-branching rules. We can always apply them
263
 ************************************************************)
264

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

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

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

    
346
let max (a : int) (b : int) =
347
  if a > b then a else b
348

    
349
(*************************************************************
350
 * Solver loop
351
 *************************************************************)
352

    
353
let printABox hcInput =
354
  outputDebug "-------------";
355
  InequalitySet.iter (fun k flags -> outputDebug (printAssertion (toAssertion k))) !hcInput;
356
  outputDebug "-------------"
357

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

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