Package org.tweetyproject.logics.pl.sat

Class DimacsMaxSatSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

org.tweetyproject.logics.pl.sat.MaxSatSolver

org.tweetyproject.logics.pl.sat.DimacsMaxSatSolver

All Implemented Interfaces:

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

Direct Known Subclasses:

OpenWboSolver

public abstract class DimacsMaxSatSolver
extends MaxSatSolver

Generic class for Dimacs-based MaxSAT solvers.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
DimacsMaxSatSolver()	Default Constructor

Method Summary

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

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, isInstalled, setDefaultSolver

Methods inherited from class java.lang.Object

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

Constructor Details

DimacsMaxSatSolver

public DimacsMaxSatSolver()

Default Constructor

Method Details

setTempFolder

public static void setTempFolder(File tempFolder)

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

Parameters:

tempFolder - some temp folder.

isSatisfiable

public boolean isSatisfiable(Collection<PlFormula> formulas)

Description copied from class: SatSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class MaxSatSolver

Parameters:

formulas - a set of formulas.

Returns:

"true" if the set is consistent.

isSatisfiable

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

Return "true" if the set is consistent.

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.

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> hardConstraints,
 Map<PlFormula,Integer> softConstraints)

interpretation of formulas

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)

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(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.

getWitness

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

Parameters:

hardConstraints - hard constraints for interpretation

softConstraints - soft constraints for interpretation

prop_index - the index

prop_inverted_index - inverted index

Returns:

the interpetation