diff --git a/docs/explain.md b/docs/explain.md index d8d8b4aaf..f32d50281 100644 --- a/docs/explain.md +++ b/docs/explain.md @@ -61,6 +61,9 @@ You have three options to generate explanations for many unsatisfiable classes a - `root`: generate explanations for all _root unsatisfiable classes_. In OWL, a root unsatisfiable class, roughly, is a class whose unsatisfiability cannot be explained by the unsatisfiability of another class. A comprehensive explanation of the concept can be found [here](https://www.sciencedirect.com/science/article/pii/S1570826805000260). +- `most_general`: this is a very naive, experimental variant of the proper `root` method. It determines +explanations for those unsatisfiable classes that, according to the _asserted class hierarchy_, have no parents that are also +unsatisfiable. Note that this approach only works if the class hierarchy does not contain cycles. - `random:n`: Sometimes, you may want to generate explanations for unsatisfiable classes en masse, but because of the large number in your source ontology, restrict your investigation to a random subset of `n` random classes. `n` must be a positive natural number. diff --git a/robot-command/src/main/java/org/obolibrary/robot/ExplainCommand.java b/robot-command/src/main/java/org/obolibrary/robot/ExplainCommand.java index ec2558470..57796b707 100644 --- a/robot-command/src/main/java/org/obolibrary/robot/ExplainCommand.java +++ b/robot-command/src/main/java/org/obolibrary/robot/ExplainCommand.java @@ -49,7 +49,7 @@ public class ExplainCommand implements Command { NS + "MISSING AXIOM ARGUMENT ERROR: must have a valid --axiom."; private static final String illegalUnsatisfiableArgumentError = NS - + "ILLEGAL UNSATISFIABLE ARGUMENT ERROR: %s. Must have either a valid --unsatisfiable option (all, root, random:n), where n is an integer."; + + "ILLEGAL UNSATISFIABLE ARGUMENT ERROR: %s. Must have either a valid --unsatisfiable option (all, root, most_general, random:n), where n is an integer."; /** Store the command-line options for the command. */ private Options options; @@ -170,6 +170,11 @@ private Set> handleUnsatisfiableMode( explanations.addAll( ExplainOperation.explainRootUnsatisfiableClasses(ontology, r, reasonerFactory, max)); break; + case "most_general": + explanations.addAll( + ExplainOperation.explainMostGeneralUnsatisfiableClasses( + ontology, r, reasonerFactory, max)); + break; case "list": handleListMode(line, r); listmode = true; @@ -293,7 +298,11 @@ private void writeExplanationsToFile( String summary = ExplainOperation.renderAxiomImpactSummary(mapMostUsedAxioms, ontology, man); Writer writer = Files.newBufferedWriter(output.toPath(), StandardCharsets.UTF_8); writer.write(result); - writer.write(summary); + if (!explanations.isEmpty()) { + writer.write(summary); + } else { + writer.write("No explanations found."); + } writer.close(); } diff --git a/robot-core/src/main/java/org/obolibrary/robot/ExplainOperation.java b/robot-core/src/main/java/org/obolibrary/robot/ExplainOperation.java index 39e980988..51b2056e2 100644 --- a/robot-core/src/main/java/org/obolibrary/robot/ExplainOperation.java +++ b/robot-core/src/main/java/org/obolibrary/robot/ExplainOperation.java @@ -14,6 +14,7 @@ import org.semanticweb.owlapi.model.parameters.Imports; import org.semanticweb.owlapi.reasoner.OWLReasoner; import org.semanticweb.owlapi.reasoner.OWLReasonerFactory; +import org.semanticweb.owlapi.reasoner.structural.StructuralReasonerFactory; import org.semanticweb.owlapi.util.AnnotationValueShortFormProvider; import org.semanticweb.owlapi.util.ShortFormProvider; import org.slf4j.Logger; @@ -113,7 +114,8 @@ public static Set> explainUnsatisfiableClasses( } /** - * Compute explanations for all root unsatisfiable classes + * Compute explanations for all root unsatisfiable classes See + * https://github.com/matthewhorridge/owlexplanation/blob/439c5ca67835f5e421adde725e4e8a3bcd760ac8/src/main/java/org/semanticweb/owl/explanation/impl/rootderived/StructuralRootDerivedReasoner.java#L122 * * @param ontology the ontology to be tested * @param reasoner the reasoner to be used to determine the unsatisfiable classes @@ -131,6 +133,41 @@ public static Set> explainRootUnsatisfiableClasses( return getUnsatExplanationsForClasses(ontology, reasonerFactory, max, unsatisfiable_classes); } + /** + * Compute explanations for all most general unsatisfiable classes Note that this is a very naive + * implementation which assumes and acyclic class hierarchy. + * + * @param ontology the ontology to be tested + * @param reasoner the reasoner to be used to determine the unsatisfiable classes + * @param reasonerFactory the reasoner factory to be used to compute the explanations + * @param max maximum number of explanations to be computed + * @return a set of explanations + */ + public static Set> explainMostGeneralUnsatisfiableClasses( + OWLOntology ontology, OWLReasoner reasoner, OWLReasonerFactory reasonerFactory, int max) { + List unsatisfiable_classes = + new ArrayList<>(getMostGeneralUnsatisfiableClasses(reasoner, ontology)); + return getUnsatExplanationsForClasses(ontology, reasonerFactory, max, unsatisfiable_classes); + } + + private static Set getMostGeneralUnsatisfiableClasses( + OWLReasoner reasoner, OWLOntology ontology) { + Set mgu = new HashSet<>(); + OWLReasoner structural = new StructuralReasonerFactory().createReasoner(ontology); + Set unsats = + new HashSet<>(reasoner.getUnsatisfiableClasses().getEntitiesMinusBottom()); + for (OWLClass c : unsats) { + Set superclasses = structural.getSuperClasses(c, false).getFlattened(); + superclasses.retainAll(unsats); + if (superclasses.isEmpty()) { + // If there is no superclass in the ontology according to the structural reasoner which is + // also unsatisfiable, we consider C a "most general unsatisfiable class". + mgu.add(c); + } + } + return mgu; + } + /** * Render an Explanation object as Markdown text, linking text labels to term IRIs and indenting * axioms. @@ -277,7 +314,7 @@ private static String renderAxiomWithImpact( + renderer.render(ax) + " [" + String.join(",", associatedOntologyIds.get(ax)) - + "]ยง\n"); + + "]\n"); } builder.append("\n"); return builder.toString(); diff --git a/robot-core/src/test/java/org/obolibrary/robot/ExplainOperationTest.java b/robot-core/src/test/java/org/obolibrary/robot/ExplainOperationTest.java index c125d15eb..b6adb85b5 100644 --- a/robot-core/src/test/java/org/obolibrary/robot/ExplainOperationTest.java +++ b/robot-core/src/test/java/org/obolibrary/robot/ExplainOperationTest.java @@ -54,7 +54,22 @@ public void testExplainInconsistentOntology() throws Exception { } /** - * Test explaining inconsistent ontology. + * Test explaining most general unsatisfiable classes. + * + * @throws Exception on any problem + */ + @Test + public void testExplainMostGeneralUnsatisfiableClasses() throws Exception { + OWLOntology ontology = loadOntology(ONT_UNSAT); + OWLReasonerFactory factory = new ReasonerFactory(); + OWLReasoner r = factory.createReasoner(ontology); + Set> explanations = + ExplainOperation.explainMostGeneralUnsatisfiableClasses(ontology, r, factory, 1); + assertEquals(explanations.size(), 3); + } + + /** + * Test explaining root unsatisfiable classes . * * @throws Exception on any problem */