Package net.sf.tweety.logics.pl.sat
Class OpenWboSolver
- java.lang.Object
-
- net.sf.tweety.logics.pl.sat.SatSolver
-
- net.sf.tweety.logics.pl.sat.MaxSatSolver
-
- net.sf.tweety.logics.pl.sat.OpenWboSolver
-
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,?>>
,ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
public class OpenWboSolver extends MaxSatSolver
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
Constructors Constructor Description OpenWboSolver(java.lang.String binaryLocation)
Creates a new solver based on the open-wbo executable given as a parameter.
-
Method Summary
Modifier and Type Method Description Interpretation<PlBeliefSet,PlFormula>
getWitness(java.util.Collection<PlFormula> hardConstraints, java.util.Map<PlFormula,java.lang.Integer> softConstraints)
Returns an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)-
Methods inherited from class net.sf.tweety.logics.pl.sat.MaxSatSolver
costOf, getWitness, isSatisfiable, setTempFolder
-
Methods inherited from class net.sf.tweety.logics.pl.sat.SatSolver
convertToDimacs, convertToDimacs, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver
-
-
-
-
Method Detail
-
getWitness
public Interpretation<PlBeliefSet,PlFormula> getWitness(java.util.Collection<PlFormula> hardConstraints, java.util.Map<PlFormula,java.lang.Integer> softConstraints)
Description copied from class:MaxSatSolver
Returns an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)- Specified by:
getWitness
in classMaxSatSolver
- 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)
-
-