Class DimacsMaxSatSolver

All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
Direct Known Subclasses:
OpenWboSolver

public abstract class DimacsMaxSatSolver extends MaxSatSolver
Generic class for Dimacs-based MaxSAT solvers.
Author:
Matthias Thimm
  • Constructor Details

    • DimacsMaxSatSolver

      public DimacsMaxSatSolver()
  • Method Details

    • setTempFolder

      public static void setTempFolder(File tempFolder)
      Set the folder for temporary files created by a MaxSAT solver.
      Parameters:
      tempFolder - some temp folder.
    • 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 MaxSatSolver
      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)
      Parameters:
      formulas - a set of formulas.
      prop_index - maps propositions to the number that shall be used to represent it (a natural number > 0).
      Returns:
      "true" if the set is consistent.
    • getWitness

      public Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)
      interpretation of formulas
      Specified by:
      getWitness in class MaxSatSolver
      Parameters:
      hardConstraints - a set of propositional formulas
      softConstraints - a map mapping clauses to weights (if there is a formula, which is not a clause, i.e. a disjunction of literals), an exception is thrown.
      Returns:
      an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)
    • 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.
    • getWitness

      public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)
      Parameters:
      hardConstraints - hard constraints for interpretation
      softConstraints - soft constraints for interpretation
      prop_index - the index
      prop_inverted_index - inverted index
      Returns:
      the interpetation