Package org.tweetyproject.logics.pl.sat

Class SatSolver

    • Constructor Summary

      Constructors 
      Constructor Description
      SatSolver()  

    • Method Summary

      Modifier and Type Method Description
      static Pair<java.lang.String,​java.util.List<PlFormula>> convertToDimacs​(java.util.Collection<PlFormula> formulas)
      Converts the given set of formulas to their string representation in Dimacs CNF.
      static java.lang.String convertToDimacs​(java.util.Collection<PlFormula> formulas, java.util.List<Proposition> props)
      Converts the given set of formulas to their string representation in Dimacs CNF.
      static SatSolver getDefaultSolver()
      Returns the default SAT solver.

      If a default SAT solver has been configured this solver is returned by this method.
      abstract Interpretation<PlBeliefSet,​PlFormula> getWitness​(java.util.Collection<PlFormula> formulas)
      If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
      Interpretation<PlBeliefSet,​PlFormula> getWitness​(BeliefSet<PlFormula,​?> bs)
      If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
      Interpretation<PlBeliefSet,​PlFormula> getWitness​(PlFormula formula)
      If the formula is consistent this method returns some model of it or, if it is inconsistent, null.
      static boolean hasDefaultSolver()
      Returns "true" if a default SAT solver is configured.
      boolean isConsistent​(java.util.Collection<PlFormula> formulas)
      Checks whether the given collection of formulas is consistent.
      boolean isConsistent​(BeliefSet<PlFormula,​?> beliefSet)
      Checks whether the given belief base is consistent.
      boolean isConsistent​(PlFormula formula)
      Checks whether the given formula is consistent.
      abstract boolean isSatisfiable​(java.util.Collection<PlFormula> formulas)
      Checks whether the given set of formulas is satisfiable.
      static void setDefaultSolver​(SatSolver solver)
      Sets the default SAT solver.
      static void setTempFolder​(java.io.File tempFolder)
      Set the folder for temporary files created by SAT solver.

      • Methods inherited from class java.lang.Object

        equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

    • Constructor Detail

      • SatSolver

        public SatSolver()

    • Method Detail

      • setDefaultSolver

        public static void setDefaultSolver​(SatSolver solver)
        Sets the default SAT solver.
        Parameters:
        solver - some SAT solver

      • setTempFolder

        public static void setTempFolder​(java.io.File tempFolder)
        Set the folder for temporary files created by SAT solver.
        Parameters:
        tempFolder - some temp folder.

      • hasDefaultSolver

        public static boolean hasDefaultSolver()
        Returns "true" if a default SAT solver is configured.
        Returns:
        "true" if a default SAT solver is configured.

      • getDefaultSolver

        public static SatSolver getDefaultSolver()
        Returns the default SAT solver.

        If a default SAT solver has been configured this solver is returned by this method. If no default solver is configured, the Sat4j solver (org.tweetyproject.pl.sat.Sat4jSolver) is returned as a fallback and a message is printed to stderr pointing out that no default SAT solver is configured.
        Returns:
        the default SAT solver.

      • convertToDimacs

        public static java.lang.String convertToDimacs​(java.util.Collection<PlFormula> formulas,
                                               java.util.List<Proposition> props)
        Converts the given set of formulas to their string representation in Dimacs CNF. Note that a single formula may be represented as multiple clauses, so there is no simple correspondence between the formulas of the set and the Dimacs representation. Use convertToDimacs(.) for obtaining a map between those.
        Parameters:
        formulas - a collection of formulas
        props - a list of propositions (=signature) where the indices are used for writing the clauses.
        Returns:
        a string in Dimacs CNF.

      • convertToDimacs

        public static Pair<java.lang.String,​java.util.List<PlFormula>> convertToDimacs​(java.util.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.

      • isSatisfiable

        public abstract boolean isSatisfiable​(java.util.Collection<PlFormula> formulas)
        Checks whether the given set of formulas is satisfiable.
        Parameters:
        formulas - a set of formulas.
        Returns:
        "true" if the set is consistent.

      • isConsistent

        public boolean isConsistent​(java.util.Collection<PlFormula> formulas)
        Description copied from interface: BeliefSetConsistencyTester
        Checks whether the given collection of formulas is consistent.
        Specified by:
        isConsistent in interface BeliefSetConsistencyTester<PlFormula>
        Parameters:
        formulas - a collection of formulas.
        Returns:
        "true" iff the given collection of formulas is consistent.