org.kahina.logic.sat.insertionmus.algorithms

Class CombinedAlgorithm

java.lang.Object

org.kahina.logic.sat.insertionmus.algorithms.AbstractAlgorithm

org.kahina.logic.sat.insertionmus.algorithms.CombinedAlgorithm

public class CombinedAlgorithm
extends AbstractAlgorithm

Field Summary

Fields

Modifier and Type	Field and Description
protected CnfSatInstance	instance
protected java.util.TreeSet<java.lang.Integer>	instanceIDs
protected CnfSatInstance	mapInstance
protected java.util.TreeSet<java.lang.Integer>	Selection

Constructor Summary

Constructors

Constructor and Description
CombinedAlgorithm()

Method Summary

Methods

Modifier and Type	Method and Description
void	findAllMUS(AlgorithmData data) Implementation of the MARCO algorithm
CnfSatInstance	findAMuse(AlgorithmData data)
protected void	growSelection()
boolean	nextStep(int clauseIndex, AlgorithmData data)
protected void	shrink()

Methods inherited from class org.kahina.logic.sat.insertionmus.algorithms.AbstractAlgorithm

nextStep, solve, solve, solve

Methods inherited from class java.lang.Object

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

Field Detail

mapInstance

protected CnfSatInstance mapInstance

instance

protected CnfSatInstance instance

instanceIDs

protected java.util.TreeSet<java.lang.Integer> instanceIDs

Selection

protected java.util.TreeSet<java.lang.Integer> Selection

Constructor Detail

CombinedAlgorithm

public CombinedAlgorithm()

Method Detail

growSelection

protected void growSelection()
                      throws java.util.concurrent.TimeoutException,
                             java.lang.InterruptedException,
                             ResultNotRetrievableException

Throws:

java.util.concurrent.TimeoutException

java.lang.InterruptedException

ResultNotRetrievableException

shrink

protected void shrink()
               throws java.util.concurrent.TimeoutException,
                      java.lang.InterruptedException,
                      ResultNotRetrievableException

Throws:

java.util.concurrent.TimeoutException

java.lang.InterruptedException

ResultNotRetrievableException

findAllMUS

public void findAllMUS(AlgorithmData data)
                throws java.util.concurrent.TimeoutException,
                       java.lang.InterruptedException,
                       java.io.IOException,
                       ResultNotRetrievableException

Implementation of the MARCO algorithm

Throws:

java.lang.InterruptedException

java.util.concurrent.TimeoutException

java.io.IOException

ResultNotRetrievableException

findAMuse

public CnfSatInstance findAMuse(AlgorithmData data)

Overrides:

findAMuse in class AbstractAlgorithm

nextStep

public boolean nextStep(int clauseIndex,
               AlgorithmData data)

Specified by:

nextStep in class AbstractAlgorithm

Returns:

true if a new Step is reached.