Package org.tweetyproject.logics.pl.sat
Class OpenWboSolver
java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
org.tweetyproject.logics.pl.sat.MaxSatSolver
org.tweetyproject.logics.pl.sat.DimacsMaxSatSolver
org.tweetyproject.logics.pl.sat.OpenWboSolver
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,
,?>> ConsistencyWitnessProvider<PlBeliefSet,
PlFormula>
Provides an interface to the open-wbo MaxSAT solver,
see https://github.com/sat-group/open-wbo.
Tested with open-wbo 2.1
- Author:
- Matthias Thimm
-
Constructor Summary
ConstructorDescriptionOpenWboSolver
(String binaryLocation) Creates a new solver based on the open-wbo executable given as a parameter. -
Method Summary
Modifier and TypeMethodDescriptiongetWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) boolean
boolean
isSatisfiable
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index) Methods inherited from class org.tweetyproject.logics.pl.sat.DimacsMaxSatSolver
getWitness, getWitness, isSatisfiable, setTempFolder
Methods inherited from class org.tweetyproject.logics.pl.sat.MaxSatSolver
costOf
Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver
getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver
-
Constructor Details
-
OpenWboSolver
Creates a new solver based on the open-wbo executable given as a parameter.- Parameters:
binaryLocation
- the path to the executable.
-
-
Method Details
-
getWitness
public Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) - Specified by:
getWitness
in classDimacsMaxSatSolver
- Parameters:
hardConstraints
- hard constraints for interpretationsoftConstraints
- soft constraints for interpretationprop_index
- the indexprop_inverted_index
- inverted index- Returns:
- the interpetation
-
isInstalled
public boolean isInstalled()- Specified by:
isInstalled
in classSatSolver
- Returns:
- whether the solve ris installed
-
isSatisfiable
- Specified by:
isSatisfiable
in classDimacsMaxSatSolver
- 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.
-