org.sat4j.tools

Class AllMUSes

java.lang.Object

org.sat4j.tools.AllMUSes

public class AllMUSes
extends java.lang.Object

This is a tool for computing all the MUSes (Minimum Unsatisfiable Sets) of a set of clauses.

Since:

2.3.3

Author:

sroussel

Constructor Summary

Constructors

Constructor and Description
AllMUSes(ASolverFactory<? extends ISolver> factory)
AllMUSes(boolean group, ASolverFactory<? extends ISolver> factory)

Method Summary

Modifier and Type	Method and Description
java.util.List<IVecInt>	computeAllMSS()
java.util.List<IVecInt>	computeAllMSS(SolutionFoundListener listener)
java.util.List<IVecInt>	computeAllMSSOrdered(SolutionFoundListener listener)
java.util.List<IVecInt>	computeAllMUSes()
java.util.List<IVecInt>	computeAllMUSes(SolutionFoundListener listener) Computes all the MUSes associated to the set of constraints added to the solver
java.util.List<IVecInt>	computeAllMUSesOrdered(SolutionFoundListener listener)
java.util.List<IVecInt>	getMssList()
<T extends ISolver> T	getSolverInstance() Gets an instance of ISolver that can be used to compute all MUSes

Methods inherited from class java.lang.Object

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

Constructor Detail

AllMUSes

public AllMUSes(boolean group,
                ASolverFactory<? extends ISolver> factory)

AllMUSes

public AllMUSes(ASolverFactory<? extends ISolver> factory)

Method Detail

getSolverInstance

public <T extends ISolver> T getSolverInstance()

Gets an instance of ISolver that can be used to compute all MUSes

Returns:

the instance of ISolver to which the clauses will be added

computeAllMUSes

public java.util.List<IVecInt> computeAllMUSes()

computeAllMUSes

public java.util.List<IVecInt> computeAllMUSes(SolutionFoundListener listener)

Computes all the MUSes associated to the set of constraints added to the solver

Parameters:

solver - the ISolver that contains the set of clauses

Returns:

a list containing all the MUSes

computeAllMUSesOrdered

public java.util.List<IVecInt> computeAllMUSesOrdered(SolutionFoundListener listener)

computeAllMSS

public java.util.List<IVecInt> computeAllMSS()

computeAllMSS

public java.util.List<IVecInt> computeAllMSS(SolutionFoundListener listener)

computeAllMSSOrdered

public java.util.List<IVecInt> computeAllMSSOrdered(SolutionFoundListener listener)

getMssList

public java.util.List<IVecInt> getMssList()