org.sat4j.minisat.core

Interface IPhaseSelectionStrategy

All Superinterfaces:

Serializable

All Known Implementing Classes:

NegativeLiteralSelectionStrategy, PhaseCachingAutoEraseStrategy, PhaseInLastLearnedClauseSelectionStrategy, PositiveLiteralSelectionStrategy, RandomLiteralSelectionStrategy, RSATLastLearnedClausesPhaseSelectionStrategy, RSATPhaseSelectionStrategy, UserFixedPhaseSelectionStrategy

public interface IPhaseSelectionStrategy
extends Serializable

The responsibility of that class is to choose the phase (positive or negative) of the variable that was selected by the IOrder.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
void	assignLiteral(int p) indicate that a literal has been satisfied.
void	init(int nlength) that method has the responsibility to initialize all arrays in the heuristics.
void	init(int var, int p) initialize the phase of a given variable to the given value.
int	select(int var) selects the phase of the variable according to a phase selection strategy.
void	updateVar(int p) To be called when the activity of a literal changed.
void	updateVarAtDecisionLevel(int q) Allow to perform a specific action when a literal of the current decision level is updated.

Method Detail

updateVar

void updateVar(int p)

To be called when the activity of a literal changed.

Parameters:

p - a literal. The associated variable will be updated.

init

void init(int nlength)

that method has the responsibility to initialize all arrays in the heuristics.

Parameters:

nlength - the number of variables managed by the heuristics.

init

void init(int var,
        int p)

initialize the phase of a given variable to the given value. That method is suppose to be called AFTER init(int).

Parameters:

var - a variable

p - it's initial phase

assignLiteral

void assignLiteral(int p)

indicate that a literal has been satisfied.

Parameters:

p -

select

int select(int var)

selects the phase of the variable according to a phase selection strategy.

Parameters:

var - a variable chosen by the heuristics

Returns:

either var or not var, depending of the selection strategy.

updateVarAtDecisionLevel

void updateVarAtDecisionLevel(int q)

Allow to perform a specific action when a literal of the current decision level is updated. That method is called after updateVar(int).

Parameters:

q - a literal