Package org.tweetyproject.logics.pl.sat

Class DimacsSatSolver

java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
org.tweetyproject.logics.pl.sat.DimacsSatSolver
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
Direct Known Subclasses:
CmdLineSatSolver, Sat4jSolver
public abstract class DimacsSatSolver extends SatSolver
Interface for SAT solvers which work on the Dimacs format. It adds some utility methods for directly manipulating clauses in Dimacs format.
Author:
Matthias Thimm

  • Constructor Details

    • DimacsSatSolver

      public DimacsSatSolver()

  • Method Details

    • setTempFolder

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

    • convertToDimacs

      public static String convertToDimacs(Collection<PlFormula> formulas)
      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.
      Parameters:
      formulas - a collection of formulas
      Returns:
      a string in Dimacs CNF.

    • convertToDimacs

      public static String convertToDimacs(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, String additional_clauses, int num_additional_clauses)
      Parameters:
      formulas - a collection of formulas
      prop_index - a map mapping propositions (=signature) to the indices that are used for writing the clauses.
      additional_clauses - additional clauses to be considered
      num_additional_clauses - number of additional clauses
      Returns:
      a string in Dimacs CNF.

    • getWitness

      public 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>
      Specified by:
      getWitness in class SatSolver
      Parameters:
      formulas - a set of formulas
      Returns:
      some model of the formulas or null.

    • getWitness

      public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index, String additional_clauses, int num_additional_clauses)
      If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
      Parameters:
      formulas - a set of formulas
      prop_index - mapping propositions to numbers used for representing the SAT instance
      prop_inverted_index - inverted index of prop_index
      additional_clauses - additional clauses in text form to be added (already correctly formatted in CNF!)
      num_additional_clauses - the number of additional_clauses
      Returns:
      some model of the formulas or null.

    • isSatisfiable

      public boolean isSatisfiable(Collection<PlFormula> formulas)
      Checks whether the given set of formulas is satisfiable.
      Specified by:
      isSatisfiable in class SatSolver
      Parameters:
      formulas - a set of formulas.
      Returns:
      "true" if the set is consistent.

    • isSatisfiable

      public abstract boolean isSatisfiable(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, String additional_clauses, int num_additional_clauses)
      Checks whether the given set of formulas is satisfiable.
      Parameters:
      formulas - a set of formulas.
      prop_index - maps propositions to the number that shall be used to represent it (a natural number > 0).
      additional_clauses - additional clauses in text form to be added (already correctly formatted in CNF!)
      num_additional_clauses - the number of additional_clauses
      Returns:
      "true" if the set is consistent.

    • isInstalled

      public abstract boolean isInstalled()
      Specified by:
      isInstalled in class SatSolver
      Returns:
      whether the solve ris installed