DIG Optimisation Techniques

DIG maintains this list of description logics optimisation techniques as a resource for implementators of description logic and related systems.

This is an initial list of optimisation techniques gathered at a DIG workshop.

Satisfiability Techniques

simplification
search techniques
- trace technique
- syntactic branching
- semantic branching
- no-goods list
- mixed strategy (local versus global, agenda)
dependency directed backtracking
- dynamic backtracking
- deterministic first versus local first
cheap inferences (sound but not complete)
- structural
- caching (of modal successors)
- caching (of models)
- model merging
heuristics
- picking disjunction/disjunct
- picking existential (e.g., interaction with alls)
- local tuning of optimisations
- picking positive/negative
qualified number restrictions
- division and counting
absorption
- standard
- specialised (range/domain etc.)
lazy unfolding
blocking techniques
simplification/normalisation
built-in idioms
- disjointness
- range/domain

simplification
basic top-down, bottom-up method
cheap inferences (e.g., told subsumer)
- told subsumers/disjoints
- propagating results of top search
model merging (obvious non-subsumption)
- alternate models
- overconstrained/incidental models
- lazy unfolding
avoiding bottom search
heuristics
- ordering of concept names
- ordering of modal successors
- ordering of disjunctions/disjuncts
- reducing number of non-absorbable axioms

hash versus subset blocking (hash supports fast equality blocking)
store concept sets labelled with node names instead of node names labelled with sets of concepts
state saving
what to record (saving space)