Package org.tweetyproject.logics.pl.sat

Class CmdLineSatSolver

java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
org.tweetyproject.logics.pl.sat.CmdLineSatSolver
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
public class CmdLineSatSolver extends SatSolver
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)
      Description copied from class: SatSolver
      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.

    • isSatisfiable

      public boolean isSatisfiable(Collection<PlFormula> formulas)
      Description copied from class: SatSolver
      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.

    • 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 SatSolver