Package net.sf.tweety.logics.pl.sat

Class MaxSatSolver

java.lang.Object

net.sf.tweety.logics.pl.sat.SatSolver

net.sf.tweety.logics.pl.sat.MaxSatSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Direct Known Subclasses:

OpenWboSolver

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

Method Summary

Modifier and Type	Method	Description
static int	costOf(Interpretation<PlBeliefSet,PlFormula> interpretation, java.util.Collection<PlFormula> hardConstraints, java.util.Map<PlFormula,java.lang.Integer> softConstraints)	Returns the cost of the given interpretation, i.e.
Interpretation<PlBeliefSet,PlFormula>	getWitness(java.util.Collection<PlFormula> formulas)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
abstract 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)
boolean	isSatisfiable(java.util.Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.
static void	setTempFolder(java.io.File tempFolder)	Set the folder for temporary files created by a MaxSAT solver.

Methods inherited from class net.sf.tweety.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 Detail

MaxSatSolver

public MaxSatSolver()

Method Detail

setTempFolder

public static void setTempFolder(java.io.File tempFolder)

Set the folder for temporary files created by a MaxSAT solver.

Parameters:

tempFolder - some temp folder.

getWitness

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

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)

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(java.util.Collection<PlFormula> formulas)

Description copied from class: SatSolver

If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.

Specified by:

getWitness in interface ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Specified by:

getWitness in class SatSolver

Parameters:

formulas - a set of formulas

Returns:

some model of the formulas or null.

isSatisfiable

public boolean isSatisfiable(java.util.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,
                         java.util.Collection<PlFormula> hardConstraints,
                         java.util.Map<PlFormula,java.lang.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