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:

DimacsMaxSatSolver

public abstract class MaxSatSolver
extends SatSolver

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

Constructors

Constructor	Description
MaxSatSolver()	Default Constructor

Method Summary

Modifier and Type	Method	Description
static int	costOf(Interpretation<PlBeliefSet,PlFormula> interpretation, Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)	Returns the cost of the given interpretation, i.e.
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)
abstract boolean	isSatisfiable(Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.

Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver

getDefaultSolver, getWitness, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, isInstalled, setDefaultSolver

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

MaxSatSolver

public MaxSatSolver()

Default Constructor

Method Details

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 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)

isSatisfiable

public abstract boolean isSatisfiable(Collection<PlFormula> formulas)

Description copied from class: SatSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class SatSolver

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 interpretation

hardConstraints - a set of hard constraints

softConstraints - a set of soft constraints

Returns:

the cost of the interpretation