Package org.tweetyproject.logics.pl.sat
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:
OpenWboSolver
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 Summary
-
Method Summary
Modifier and TypeMethodDescriptionstatic int
costOf(Interpretation<PlBeliefSet,PlFormula> interpretation, Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)
Returns the cost of the given interpretation, i.e.getWitness(Collection<PlFormula> formulas)
If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.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)boolean
isSatisfiable(Collection<PlFormula> formulas)
Checks whether the given set of formulas is satisfiable.static void
setTempFolder(File tempFolder)
Set the folder for temporary files created by a MaxSAT solver.Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver
convertToDimacs, convertToDimacs, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver
-
Constructor Details
-
MaxSatSolver
public MaxSatSolver()
-
-
Method Details
-
setTempFolder
Set the folder for temporary files created by a MaxSAT solver.- Parameters:
tempFolder
- some temp folder.
-
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 formulassoftConstraints
- 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
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 interfaceConsistencyWitnessProvider<PlBeliefSet,PlFormula>
- Specified by:
getWitness
in classSatSolver
- Parameters:
formulas
- a set of formulas- Returns:
- some model of the formulas or null.
-
isSatisfiable
Description copied from class:SatSolver
Checks whether the given set of formulas is satisfiable.- Specified by:
isSatisfiable
in classSatSolver
- 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 interpretationhardConstraints
- a set of hard constraintssoftConstraints
- a set of soft constraints- Returns:
- the cost of the interpretation
-