Package org.tweetyproject.logics.pl.sat

Class SatSolver

java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
Direct Known Subclasses:
CmdLineSatSolver, MaxSatSolver, Sat4jSolver, SimpleDpllSolver
public abstract class SatSolver extends Object implements BeliefSetConsistencyTester<PlFormula>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
Abstract class for specifying SAT solvers. Also includes methods to convert knowledge bases into the Dimacs format.
Author:
Matthias Thimm

  • Constructor Details

    • SatSolver

      public SatSolver()

  • Method Details

    • setDefaultSolver

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

    • setTempFolder

      public static void setTempFolder(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 String convertToDimacs(Collection<PlFormula> formulas, 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<String,List<PlFormula>> convertToDimacs(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.

    • getWitness

      public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> formulas)
      If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
      Specified by:
      getWitness in interface ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
      Parameters:
      formulas - a set of formulas
      Returns:
      some model of the formulas or null.

    • isSatisfiable

      public abstract boolean isSatisfiable(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(BeliefSet<PlFormula,?> beliefSet)
      Description copied from interface: ConsistencyTester
      Checks whether the given belief base is consistent.
      Specified by:
      isConsistent in interface BeliefSetConsistencyTester<PlFormula>
      Specified by:
      isConsistent in interface ConsistencyTester<BeliefSet<PlFormula,?>>
      Parameters:
      beliefSet - a belief base.
      Returns:
      "true" iff the given belief base is consistent.

    • isConsistent

      public boolean isConsistent(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.

    • isConsistent

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

    • getWitness

      public Interpretation<PlBeliefSet,PlFormula> getWitness(PlFormula formula)
      Description copied from interface: ConsistencyWitnessProvider
      If the formula is consistent this method returns some model of it or, if it is inconsistent, null.
      Specified by:
      getWitness in interface ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
      Parameters:
      formula - a formula
      Returns:
      some model of the formula or null.

    • getWitness

      public Interpretation<PlBeliefSet,PlFormula> getWitness(BeliefSet<PlFormula,?> bs)
      Description copied from interface: ConsistencyWitnessProvider
      If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
      Specified by:
      getWitness in interface ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
      Parameters:
      bs - a belief set
      Returns:
      some model of the belief set or null.

    • isInstalled

      public abstract boolean isInstalled()