Package org.tweetyproject.logics.pl.sat

Class CmdLineSatSolver

java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
org.tweetyproject.logics.pl.sat.DimacsSatSolver
org.tweetyproject.logics.pl.sat.CmdLineSatSolver
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
public class CmdLineSatSolver extends DimacsSatSolver
This class offers a generic wrapper for command line based SAT solvers. It is likely to work for most solvers that use the Dimacs format, e.g. most solvers presented at SAT solver competitions. Tested with the following solvers:
Author:
Anna Gessler

  • Constructor Details

    • CmdLineSatSolver

      public CmdLineSatSolver(String binaryLocation)
      Creates a new SAT solver based on the given binary location.
      Parameters:
      binaryLocation - the location of the binary

  • Method Details

    • getWitness

      public 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)
      Description copied from class: DimacsSatSolver
      If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
      Specified by:
      getWitness in class DimacsSatSolver
      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, Map<Proposition,Integer> prop_index, String additional_clauses, int num_additional_clauses)
      Description copied from class: DimacsSatSolver
      Checks whether the given set of formulas is satisfiable.
      Specified by:
      isSatisfiable in class DimacsSatSolver
      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.

    • addOption

      public void addOption(String option)
      Adds a single command line parameter. Needs to be in the correct format, usually in the form "--opt". Note: Available options can be found in the manuals of the respective solvers.
      Parameters:
      option - string

    • setOptions

      public void setOptions(String options)
      Sets the options parameter of the sat solver. Needs to be in the correct format, usually in the form "--opt1 --opt2", with spaces between different options. This replaces the whole options string, replacing any previously added parameters or default parameters. Note: Available options can be found in the manuals of the respective solvers.
      Parameters:
      options - string of options

    • isInstalled

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