Project

General

Profile

Statistics
| Branch: | Revision:

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