org.kahina.logic.sat.muc.heuristics

Class ReductionHeuristic

java.lang.Object

org.kahina.logic.sat.muc.heuristics.ReductionHeuristic

Direct Known Subclasses:

AscendingIndexHeuristic, AscendingRelevanceHeuristic, CenteredIndexHeuristic, CenteredRelevanceHeuristic, DescendingIndexHeuristic, DescendingRelevanceHeuristic, SingleStepHeuristic

public abstract class ReductionHeuristic
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
protected MUCStep	uc

Constructor Summary

Constructors

Constructor and Description
ReductionHeuristic()

Method Summary

Methods

Modifier and Type	Method and Description
void	deliverCriticalClauses(java.util.Set<java.lang.Integer> criticalClauses) Does nothing by default
void	deliverProof(ResolutionProofTree proof) Is called by the reduction agent to hand on proof trees to the heuristic for complex calculations, if usesProofs() is defined to return true.
java.lang.String	getName() Defines the name of the heuristic as displayed in the reduction agent system.
abstract int	getNextCandidate() Is used by the reduction agent steered by this heuristic to poll reduction candidates.
boolean	needsProof()
void	setNewUC(MUCStep uc)
void	setSelVarOffset(int selVarOffset)
boolean	usesProofs() Determines whether the heuristic wants to be informed about

Methods inherited from class java.lang.Object

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

Field Detail

uc

protected MUCStep uc

Constructor Detail

ReductionHeuristic

public ReductionHeuristic()

Method Detail

setSelVarOffset

public void setSelVarOffset(int selVarOffset)

setNewUC

public void setNewUC(MUCStep uc)

needsProof

public boolean needsProof()

Returns:

usesProofs

public boolean usesProofs()

Determines whether the heuristic wants to be informed about

Returns:

deliverProof

public void deliverProof(ResolutionProofTree proof)

Is called by the reduction agent to hand on proof trees to the heuristic for complex calculations, if usesProofs() is defined to return true.

Parameters:

proof -

deliverCriticalClauses

public void deliverCriticalClauses(java.util.Set<java.lang.Integer> criticalClauses)

Does nothing by default

Parameters:

criticalClauses -

getNextCandidate

public abstract int getNextCandidate()

Is used by the reduction agent steered by this heuristic to poll reduction candidates. This is the main interface for defining a heuristic, and it may depend on arbitrarily complex internal calculations. This method is abstract, so that every heuristic needs to implement it.

Returns:

the next reduction candidate to be tried, -1 to terminate.

getName

public java.lang.String getName()

Defines the name of the heuristic as displayed in the reduction agent system.

Returns:

the name of the heuristic.