Added new option for unsats: most_general

see #686 (comment)

Another method for avoiding redundant explanations.

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.

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<Explanation<OWLAxiom>> 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();
   }
 

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<Explanation<OWLAxiom>> 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<Explanation<OWLAxiom>> 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<Explanation<OWLAxiom>> explainMostGeneralUnsatisfiableClasses(
+      OWLOntology ontology, OWLReasoner reasoner, OWLReasonerFactory reasonerFactory, int max) {
+    List<OWLClass> unsatisfiable_classes =
+        new ArrayList<>(getMostGeneralUnsatisfiableClasses(reasoner, ontology));
+    return getUnsatExplanationsForClasses(ontology, reasonerFactory, max, unsatisfiable_classes);
+  }
+
+  private static Set<OWLClass> getMostGeneralUnsatisfiableClasses(
+      OWLReasoner reasoner, OWLOntology ontology) {
+    Set<OWLClass> mgu = new HashSet<>();
+    OWLReasoner structural = new StructuralReasonerFactory().createReasoner(ontology);
+    Set<OWLClass> unsats =
+        new HashSet<>(reasoner.getUnsatisfiableClasses().getEntitiesMinusBottom());
+    for (OWLClass c : unsats) {
+      Set<OWLClass> 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();

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<Explanation<OWLAxiom>> explanations =
+        ExplainOperation.explainMostGeneralUnsatisfiableClasses(ontology, r, factory, 1);
+    assertEquals(explanations.size(), 3);
+  }
+
+  /**
+   * Test explaining root unsatisfiable classes .
    *
    * @throws Exception on any problem
    */