## cool / src / lib / ALCGraph.ml @ 7c4d2eb4

History | View | Annotate | Download (15.1 KB)

1 |
(** An on-the fly graph-tableau-based decision procedure |
---|---|

2 |
for ALC-satisfiability with respect to a TBox |

3 |
which blocks on all nodes. |

4 |
It is optimal, that is EXPTIME. |

5 |
It also incorporates some optimisations. |

6 |
@author Florian Widmann |

7 |
*) |

8 | |

9 | |

10 |
module A = ALCFormula |

11 | |

12 |
type formula = A.formula |

13 |
type definition = A.definition |

14 | |

15 | |

16 |
open ALCMisc |

17 |
open MiscSolver |

18 | |

19 | |

20 |
(** An instantiation of a hash table (of the standard library) for bitsets. |

21 |
*) |

22 |
module GHt = Hashtbl.Make( |

23 |
struct |

24 |
type t = bitset |

25 |
let equal (bs1 : t) bs2 = compareBS bs1 bs2 = 0 |

26 |
let hash (bs : t) = hashBS bs |

27 |
end |

28 |
) |

29 | |

30 | |

31 |
(** The status of a state. It can be either satisfiable, unsatisfiable, |

32 |
not yet expanded, or not yet known. In the latter case, |

33 |
it is distinguished whether the node is an or-node |

34 |
or an and-node (i.e. a state). |

35 |
Dependent on the status the following information is stored: |

36 |
Unexp: the principal formula that is to be used for expanding |

37 |
(if the node is a state then the formula is one of its <>-formulae |

38 |
to indicate that the state is not trivially satisfiable). |

39 |
AndNode: the number of children (i.e. core-nodes) |

40 |
that have no result yet (all other core-nodes must be satisfiable, |

41 |
otherwise the node would already be marked unsatisfiable). |

42 |
OrNode: see orStatus |

43 |
Unsat: A "minimal subset" of the set of formulae of the node |

44 |
that already contains the contradiction. |

45 |
*) |

46 |
type status = |

47 |
Unexp of int |

48 |
| AndNode of int |

49 |
| OrNode of orStatus |

50 |
| Sat |

51 |
| Unsat of bitset |

52 | |

