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>

public class OpenWboSolver
extends DimacsMaxSatSolver

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, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)	Return the interpetation
boolean	isInstalled()	Return whether the solve ris installed
boolean	isSatisfiable(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index)	Return "true" if the set is consistent.

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

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,
 Map<Proposition,Integer> prop_index,
 Map<Integer,Proposition> prop_inverted_index)

Description copied from class: DimacsMaxSatSolver

Return the interpetation

Specified by:

getWitness in class DimacsMaxSatSolver

Parameters:

hardConstraints - hard constraints for interpretation

softConstraints - soft constraints for interpretation

prop_index - the index

prop_inverted_index - inverted index

Returns:

the interpetation

isInstalled

public boolean isInstalled()

Description copied from class: SatSolver

Return whether the solve ris installed

Specified by:

isInstalled in class SatSolver

Returns:

whether the solve ris installed

isSatisfiable

public boolean isSatisfiable(Collection<PlFormula> formulas,
 Map<Proposition,Integer> prop_index)

Description copied from class: DimacsMaxSatSolver

Return "true" if the set is consistent.

Specified by:

isSatisfiable in class DimacsMaxSatSolver

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.