Package org.tweetyproject.logics.pl.sat

Class PlMusEnumerator

java.lang.Object
org.tweetyproject.logics.commons.analysis.AbstractMusEnumerator<PlFormula>
org.tweetyproject.logics.pl.sat.PlMusEnumerator
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, MusEnumerator<PlFormula>
Direct Known Subclasses:
MarcoMusEnumerator, MimusMusEnumerator
public abstract class PlMusEnumerator extends AbstractMusEnumerator<PlFormula>
This abstract class models a MUS enumerator for propositional logic, i.e. an approach that lists all minimal unsatisfiable subsets of a given set of formulas. It also provides some static methods for accessing a centrally configured default MUS enumerator.
Author:
Matthias Thimm

  • Constructor Details

    • PlMusEnumerator

      public PlMusEnumerator()

  • Method Details

    • setDefaultEnumerator

      public static void setDefaultEnumerator(AbstractMusEnumerator<PlFormula> enumerator)
      Sets the default MUS enumerator.
      Parameters:
      enumerator - some MUS enumerator

    • hasDefaultEnumerator

      public static boolean hasDefaultEnumerator()
      Returns "true" if a default MUS enumerator is configured.
      Returns:
      "true" if a default MUS enumerator is configured.

    • convertToDimacsAndIndex

      public static Pair<String,List<PlFormula>> convertToDimacsAndIndex(Collection<PlFormula> formulas)
      Converts the given set of formulas to their string representation in Dimacs CNF. The return value is a pair of
      1.) the string representation
      2.) a list of collections of formulas (all from the given set); the interpretation of this list is that the generated clause no K originated from the propositional formula given at index k.
      Parameters:
      formulas - a collection of formulas.
      Returns:
      a string in Dimacs CNF and a mapping between clauses and original formulas.

    • getDefaultEnumerator

      public static AbstractMusEnumerator<PlFormula> getDefaultEnumerator()
      Returns the default MUS enumerator.

      If a default MUS enumerator has been configured this enumerator is returned by this method. If no default MUS enumerator is configured, a naive enumerator based on the default SAT solver is returned as a fallback and a message is printed to stderr pointing out that no default MUS enumerator is configured.
      Returns:
      the default MUS enumerator.

    • minimalInconsistentSubsets

      public abstract Collection<Collection<PlFormula>> minimalInconsistentSubsets(Collection<PlFormula> formulas)
      Description copied from interface: MusEnumerator
      This method returns the minimal inconsistent subsets of the given set of formulas.
      Specified by:
      minimalInconsistentSubsets in interface MusEnumerator<PlFormula>
      Specified by:
      minimalInconsistentSubsets in class AbstractMusEnumerator<PlFormula>
      Parameters:
      formulas - a set of formulas.
      Returns:
      the minimal inconsistent subsets of the given set of formulas