Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / FuzzyALCReasoner.ml @ fa1727d2

History | View | Annotate | Download (15.3 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
 * For debug reasons: Prints ABox to stdout
156
 *)
157
let printABox hcInput =
158
  outputDebug "-------------";
159
  InequalitySet.iter (fun k flags -> outputDebug (printAssertion (toAssertion k))) !hcInput;
160
  outputDebug "-------------"
161

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

    
182
let maxrole = ref (0)
183

    
184
let max (a : int) (b : int) =
185
  if a > b then a else b
186

    
187
let freshIndividual =
188
  maxrole := (!maxrole) + 1;
189
  !maxrole
190

    
191
exception InternalReasonerError of string
192

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

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

    
271
let addInequality ref changed ineq flags =
272
  if not (InequalitySet.mem ineq !ref) then (
273
    ref := InequalitySet.add ineq flags !ref;
274
    changed := true)
275

    
276
(************************************************************
277
 * non-branching rules. We can always apply them
278
 ************************************************************)
279

    
280
(*
281
 * Applies negation elimination to both sides of the
282
 * inequality, left and right
283
 *)
284
let rec ruleNeg hcF ret changed =
285
  let iter ((left, gr, right) as ineq) flags =
286
    let iter_asst_left hcasst =
287
      match hcasst with
288
      | HCCONCEPT(a, {fml = NOT(y); _}) ->
289
          (*ret := InequalitySet.remove ineq !ret;*)
290
          addInequality ret changed (AsstMultiSet.remove hcasst left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) right) emptyFlags;
291
      | _ -> ()
292
    in
293
    let iter_asst_right hcasst =
294
      match hcasst with
295
      | HCCONCEPT(a, {fml = NOT(y); _}) ->
296
          (*ret := InequalitySet.remove ineq !ret;*)
297
          addInequality ret changed (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) left, gr-1, AsstMultiSet.remove hcasst right) emptyFlags;
298
      | _ -> ()
299
    in
300
    AsstMultiSet.iter iter_asst_left left;
301
    AsstMultiSet.iter iter_asst_right right;
302
  in
303
  InequalitySet.iter iter !ret
304

    
305
let rec ruleAndRight hcF ret changed =
306
  let iter (left, gr, right) flags =
307
    let f elem =
308
      match elem with
309
      | HCCONCEPT(a, {fml = AND(x, y); _}) ->
310
          let nr = AsstMultiSet.remove elem right in
311
          addInequality ret changed (left, gr, nr) emptyFlags;
312
          addInequality ret changed (left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) nr)) emptyFlags;
313
      | _ -> ();
314
    in
315
    AsstMultiSet.iter f right;
316
  in
317
  InequalitySet.iter iter !ret
318

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

    
361
(*************************************************************
362
 * Solver loop and branching rules (mutually recursive
363
 * with main solver routine)
364
 *************************************************************)
365

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

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