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

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) |