Consider more-performant alternatives to ROBOT's "Checking for unsatisfiable [classes/object properties]"?

[jclerman]

I have noticed that the "reason" step in ROBOT takes much longer than it does in Protege, for the same version of Hermit and the same ontology (and same hardware).

The difference isn't in the reasoning step per se (i.e., computation of the class hierarchy, and subsequent sub-steps) - rather it is the fact that ROBOT does separate steps for Checking for unsatisfiable classes and Checking for unsatisfiable object properties (in my hands, it's the 2nd one that can be very expensive - as much as 60 minutes in a CI environment).

This was mentioned a few years ago in #368, but wasn't really the focus of that ticket (though it triggered some discussion).

@cmungall noted at the time that omitting those steps altogether would be unwise - but on the other hand, as far as I can tell, Protege accomplishes the same result, at least for unsatisfiable classes, more or less as a side-effect of computing the class hierarchy. So for classes at least, it seems that ROBOT's logic could place the class-unsats check after the class-hierarchy computation, and then implement it simply as a check for classes equivalent to owl:Nothing.

For object-properties, I'm less certain about the opportunities for a speedup - in a way, the question comes down to "does Protege effectively compute unsatisfiable object properties as an artifact of running a reasoner, the way it does for unsatisfiable classes?". If so, it'd be nice to have ROBOT skip "Checking for unsatisfiable object properties" and instead take advantage of reasoning results to infer it, saving lots of time when doing robot reason.

[jclerman]

Based on a quick bit of testing, it looks like Protege does in fact also compute unsatisfiable properties in the course of computing the object-property hierarchy, in the the sense that they are inferred to be equivalent to owl:bottomObjectProperty (behold silly example below).

Could ROBOT take the same approach?

[cmungall]

It looks like I may be responsible for this

I think this stems from my attempt to address

• test for unsatisfiable ObjectProperties #104.

Clearly the simpler thing to do is to test the RBox classification for equivalence to bottomProperty as you suggest.

The one advantage my more complicated approach has is that it will work with Elk, which is important for a lot of large ontologies. But it doesn't make sense to employ it if you're already using a DL reasoner like hermit

[jclerman]

Instead of the more complicated approach currently implemented, would it be feasible to always use Hermit just to check for unsatisfiable object-properties (by computing the object-property hierarchy & checking for bottomProperty equivalences) - regardless of which reasoner is selected for the "overall" reason step? I don't know if that'd be tractable for the larger ontologies?

Or, leave things as-is when ELK is in use, but use my suggested approach when Hermit is the selected reasoner.

[cmungall]

You need to include the tbox to get complete results - see the linked example above.

I think the latter approach is best. The question is whether to change current behavior for non elk reasoners or make the strategy more explicitly under the control of the user

[jamesaoverton]

I haven't looked at the code for this, but in general backwards compatibly is very important for ROBOT. If we can improve performance without otherwise changing behaviour, that's great. Otherwise we can consider adding yet another option flag. Of course, the complexity and maintainability of changes are also important.

[cmungall]

I think there is a good argument that dynamically switching to the simpler testing of equivalence to bottom if a DL reasoner is past still preserves backwards compatibility. The inferences should be the same.

[jamesaoverton]

Ok. The truth is that I can't make this a priority for my team on any reasonable timeline. A PR would be very welcome.

[jclerman]

I'd be happy to try my hand at a PR for this, but I have next to no Java programming experience. I've opened the code in IntelliJ and experimented with just trying to add a conditional precomputation of the object-property hierarchy, depending on whether the HermiT reasoner is in use - but I quickly found that it's nontrivial to determine which reasoner is in use, from an OWLReasoner object. Is there a good way to do that?

Here's what I'm trying, within ReasonOperation.java:

    logger.info("Precomputing class hierarchy...");
    reasoner.precomputeInferences(InferenceType.CLASS_HIERARCHY);

    // my code added below
    if (reasoner.getReasonerName().contains("HermiT")) {
      logger.info("Using HermiT, so precomputing object-property hierarchy...");
      reasoner.precomputeInferences(InferenceType.OBJECT_PROPERTY_HIERARCHY);
    }

The issue I encounter is that getReasonerName() returns null (much to my chagrin).

UPDATE: reasoner.getClass().getPackage().getName() worked as a substitute. Looks like I may be on my way. Advice welcome - the codebase is new to me, and the closest I've come to Java-development was programming in Scala for about 6 months several years ago.

[jamesaoverton]

Ok. It's unfortunate that getReasonerName() returns null, but I think that reasoner.getClass().getPackage().getName() is fine. A PR that switches behaviour when HermiT is detected would be a great start.

[jclerman]

PR filed. I took a different approach than the getName() thing mentioned above - hopefully much more robust. Should be ready for review - not sure if more test-cases are needed, and I haven't updated the CHANGELOG yet - will do that tomorrow.

[jamesaoverton]

Thanks @jclerman! I skimmed the PR and things look good. We'll do a more thorough review. @matentzn Is there someone you can ask to review?

I just want to manage expectations: We have a limited number of hours to work on ROBOT and related tools. The OWLAPI update is taking a lot of hours. So we may not be able to handle this PR as quickly as we would like.

[jclerman]

Sounds good @jamesaoverton, hope the PR is as helpful to others as I expect it to be to me! ROBOT has been a very valuable tool for me and I'm happy to make a small contribution to the project.

I've marked it as ready for review - but please let me know if there are additional test-cases you'd like to see.