Class SatSolver

    • Field Summary

      Fields 
      Modifier and Type Field Description
      private static SatSolver defaultSatSolver
      The default SAT solver.
      private static java.io.File tempFolder
      For temporary files.
    • 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.
      protected 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.
      protected static Pair<java.io.File,​java.util.List<PlFormula>> createTmpDimacsFile​(java.util.Collection<PlFormula> formulas)
      Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.
      protected static java.io.File createTmpDimacsFile​(java.util.Collection<PlFormula> formulas, java.util.List<Proposition> props)
      Creates a temporary file in Dimacs format with the given proposition2variable mapping.
      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

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Field Detail

      • defaultSatSolver

        private static SatSolver defaultSatSolver
        The default SAT solver.
      • tempFolder

        private static java.io.File tempFolder
        For temporary files.
    • 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 (net.sf.tweety.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

        protected 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.
      • createTmpDimacsFile

        protected static java.io.File createTmpDimacsFile​(java.util.Collection<PlFormula> formulas,
                                                          java.util.List<Proposition> props)
                                                   throws java.io.IOException
        Creates a temporary file in Dimacs format with the given proposition2variable mapping.
        Parameters:
        formulas - a collection of formulas
        props - a list of propositions (=signature) where the indices are used for writing the clauses.
        Returns:
        the file handler.
        Throws:
        java.io.IOException - if something went wrong while creating a temporary file.
      • createTmpDimacsFile

        protected static Pair<java.io.File,​java.util.List<PlFormula>> createTmpDimacsFile​(java.util.Collection<PlFormula> formulas)
                                                                                         throws java.io.IOException
        Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.
        Parameters:
        formulas - a collection of formulas
        Returns:
        the file handler and a mapping between clauses and original formulas.
        Throws:
        java.io.IOException - if something went wrong while creating a temporary file.
      • 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.