Class MaxSatSolver

java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
org.tweetyproject.logics.pl.sat.MaxSatSolver
All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
Direct Known Subclasses:
DimacsMaxSatSolver

public abstract class MaxSatSolver extends SatSolver
Provides a generic class for implementing MaxSAT solvers, i.e. solvers that get as input a set of hard constraints (=propositional formulas that need to be satisfied) and a set of soft constraints (=clauses with weights) whose satisfaction should be maximized (=sum of weights should be maximized).
Author:
Matthias Thimm
  • Constructor Details

    • MaxSatSolver

      public MaxSatSolver()
  • Method Details

    • getWitness

      public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)
      Returns an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)
      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)
    • isSatisfiable

      public abstract 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.
    • costOf

      public static int costOf(Interpretation<PlBeliefSet,PlFormula> interpretation, Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)
      Returns the cost of the given interpretation, i.e. the sum of the weights of all violated soft constraints. If the interpretation does not satisfy the hard constraints -1 is returned;
      Parameters:
      interpretation - some interpretation
      hardConstraints - a set of hard constraints
      softConstraints - a set of soft constraints
      Returns:
      the cost of the interpretation