org.kahina.logic.sat.muc.task

Class ReductionTask

java.lang.Object

org.kahina.core.task.KahinaTask

org.kahina.logic.sat.muc.task.ReductionTask

All Implemented Interfaces:

java.lang.Runnable

public class ReductionTask
extends KahinaTask

Field Summary

Fields

Modifier and Type	Field and Description
java.util.List<java.lang.Integer>	candidates
static int	idCounter
int	reductionID
MUCStep	uc
int	ucID

Constructor Summary

Constructors

Constructor and Description
ReductionTask(KahinaProgressBar progressBar, KahinaTaskManager manager, MUCStatistics stat, MUCStep uc, int ucID, java.util.List<java.lang.Integer> candidates, MiniSATFiles files, CnfSatInstance instance)
ReductionTask(KahinaProgressBar progressBar, KahinaTaskManager manager, MUCStatistics stat, MUCStep uc, int ucID, java.util.List<java.lang.Integer> candidates, MUCStep result, CnfSatInstance instance) Construct a pseudo-reduction task for a known outcome which simply retrieves a result step.

Method Summary

Methods

Modifier and Type	Method and Description
CompleteAssignment	getModel()
static int	getNextID()
MUCStep	getResult() Retrieve the MUCStep resulting from the reduction (attempt)
boolean	isDummyTask()
void	run()
void	setAutarkyReduction(boolean autarkyReduction)
void	setClauseSetRefinement(boolean clauseSetRefinement)
void	setModelRotation(boolean modelRotation)
java.lang.String	toString()
boolean	usesAutarkyReduction()
boolean	usesClauseSetRefinement()
boolean	usesModelRotation()

Methods inherited from class org.kahina.core.task.KahinaTask

isCanceled, isFinished, setCanceled, setFinished, setProgressAndStatus

Methods inherited from class java.lang.Object

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

Field Detail

idCounter

public static int idCounter

reductionID

public final int reductionID

uc

public final MUCStep uc

ucID

public final int ucID

candidates

public final java.util.List<java.lang.Integer> candidates

Constructor Detail

ReductionTask

public ReductionTask(KahinaProgressBar progressBar,
             KahinaTaskManager manager,
             MUCStatistics stat,
             MUCStep uc,
             int ucID,
             java.util.List<java.lang.Integer> candidates,
             MUCStep result,
             CnfSatInstance instance)

Construct a pseudo-reduction task for a known outcome which simply retrieves a result step.

Parameters:

progressBar -

reducer -

uc -

ucID -

candidate -

ReductionTask

public ReductionTask(KahinaProgressBar progressBar,
             KahinaTaskManager manager,
             MUCStatistics stat,
             MUCStep uc,
             int ucID,
             java.util.List<java.lang.Integer> candidates,
             MiniSATFiles files,
             CnfSatInstance instance)

Method Detail

getNextID

public static int getNextID()

usesClauseSetRefinement

public boolean usesClauseSetRefinement()

setClauseSetRefinement

public void setClauseSetRefinement(boolean clauseSetRefinement)

usesModelRotation

public boolean usesModelRotation()

setModelRotation

public void setModelRotation(boolean modelRotation)

usesAutarkyReduction

public boolean usesAutarkyReduction()

setAutarkyReduction

public void setAutarkyReduction(boolean autarkyReduction)

isDummyTask

public boolean isDummyTask()

run

public void run()

getModel

public CompleteAssignment getModel()

Returns:

the model in case of a SAT result, if modelRotation is set; null otherwise

getResult

public MUCStep getResult()

Retrieve the MUCStep resulting from the reduction (attempt)

Returns:

a new MUCStep if the reduction was successful, otherwise the input step with an additional clause marked as irreducible

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object