Package org.tweetyproject.logics.pl.sat

Class PlMusEnumerator

java.lang.Object

org.tweetyproject.logics.commons.analysis.AbstractMusEnumerator<PlFormula>

org.tweetyproject.logics.pl.sat.PlMusEnumerator

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, MusEnumerator<PlFormula>

Direct Known Subclasses:

MarcoMusEnumerator, MimusMusEnumerator

public abstract class PlMusEnumerator
extends AbstractMusEnumerator<PlFormula>

This abstract class models a MUS enumerator for propositional logic, i.e. an approach that lists all minimal unsatisfiable subsets of a given set of formulas. It also provides some static methods for accessing a centrally configured default MUS enumerator.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
PlMusEnumerator()	Default Constructor

Method Summary

Modifier and Type	Method	Description
static Pair<String,List<PlFormula>>	convertToDimacsAndIndex(Collection<PlFormula> formulas)	Converts the given set of formulas to their string representation in Dimacs CNF.
static AbstractMusEnumerator<PlFormula>	getDefaultEnumerator()	Returns the default MUS enumerator. If a default MUS enumerator has been configured this enumerator is returned by this method.
static boolean	hasDefaultEnumerator()	Returns "true" if a default MUS enumerator is configured.
abstract Collection<Collection<PlFormula>>	minimalInconsistentSubsets(Collection<PlFormula> formulas)	This method returns the minimal inconsistent subsets of the given set of formulas.
static void	setDefaultEnumerator(AbstractMusEnumerator<PlFormula> enumerator)	Sets the default MUS enumerator.

Methods inherited from class org.tweetyproject.logics.commons.analysis.AbstractMusEnumerator

getMiComponents, isConsistent, isConsistent, isConsistent, maximalConsistentSubsets, minimalCorrectionSubsets

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.tweetyproject.logics.commons.analysis.MusEnumerator

isInstalled

Constructor Details

PlMusEnumerator

public PlMusEnumerator()

Default Constructor

Method Details

setDefaultEnumerator

public static void setDefaultEnumerator(AbstractMusEnumerator<PlFormula> enumerator)

Sets the default MUS enumerator.

Parameters:

enumerator - some MUS enumerator

hasDefaultEnumerator

public static boolean hasDefaultEnumerator()

Returns "true" if a default MUS enumerator is configured.

Returns:

"true" if a default MUS enumerator is configured.

convertToDimacsAndIndex

public static Pair<String,List<PlFormula>> convertToDimacsAndIndex(Collection<PlFormula> formulas)

Converts the given set of formulas to their string representation in Dimacs CNF. The return value is a pair of
1.) the string representation
2.) a list of collections of formulas (all from the given set); the interpretation of this list is that the generated clause no K originated from the propositional formula given at index k.

Parameters:

formulas - a collection of formulas.

Returns:

a string in Dimacs CNF and a mapping between clauses and original formulas.

getDefaultEnumerator

public static AbstractMusEnumerator<PlFormula> getDefaultEnumerator()

Returns the default MUS enumerator.

If a default MUS enumerator has been configured this enumerator is returned by this method. If no default MUS enumerator is configured, a naive enumerator based on the default SAT solver is returned as a fallback and a message is printed to stderr pointing out that no default MUS enumerator is configured.

Returns:

the default MUS enumerator.

minimalInconsistentSubsets

public abstract Collection<Collection<PlFormula>> minimalInconsistentSubsets(Collection<PlFormula> formulas)

Description copied from interface: MusEnumerator

This method returns the minimal inconsistent subsets of the given set of formulas.

Specified by:

minimalInconsistentSubsets in interface MusEnumerator<PlFormula>

Specified by:

minimalInconsistentSubsets in class AbstractMusEnumerator<PlFormula>

Parameters:

formulas - a set of formulas.

Returns:

the minimal inconsistent subsets of the given set of formulas