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

Field Summary

Fields

Modifier and Type	Field	Description
private static java.io.File	tempFolder	For temporary files.

Constructor Summary

Constructors

Constructor	Description
MaxSatSolver()

Method Summary

Modifier and Type	Method	Description
protected static java.lang.String	convertToDimacsWcnf(java.util.Collection<PlFormula> hardConstraints, java.util.Map<PlFormula,java.lang.Integer> softConstraints, java.util.List<Proposition> props)	Converts the given MaxSAT instance (i.e.
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.
protected static java.io.File	createTmpDimacsWcnfFile(java.util.Collection<PlFormula> hardConstraints, java.util.Map<PlFormula,java.lang.Integer> softConstraints, java.util.List<Proposition> props)	Converts the given MaxSAT instance (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, createTmpDimacsFile, createTmpDimacsFile, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver

Methods inherited from class java.lang.Object

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

Field Detail

tempFolder

private static java.io.File tempFolder

For temporary files.

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.

convertToDimacsWcnf

protected static java.lang.String convertToDimacsWcnf(java.util.Collection<PlFormula> hardConstraints,
                                                      java.util.Map<PlFormula,java.lang.Integer> softConstraints,
                                                      java.util.List<Proposition> props)
                                               throws java.lang.IllegalArgumentException

Converts the given MaxSAT instance (i.e. hard and soft constraints, the latter can only be clauses) to their string representation in Dimacs WCNF. Note that a single formula may be represented as multiple clauses, so there is no simple correspondence between the formulas of the set and the Dimacs representation.

Parameters:

hardConstraints - a collection of formulas

softConstraints - a map mapping clauses to weights

props - a list of propositions (=signature) where the indices are used for writing the clauses.

Returns:

a string in Dimacs CNF.

Throws:

java.lang.IllegalArgumentException - if any soft constraint is not a clause.

createTmpDimacsWcnfFile

protected static java.io.File createTmpDimacsWcnfFile(java.util.Collection<PlFormula> hardConstraints,
                                                      java.util.Map<PlFormula,java.lang.Integer> softConstraints,
                                                      java.util.List<Proposition> props)
                                               throws java.io.IOException

Converts the given MaxSAT instance (i.e. hard and soft constraints, the latter can only be clauses) to their string representation in Dimacs WCNF and writes it to a temporary file. Note that a single formula may be represented as multiple clauses, so there is no simple correspondence between the formulas of the set and the Dimacs representation.

Parameters:

hardConstraints - a collection of formulas

softConstraints - a map mapping clauses to weights

props - a list of propositions (=signature) where the indices are used for writing the clauses.

Returns:

a string in Dimacs CNF.

Throws:

java.io.IOException - if some file issue occurs

java.lang.IllegalArgumentException - if any soft constraint is not a clause.

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