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