OpenWboSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

org.tweetyproject.logics.pl.sat.MaxSatSolver

org.tweetyproject.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(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(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

isInstalled()

Methods inherited from class org.tweetyproject.logics.pl.sat.MaxSatSolver
costOf, getWitness, isSatisfiable, setTempFolder

Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver
convertToDimacs, convertToDimacs, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details
- OpenWboSolver
  
  public OpenWboSolver(String binaryLocation)
  
  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)
  
  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 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)
- isInstalled
  
  public boolean isInstalled()
  
  Specified by:
  
  isInstalled in class SatSolver