Interface MusEnumerator<S extends Formula>
- Type Parameters:
S
- the type of formulas
- All Superinterfaces:
BeliefSetConsistencyTester<S>
,ConsistencyTester<BeliefSet<S,
?>>
- All Known Implementing Classes:
AbstractMusEnumerator
,MarcoMusEnumerator
,MimusMusEnumerator
,NaiveMusEnumerator
,PlMusEnumerator
Interface for classes enumerating MUSes (minimal unsatisfiable sets) and
MCSs (maximal consistent sets).
- Author:
- Matthias Thimm
-
Method Summary
Modifier and TypeMethodDescriptiongetMiComponents
(Collection<S> formulas) Computes the maximal (wrt.boolean
isConsistent
(Collection<S> formulas) Checks whether the given collection of formulas is consistent.boolean
isConsistent
(BeliefSet<S, ?> beliefSet) Checks whether the given belief base is consistent.boolean
isConsistent
(S formula) Checks whether the given formula is consistent.boolean
maximalConsistentSubsets
(Collection<S> formulas) This method returns the maximal consistent subsets of the given set of formulasminimalCorrectionSubsets
(Collection<S> formulas) This method returns the minimal correction subsets of the given set of formulas (i.e.minimalInconsistentSubsets
(Collection<S> formulas) This method returns the minimal inconsistent subsets of the given set of formulas.
-
Method Details
-
minimalInconsistentSubsets
This method returns the minimal inconsistent subsets of the given set of formulas.- Parameters:
formulas
- a set of formulas.- Returns:
- the minimal inconsistent subsets of the given set of formulas
-
maximalConsistentSubsets
This method returns the maximal consistent subsets of the given set of formulas- Parameters:
formulas
- a set of formulas- Returns:
- the maximal consistent subsets of the given set of formulas.
-
minimalCorrectionSubsets
This method returns the minimal correction subsets of the given set of formulas (i.e. the complements of maximal consistent subsets)- Parameters:
formulas
- a set of formulas- Returns:
- the minimal corrections subsets of the given set of formulas.
-
getMiComponents
Computes the maximal (wrt. cardinality) partitioning {K1,...,Kn} of K (ie. K is a disjoint union of K1,...,Kn) such that MI(K) is a disjoint union of MI(K1),...,MI(Kn).- Parameters:
formulas
- a set of formulas K- Returns:
- the MI components of K
-
isConsistent
Description copied from interface:ConsistencyTester
Checks whether the given belief base is consistent.- Specified by:
isConsistent
in interfaceBeliefSetConsistencyTester<S extends Formula>
- Specified by:
isConsistent
in interfaceConsistencyTester<S extends Formula>
- Parameters:
beliefSet
- a belief base.- Returns:
- "true" iff the given belief base is consistent.
-
isConsistent
Description copied from interface:BeliefSetConsistencyTester
Checks whether the given collection of formulas is consistent.- Specified by:
isConsistent
in interfaceBeliefSetConsistencyTester<S extends Formula>
- Parameters:
formulas
- a collection of formulas.- Returns:
- "true" iff the given collection of formulas is consistent.
-
isConsistent
Description copied from interface:BeliefSetConsistencyTester
Checks whether the given formula is consistent.- Specified by:
isConsistent
in interfaceBeliefSetConsistencyTester<S extends Formula>
- Parameters:
formula
- a formulas.- Returns:
- "true" iff the formula is consistent.
-
isInstalled
boolean isInstalled()- Returns:
- whether the consistency measure is installed
-