53 |
(** The sub-status of an or-node whose final status is still unknown. |

54 |
OneUnsat: One of its children is unsatisfiable. |

55 |
The part of the "minimal subset" that is contributed |

56 |
by the unsatisfiable child is stored. |

57 |
BothUnknwn: The status of both children are still unknown. |

58 |
The principal or-formula is stored |

59 |
as well as the "queue element" of the second child |

60 |
unless the second child's status was known |

61 |
while processing the or-node. |

62 |
That is the list is either empty or contains a single element |

63 |
consisting of the set of formulae of the second child, |

64 |
the child itself and the current or-node (i.e. the child's parent). |

65 |
*) |

66 |
and orStatus = |

67 |
OneUnsat of bitset |

68 |
| BothUnknwn of int * (bitset * node * node) list |

69 | |

70 |
(** The information about a node that is stored in the graph: |

71 |
The current status of the node; and |

72 |
each predecessor of the node together with a dependency map. |

73 |
The actual set of formulae is not included as it is used |

74 |
to index the node. |

75 |
*) |

76 |
and node = { mutable status : status; mutable preds : (node * dependency) list } |

77 | |

78 | |

79 |
(** Represents a graph. |

80 |
*) |

81 |
type graph = node GHt.t |

82 | |

83 |
(** Initialises a graph. |

84 |
@return An empty graph. |

85 |
*) |

86 |
let mkGraph () = (GHt.create 64 : graph) |

87 | |

88 |
(** Returns the node that is assigned to a set of formulae in a graph |

89 |
if it exists. |

90 |
@param grph A graph. |

91 |
@param fs A bitset of formulae. |

92 |
@return None if fs is not contained in grph, Some n otherwise. |

93 |
In the latter case n is the node that is assigned to fs in grph. |

94 |
*) |

95 |
let memGraph (grph : graph) fs = |

96 |
try |

97 |
Some (GHt.find grph fs) |

98 |
with Not_found -> None |

99 | |

100 |
(** Adds a set of formula and its assigned node to a graph. |

101 |
@param grph A graph. |

102 |
@param fs A bitset of formulae. |

103 |
@param node The node that is assigned to fs. |

104 |
*) |

105 |
let addGraph (grph : graph) fs node = GHt.add grph fs node |

106 | |

107 |
(** Returns the size of a graph. |

108 |
@param grph A graph. |

109 |
@return The number of nodes in grph. |

110 |
*) |

111 |
let sizeGraph (grph : graph) = GHt.length grph |

112 | |

113 | |

114 |
(** Propagates (un)satisfiability as far as possible in a graph. |

115 |
@param equeue The queue of nodes that still might have to be expanded in grph. |

116 |
@param pqueue The queue of (expanded) nodes whose status has to be updated. |

117 |
It is a list of tuples (n, d, s) where: |

118 |
n is a node in the graph; |

119 |
d is the dependency map between the child that caused the update |

120 |
and the current node; and |

121 |
s is the status of the child that caused the update. |

122 |
@return The updated queue of nodes that still might have to be expanded in grph. |

123 |
*) |

124 |
let rec propagate equeue pqueue = |

125 |
match pqueue with |

126 |
| (node, dep, sts)::tl -> begin |

127 |
match node.status with |

128 |
| AndNode i -> begin |

129 |
match sts with |

130 |
| Unsat ccfs -> |

131 |
let cfs = makeBS () in |

132 |
makeCSDep false ccfs dep cfs; |

133 |
List.iter (addBSNoChk cfs) (findDep dep (-1)); |

134 |
let nsts = Unsat cfs in |

135 |
node.status <- nsts; |

136 |
let ntl = List.fold_left (addTuple nsts) tl node.preds in |

137 |
propagate equeue ntl |

138 |
| _ -> (* must be Sat *) |

139 |
if i <= 1 then begin |

140 |
node.status <- Sat; |

141 |
let ntl = List.fold_left (addTuple Sat) tl node.preds in |

142 |
propagate equeue ntl |

143 |
end |

144 |
else begin |

145 |
node.status <- AndNode (pred i); |

146 |
propagate equeue tl |

147 |
end |

148 |
end |

149 |
| OrNode orsts -> begin |

150 |
match sts with |

151 |
| Unsat ccfs -> begin |

152 |
match orsts with |

153 |
| BothUnknwn (pf, eql) -> |

154 |
let cfs = makeBS () in |

155 |
makeCSDep true ccfs dep cfs; |

156 |
if memBS cfs pf then begin |

157 |
node.status <- OrNode (OneUnsat cfs); |

158 |
propagate (eql @ equeue) tl |

159 |
end |

160 |
else begin |

161 |
let nsts = Unsat cfs in |

162 |
node.status <- nsts; |

163 |
let ntl = List.fold_left (addTuple nsts) tl node.preds in |

164 |
propagate equeue ntl |

165 |
end |

166 |
| OneUnsat cfs -> |

167 |
makeCSDep true ccfs dep cfs; |

168 |
let nsts = Unsat cfs in |

169 |
node.status <- nsts; |

170 |
let ntl = List.fold_left (addTuple nsts) tl node.preds in |

171 |
propagate equeue ntl |

172 |
end |

173 |
| _ -> (* must be Sat *) |

174 |
node.status <- Sat; |

175 |
let ntl = List.fold_left (addTuple Sat) tl node.preds in |

176 |
propagate equeue ntl |

177 |
end |

178 |
| _ -> propagate equeue tl (* must be Sat or Unsat *) |

179 |
end |

180 |
| [] -> equeue |

181 | |

182 | |

183 |
(** Checks for immediate (un)satisfiability. |

184 |
If this is not the case it checks whether the node is already in the graph |

185 |
and creates and inserts it otherwise. |

186 |
@param grph A graph. |

187 |
@param root The root node of the graph. |

188 |
When it is set to (un)satisfiable during the propagation |

189 |
then the decision procedure can stop. |

190 |
@param fset A set of formulae that is to be "inserted" in grph |

191 |
(if it already exists then its edges are updated). |

192 |
@param node The node that caused the creation of fset. |

193 |
@param dep The dependency map of fset and node. |

194 |
@param cntr None iff fset does not contain a contradiction, |

195 |
and Some cfs otherwise where cfs is a "minimal subset" of fset |

196 |
that already contains the contradiction. |

197 |
@param queue The queue of nodes that have to be processed in grph |

198 |
before updating it. |

199 |
@return The updated queue of nodes that still might have to be expanded in grph. |

200 |
*) |

201 |
let intern_chkNode grph root fset node (dep, cntr) queue = |

202 |
match cntr with |

203 |
| None -> |

204 |
let pf = getPFinclEX fset in |

205 |
if pf >= 0 then |

206 |
match memGraph grph fset with |

207 |
| None -> begin |

208 |
let child = { status = Unexp pf; preds = [(node, dep)] } in |

209 |
let gfset = copyBS fset in |

210 |
addGraph grph gfset child; |

211 |
match node.status with |

212 |
| OrNode (BothUnknwn (opf, oql)) when oql = [] -> |

213 |
node.status <- OrNode (BothUnknwn (opf, [(fset, child, node)])); |

214 |
queue |

215 |
| _ -> (fset, child, node)::queue |

216 |
end |

217 |
| Some n -> begin |

218 |
match n.status with |

219 |
| Unexp _ -> begin |

220 |
n.preds <- (node, dep)::n.preds; |

221 |
match node.status with |

222 |
| OrNode (BothUnknwn (opf, oql)) when oql = [] -> |

223 |
node.status <- OrNode (BothUnknwn (opf, [(fset, n, node)])); |

224 |
queue |

225 |
| _ -> (fset, n, node)::queue |

226 |
end |

227 |
| Unsat _ as sts -> |

228 |
let queue1 = propagate queue [(node, dep, sts)] in |

229 |
begin |

230 |
match root.status with |

231 |
| Unsat _ -> raise (ALC_finished false) |

232 |
| _ -> () |

233 |
end; |

234 |
queue1 |

235 |
| Sat -> |

236 |
let queue1 = propagate queue [(node, dep, Sat)] in |

237 |
if root.status = Sat then raise (ALC_finished true) else (); |

238 |
queue1 |

239 |
| _ -> |

240 |
n.preds <- (node, dep)::n.preds; |

241 |
queue |

242 |
end |

243 |
else |

244 |
let queue1 = propagate queue [(node, dep, Sat)] in |

245 |
if root.status = Sat then raise (ALC_finished true) else (); |

246 |
queue1 |

247 |
| Some cfs -> |

248 |
let queue1 = propagate queue [(node, dep, Unsat cfs)] in |

249 |
begin |

250 |
match root.status with |

251 |
| Unsat _ -> raise (ALC_finished false) |

252 |
| _ -> () |

253 |
end; |

254 |
queue1 |

255 | |

256 | |

257 |
(** Expands an unexpanded node in a graph. |

258 |
@param grph A graph. |

259 |
@param root The root node of the graph. |

260 |
When it is set to (un)satisfiable during the propagation |

261 |
then the decision procedure can stop. |

262 |
@param tbox A set of formulae representing |

263 |
the non-definitional part of a TBox. |

264 |
@param queue The queue of nodes that have to be processed in grph. |

265 |
The list queue contains triples (fs, n, p) where |

266 |
fs is the set of formulae of node n; |

267 |
n is the node that is assigned to fs in the graph; and |

268 |
p is the parent of fs that caused fs to be inserted in the queue. |

269 |
@return True iff the root is satisfiable. |

270 |
*) |

271 |
let rec intern_isSat grph root tbox queue = |

272 |
match queue with |

273 |
| (fset, node, prnt)::tl -> begin |

274 |
match prnt.status with |

275 |
| OrNode _ |

276 |
| AndNode _ -> begin |

277 |
match node.status with |

278 |
| Unexp pf -> begin |

279 |
match !arrayType.(pf) with |

280 |
| 4 -> |

281 |
let f1 = !arrayDest1.(pf) in |

282 |
let f2 = !arrayDest2.(pf) in |

283 |
if not (containsFormula fset f1 || containsFormula fset f2) then begin |

284 |
node.status <- OrNode (BothUnknwn (pf, [])); |

285 |
remBS fset pf; |

286 |
let fset2 = copyBS fset in |

287 |
let pair2a = |

288 |
let (dep2, cntr2) as res2 = insertFormulaDep fset2 f2 emptyDep [pf] in |

289 |
match cntr2 with |

290 |
| None -> |

291 |
let notf1 = !arrayNeg.(f1) in |

292 |
if notf1 >= 0 then insertFormulaDep fset2 notf1 dep2 [pf] |

293 |
else res2 |

294 |
| Some _ -> res2 |

295 |
in |

296 |
let pair2b = testSubsume true fset2 pair2a in |

297 |
let tl1 = intern_chkNode grph root fset2 node pair2b tl in |

298 |
match node.status with |

299 |
| OrNode _ -> |

300 |
let pair1a = insertFormulaDep fset f1 emptyDep [pf] in |

301 |
let pair1b = testSubsume true fset pair1a in |

302 |
let tl2 = intern_chkNode grph root fset node pair1b tl1 in |

303 |
intern_isSat grph root tbox tl2 |

304 |
| _ -> intern_isSat grph root tbox tl1 |

305 |
end |

306 |
else begin |

307 |
node.status <- OrNode (OneUnsat (makeBS ())); |

308 |
remBS fset pf; |

309 |
let pair = (emptyDep, None) in |

310 |
let tl1 = intern_chkNode grph root fset node pair tl in |

311 |
intern_isSat grph root tbox tl1 |

312 |
end |

313 |
| _ -> (* must be 6 *) |

314 |
let rec detmrk acc = function |

315 |
| pfi::tlpf -> |

316 |
let fseti = copyBS tbox in |

317 |
let (dep, cntr) = mkDeltaDep fset pfi fseti in |

318 |
let dep2 = addDep dep (-1) [pfi] in |

319 |
let pairi = testSubsume false fseti (dep2, cntr) in |

320 |
let nacc = intern_chkNode grph root fseti node pairi acc in |

321 |
begin |

322 |
match node.status with |

323 |
| AndNode _ -> detmrk nacc tlpf |

324 |
| _ -> intern_isSat grph root tbox nacc |

325 |
end |

326 |
| [] -> intern_isSat grph root tbox acc |

327 |
in |

328 |
let succs = mkEXList fset in |

329 |
node.status <- AndNode (List.length succs); |

330 |
detmrk tl succs |

331 |
end |

332 |
| _ -> intern_isSat grph root tbox tl |

333 |
end |

334 |
| _ -> intern_isSat grph root tbox tl (* must be Sat or Unsat *) |

335 |
end |

336 |
| [] -> |

337 |
match root.status with |

338 |
| Unsat _ -> false |

339 |
| _ -> true |

340 | |

341 | |

342 |
(** An on-the fly graph-tableau-based decision procedure |

343 |
for ALC-satisfiability with respect to a TBox |

344 |
which blocks on all nodes. |

345 |
It is optimal, that is EXPTIME. |

346 |
It also incorporates some optimisations. |

347 |
@param verbose An optional switch which determines |

348 |
whether the procedure shall print some information on the standard output. |

349 |
The default is false. |

350 |
@param fl A list of input formulae that are tested for satisfiability. |

351 |
@param tboxND A list of formulae representing |

352 |
the non-definitional part of a TBox. |

353 |
@param tboxD A list of definitions (see ALCFormula.ml) |

354 |
representing the definitional part of a TBox. |

355 |
The definitions must not be cyclic |

356 |
and each concept must not be defined more than once. |

357 |
@return True if fl is satisfiable in the given TBox, false otherwise. |

358 |
*) |

359 |
let isSat ?(verbose = false) fl tboxND tboxD = |

360 |
let start = if verbose then Unix.gettimeofday () else 0. in |

361 |
let grph = mkGraph () in |

362 |
let (nfl, ntboxND, ntboxD, fset, tbox, cntr) = ppFormulae fl tboxND tboxD rankingNoAnd notyNoAnd false in |

363 |
let sat = |

364 |
if cntr || subsume fset then false |

365 |
else |

366 |
let pf = getPFinclEX fset in |

367 |
if pf >= 0 then |

368 |
try |

369 |
let dummy = { status = AndNode (-1); preds = [] } in |

370 |
let root = { status = Unexp pf; preds = [] } in |

371 |
let gfset = copyBS fset in |

372 |
addGraph grph gfset root; |

373 |
intern_isSat grph root tbox [(fset, root, dummy)] |

374 |
with ALC_finished res -> res |

375 |
else true |

376 |
in |

377 |
if verbose then begin |

378 |
let stop = Unix.gettimeofday () in |

379 |
(* |

380 |
let addup lst = List.fold_left (fun acc e -> acc + (A.sizeFormula e)) 0 lst in |

381 |
let addup2 lst = |

382 |
let addD acc = function |

383 |
| A.PRIMITIVE (_, f) |

384 |
| A.NECANDSUFF (_, f) -> acc + (A.sizeFormula f) |

385 |
in |

386 |
List.fold_left addD 0 lst |

387 |
in |

388 |
print_newline (); |

389 |
print_endline ("Query: " ^ (A.exportQuery fl tboxND tboxD)); |

390 |
let size = (addup fl) + (addup tboxND) + (addup2 tboxD) in |

391 |
print_endline ("Added Size: " ^ (string_of_int size)); |

392 |
print_endline ("Negation Normal Form: " ^ (A.exportQuery nfl ntboxND ntboxD)); |

393 |
let nsize = (addup nfl) + (addup ntboxND) + (addup2 ntboxD) in |

394 |
print_endline ("Added Size: " ^ (string_of_int nsize)); |

395 |
*) |

396 |
print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); |

397 |
print_endline ("Time: " ^ (string_of_float (stop -. start))); |

398 |
print_endline ("Generated nodes: " ^ (string_of_int (sizeGraph grph))); |

399 |
print_newline () |

400 |
end else (); |

401 |
sat |