### Profile

Statistics
| Branch: | Revision:

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

 1 ```(** An on-the fly graph-tableau-based decision procedure ``` ``` for ALC-satisfiability with respect to a TBox ``` ``` which blocks on all nodes. ``` ``` It is optimal, that is EXPTIME. ``` ``` It also incorporates some optimisations. ``` ``` @author Florian Widmann ``` ``` *) ``` ```module A = ALCFormula ``` ```type formula = A.formula ``` ```type definition = A.definition ``` ```open ALCMisc ``` ```open MiscSolver ``` ```(** An instantiation of a hash table (of the standard library) for bitsets. ``` ``` *) ``` ```module GHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = bitset ``` ``` let equal (bs1 : t) bs2 = compareBS bs1 bs2 = 0 ``` ``` let hash (bs : t) = hashBS bs ``` ``` end ``` ``` ) ``` ```(** The status of a state. It can be either satisfiable, unsatisfiable, ``` ``` not yet expanded, or not yet known. In the latter case, ``` ``` it is distinguished whether the node is an or-node ``` ``` or an and-node (i.e. a state). ``` ``` Dependent on the status the following information is stored: ``` ``` Unexp: the principal formula that is to be used for expanding ``` ``` (if the node is a state then the formula is one of its <>-formulae ``` ``` to indicate that the state is not trivially satisfiable). ``` ``` AndNode: the number of children (i.e. core-nodes) ``` ``` that have no result yet (all other core-nodes must be satisfiable, ``` ``` otherwise the node would already be marked unsatisfiable). ``` ``` OrNode: see orStatus ``` ``` Unsat: A "minimal subset" of the set of formulae of the node ``` ``` that already contains the contradiction. ``` ``` *) ``` ```type status = ``` ``` Unexp of int ``` ``` | AndNode of int ``` ``` | OrNode of orStatus ``` ``` | Sat ``` ``` | Unsat of bitset ``` ```(** The sub-status of an or-node whose final status is still unknown. ``` ``` OneUnsat: One of its children is unsatisfiable. ``` ``` The part of the "minimal subset" that is contributed ``` ``` by the unsatisfiable child is stored. ``` ``` BothUnknwn: The status of both children are still unknown. ``` ``` The principal or-formula is stored ``` ``` as well as the "queue element" of the second child ``` ``` unless the second child's status was known ``` ``` while processing the or-node. ``` ``` That is the list is either empty or contains a single element ``` ``` consisting of the set of formulae of the second child, ``` ``` the child itself and the current or-node (i.e. the child's parent). ``` ``` *) ``` ```and orStatus = ``` ``` OneUnsat of bitset ``` ``` | BothUnknwn of int * (bitset * node * node) list ``` ```(** The information about a node that is stored in the graph: ``` ``` The current status of the node; and ``` ``` each predecessor of the node together with a dependency map. ``` ``` The actual set of formulae is not included as it is used ``` ``` to index the node. ``` ``` *) ``` ```and node = { mutable status : status; mutable preds : (node * dependency) list } ``` ```(** Represents a graph. ``` ``` *) ``` ```type graph = node GHt.t ``` ```(** Initialises a graph. ``` ``` @return An empty graph. ``` ``` *) ``` ```let mkGraph () = (GHt.create 64 : graph) ``` ```(** Returns the node that is assigned to a set of formulae in a graph ``` ``` if it exists. ``` ``` @param grph A graph. ``` ``` @param fs A bitset of formulae. ``` ``` @return None if fs is not contained in grph, Some n otherwise. ``` ``` In the latter case n is the node that is assigned to fs in grph. ``` ``` *) ``` ```let memGraph (grph : graph) fs = ``` ``` try ``` ``` Some (GHt.find grph fs) ``` ``` with Not_found -> None ``` ```(** Adds a set of formula and its assigned node to a graph. ``` ``` @param grph A graph. ``` ``` @param fs A bitset of formulae. ``` ``` @param node The node that is assigned to fs. ``` ``` *) ``` ```let addGraph (grph : graph) fs node = GHt.add grph fs node ``` ```(** Returns the size of a graph. ``` ``` @param grph A graph. ``` ``` @return The number of nodes in grph. ``` ``` *) ``` ```let sizeGraph (grph : graph) = GHt.length grph ``` ```(** Propagates (un)satisfiability as far as possible in a graph. ``` ``` @param equeue The queue of nodes that still might have to be expanded in grph. ``` ``` @param pqueue The queue of (expanded) nodes whose status has to be updated. ``` ``` It is a list of tuples (n, d, s) where: ``` ``` n is a node in the graph; ``` ``` d is the dependency map between the child that caused the update ``` ``` and the current node; and ``` ``` s is the status of the child that caused the update. ``` ``` @return The updated queue of nodes that still might have to be expanded in grph. ``` ``` *) ``` ```let rec propagate equeue pqueue = ``` ``` match pqueue with ``` ``` | (node, dep, sts)::tl -> begin ``` ``` match node.status with ``` ``` | AndNode i -> begin ``` ``` match sts with ``` ``` | Unsat ccfs -> ``` ``` let cfs = makeBS () in ``` ``` makeCSDep false ccfs dep cfs; ``` ``` List.iter (addBSNoChk cfs) (findDep dep (-1)); ``` ``` let nsts = Unsat cfs in ``` ``` node.status <- nsts; ``` ``` let ntl = List.fold_left (addTuple nsts) tl node.preds in ``` ``` propagate equeue ntl ``` ``` | _ -> (* must be Sat *) ``` ``` if i <= 1 then begin ``` ``` node.status <- Sat; ``` ``` let ntl = List.fold_left (addTuple Sat) tl node.preds in ``` ``` propagate equeue ntl ``` ``` end ``` ``` else begin ``` ``` node.status <- AndNode (pred i); ``` ``` propagate equeue tl ``` ``` end ``` ``` end ``` ``` | OrNode orsts -> begin ``` ``` match sts with ``` ``` | Unsat ccfs -> begin ``` ``` match orsts with ``` ``` | BothUnknwn (pf, eql) -> ``` ``` let cfs = makeBS () in ``` ``` makeCSDep true ccfs dep cfs; ``` ``` if memBS cfs pf then begin ``` ``` node.status <- OrNode (OneUnsat cfs); ``` ``` propagate (eql @ equeue) tl ``` ``` end ``` ``` else begin ``` ``` let nsts = Unsat cfs in ``` ``` node.status <- nsts; ``` ``` let ntl = List.fold_left (addTuple nsts) tl node.preds in ``` ``` propagate equeue ntl ``` ``` end ``` ``` | OneUnsat cfs -> ``` ``` makeCSDep true ccfs dep cfs; ``` ``` let nsts = Unsat cfs in ``` ``` node.status <- nsts; ``` ``` let ntl = List.fold_left (addTuple nsts) tl node.preds in ``` ``` propagate equeue ntl ``` ``` end ``` ``` | _ -> (* must be Sat *) ``` ``` node.status <- Sat; ``` ``` let ntl = List.fold_left (addTuple Sat) tl node.preds in ``` ``` propagate equeue ntl ``` ``` end ``` ``` | _ -> propagate equeue tl (* must be Sat or Unsat *) ``` ``` end ``` ``` | [] -> equeue ``` ```(** Checks for immediate (un)satisfiability. ``` ``` If this is not the case it checks whether the node is already in the graph ``` ``` and creates and inserts it otherwise. ``` ``` @param grph A graph. ``` ``` @param root The root node of the graph. ``` ``` When it is set to (un)satisfiable during the propagation ``` ``` then the decision procedure can stop. ``` ``` @param fset A set of formulae that is to be "inserted" in grph ``` ``` (if it already exists then its edges are updated). ``` ``` @param node The node that caused the creation of fset. ``` ``` @param dep The dependency map of fset and node. ``` ``` @param cntr None iff fset does not contain a contradiction, ``` ``` and Some cfs otherwise where cfs is a "minimal subset" of fset ``` ``` that already contains the contradiction. ``` ``` @param queue The queue of nodes that have to be processed in grph ``` ``` before updating it. ``` ``` @return The updated queue of nodes that still might have to be expanded in grph. ``` ``` *) ``` ```let intern_chkNode grph root fset node (dep, cntr) queue = ``` ``` match cntr with ``` ``` | None -> ``` ``` let pf = getPFinclEX fset in ``` ``` if pf >= 0 then ``` ``` match memGraph grph fset with ``` ``` | None -> begin ``` ``` let child = { status = Unexp pf; preds = [(node, dep)] } in ``` ``` let gfset = copyBS fset in ``` ``` addGraph grph gfset child; ``` ``` match node.status with ``` ``` | OrNode (BothUnknwn (opf, oql)) when oql = [] -> ``` ``` node.status <- OrNode (BothUnknwn (opf, [(fset, child, node)])); ``` ``` queue ``` ``` | _ -> (fset, child, node)::queue ``` ``` end ``` ``` | Some n -> begin ``` ``` match n.status with ``` ``` | Unexp _ -> begin ``` ``` n.preds <- (node, dep)::n.preds; ``` ``` match node.status with ``` ``` | OrNode (BothUnknwn (opf, oql)) when oql = [] -> ``` ``` node.status <- OrNode (BothUnknwn (opf, [(fset, n, node)])); ``` ``` queue ``` ``` | _ -> (fset, n, node)::queue ``` ``` end ``` ``` | Unsat _ as sts -> ``` ``` let queue1 = propagate queue [(node, dep, sts)] in ``` ``` begin ``` ``` match root.status with ``` ``` | Unsat _ -> raise (ALC_finished false) ``` ``` | _ -> () ``` ``` end; ``` ``` queue1 ``` ``` | Sat -> ``` ``` let queue1 = propagate queue [(node, dep, Sat)] in ``` ``` if root.status = Sat then raise (ALC_finished true) else (); ``` ``` queue1 ``` ``` | _ -> ``` ``` n.preds <- (node, dep)::n.preds; ``` ``` queue ``` ``` end ``` ``` else ``` ``` let queue1 = propagate queue [(node, dep, Sat)] in ``` ``` if root.status = Sat then raise (ALC_finished true) else (); ``` ``` queue1 ``` ``` | Some cfs -> ``` ``` let queue1 = propagate queue [(node, dep, Unsat cfs)] in ``` ``` begin ``` ``` match root.status with ``` ``` | Unsat _ -> raise (ALC_finished false) ``` ``` | _ -> () ``` ``` end; ``` ``` queue1 ``` ```(** Expands an unexpanded node in a graph. ``` ``` @param grph A graph. ``` ``` @param root The root node of the graph. ``` ``` When it is set to (un)satisfiable during the propagation ``` ``` then the decision procedure can stop. ``` ``` @param tbox A set of formulae representing ``` ``` the non-definitional part of a TBox. ``` ``` @param queue The queue of nodes that have to be processed in grph. ``` ``` The list queue contains triples (fs, n, p) where ``` ``` fs is the set of formulae of node n; ``` ``` n is the node that is assigned to fs in the graph; and ``` ``` p is the parent of fs that caused fs to be inserted in the queue. ``` ``` @return True iff the root is satisfiable. ``` ``` *) ``` ```let rec intern_isSat grph root tbox queue = ``` ``` match queue with ``` ``` | (fset, node, prnt)::tl -> begin ``` ``` match prnt.status with ``` ``` | OrNode _ ``` ``` | AndNode _ -> begin ``` ``` match node.status with ``` ``` | Unexp pf -> begin ``` ``` match !arrayType.(pf) with ``` ``` | 4 -> ``` ``` let f1 = !arrayDest1.(pf) in ``` ``` let f2 = !arrayDest2.(pf) in ``` ``` if not (containsFormula fset f1 || containsFormula fset f2) then begin ``` ``` node.status <- OrNode (BothUnknwn (pf, [])); ``` ``` remBS fset pf; ``` ``` let fset2 = copyBS fset in ``` ``` let pair2a = ``` ``` let (dep2, cntr2) as res2 = insertFormulaDep fset2 f2 emptyDep [pf] in ``` ``` match cntr2 with ``` ``` | None -> ``` ``` let notf1 = !arrayNeg.(f1) in ``` ``` if notf1 >= 0 then insertFormulaDep fset2 notf1 dep2 [pf] ``` ``` else res2 ``` ``` | Some _ -> res2 ``` ``` in ``` ``` let pair2b = testSubsume true fset2 pair2a in ``` ``` let tl1 = intern_chkNode grph root fset2 node pair2b tl in ``` ``` match node.status with ``` ``` | OrNode _ -> ``` ``` let pair1a = insertFormulaDep fset f1 emptyDep [pf] in ``` ``` let pair1b = testSubsume true fset pair1a in ``` ``` let tl2 = intern_chkNode grph root fset node pair1b tl1 in ``` ``` intern_isSat grph root tbox tl2 ``` ``` | _ -> intern_isSat grph root tbox tl1 ``` ``` end ``` ``` else begin ``` ``` node.status <- OrNode (OneUnsat (makeBS ())); ``` ``` remBS fset pf; ``` ``` let pair = (emptyDep, None) in ``` ``` let tl1 = intern_chkNode grph root fset node pair tl in ``` ``` intern_isSat grph root tbox tl1 ``` ``` end ``` ``` | _ -> (* must be 6 *) ``` ``` let rec detmrk acc = function ``` ``` | pfi::tlpf -> ``` ``` let fseti = copyBS tbox in ``` ``` let (dep, cntr) = mkDeltaDep fset pfi fseti in ``` ``` let dep2 = addDep dep (-1) [pfi] in ``` ``` let pairi = testSubsume false fseti (dep2, cntr) in ``` ``` let nacc = intern_chkNode grph root fseti node pairi acc in ``` ``` begin ``` ``` match node.status with ``` ``` | AndNode _ -> detmrk nacc tlpf ``` ``` | _ -> intern_isSat grph root tbox nacc ``` ``` end ``` ``` | [] -> intern_isSat grph root tbox acc ``` ``` in ``` ``` let succs = mkEXList fset in ``` ``` node.status <- AndNode (List.length succs); ``` ``` detmrk tl succs ``` ``` end ``` ``` | _ -> intern_isSat grph root tbox tl ``` ``` end ``` ``` | _ -> intern_isSat grph root tbox tl (* must be Sat or Unsat *) ``` ``` end ``` ``` | [] -> ``` ``` match root.status with ``` ``` | Unsat _ -> false ``` ``` | _ -> true ``` ```(** An on-the fly graph-tableau-based decision procedure ``` ``` for ALC-satisfiability with respect to a TBox ``` ``` which blocks on all nodes. ``` ``` It is optimal, that is EXPTIME. ``` ``` It also incorporates some optimisations. ``` ``` @param verbose An optional switch which determines ``` ``` whether the procedure shall print some information on the standard output. ``` ``` The default is false. ``` ``` @param fl A list of input formulae that are tested for satisfiability. ``` ``` @param tboxND A list of formulae representing ``` ``` the non-definitional part of a TBox. ``` ``` @param tboxD A list of definitions (see ALCFormula.ml) ``` ``` representing the definitional part of a TBox. ``` ``` The definitions must not be cyclic ``` ``` and each concept must not be defined more than once. ``` ``` @return True if fl is satisfiable in the given TBox, false otherwise. ``` ``` *) ``` ```let isSat ?(verbose = false) fl tboxND tboxD = ``` ``` let start = if verbose then Unix.gettimeofday () else 0. in ``` ``` let grph = mkGraph () in ``` ``` let (nfl, ntboxND, ntboxD, fset, tbox, cntr) = ppFormulae fl tboxND tboxD rankingNoAnd notyNoAnd false in ``` ``` let sat = ``` ``` if cntr || subsume fset then false ``` ``` else ``` ``` let pf = getPFinclEX fset in ``` ``` if pf >= 0 then ``` ``` try ``` ``` let dummy = { status = AndNode (-1); preds = [] } in ``` ``` let root = { status = Unexp pf; preds = [] } in ``` ``` let gfset = copyBS fset in ``` ``` addGraph grph gfset root; ``` ``` intern_isSat grph root tbox [(fset, root, dummy)] ``` ``` with ALC_finished res -> res ``` ``` else true ``` ``` in ``` ``` if verbose then begin ``` ``` let stop = Unix.gettimeofday () in ``` ```(* ``` ``` let addup lst = List.fold_left (fun acc e -> acc + (A.sizeFormula e)) 0 lst in ``` ``` let addup2 lst = ``` ``` let addD acc = function ``` ``` | A.PRIMITIVE (_, f) ``` ``` | A.NECANDSUFF (_, f) -> acc + (A.sizeFormula f) ``` ``` in ``` ``` List.fold_left addD 0 lst ``` ``` in ``` ``` print_newline (); ``` ``` print_endline ("Query: " ^ (A.exportQuery fl tboxND tboxD)); ``` ``` let size = (addup fl) + (addup tboxND) + (addup2 tboxD) in ``` ``` print_endline ("Added Size: " ^ (string_of_int size)); ``` ``` print_endline ("Negation Normal Form: " ^ (A.exportQuery nfl ntboxND ntboxD)); ``` ``` let nsize = (addup nfl) + (addup ntboxND) + (addup2 ntboxD) in ``` ``` print_endline ("Added Size: " ^ (string_of_int nsize)); ``` ``` *) ``` ``` print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); ``` ``` print_endline ("Time: " ^ (string_of_float (stop -. start))); ``` ``` print_endline ("Generated nodes: " ^ (string_of_int (sizeGraph grph))); ``` ``` print_newline () ``` ``` end else (); ``` ``` sat ```