org.kahina.logic.sat.muc.heuristics

Class AscendingRelevanceHeuristic

java.lang.Object

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

org.kahina.logic.sat.muc.heuristics.AscendingRelevanceHeuristic

public class AscendingRelevanceHeuristic
extends ReductionHeuristic

Field Summary

Fields inherited from class org.kahina.logic.sat.muc.heuristics.ReductionHeuristic

uc

Constructor Summary

Constructors

Constructor and Description
AscendingRelevanceHeuristic()

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.
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

Constructor Detail

AscendingRelevanceHeuristic

public AscendingRelevanceHeuristic()

Method Detail

setSelVarOffset

public void setSelVarOffset(int selVarOffset)

Overrides:

setSelVarOffset in class ReductionHeuristic

setNewUC

public void setNewUC(MUCStep uc)

Overrides:

setNewUC in class ReductionHeuristic

needsProof

public boolean needsProof()

Overrides:

needsProof in class ReductionHeuristic

Returns:

usesProofs

public boolean usesProofs()

Description copied from class: ReductionHeuristic

Determines whether the heuristic wants to be informed about

Overrides:

usesProofs in class ReductionHeuristic

Returns:

deliverProof

public void deliverProof(ResolutionProofTree proof)

Description copied from class: ReductionHeuristic

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

Overrides:

deliverProof in class ReductionHeuristic

getNextCandidate

public int getNextCandidate()

Description copied from class: ReductionHeuristic

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.

Specified by:

getNextCandidate in class ReductionHeuristic

Returns:

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

deliverCriticalClauses

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

Description copied from class: ReductionHeuristic

Does nothing by default

Overrides:

deliverCriticalClauses in class ReductionHeuristic

getName

public java.lang.String getName()

Description copied from class: ReductionHeuristic

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

Overrides:

getName in class ReductionHeuristic

Returns:

the name of the heuristic.