org.sat4j.minisat.orders
Class PhaseInLastLearnedClauseSelectionStrategy

java.lang.Object
  org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy

All Implemented Interfaces:

Serializable, IPhaseSelectionStrategy

public final class PhaseInLastLearnedClauseSelectionStrategy
extends Object

Keeps record of the phase of a variable in the lastest recorded clause.

Author:

leberre

See Also:

Serialized Form

Field Summary

protected int[]

phase

Constructor Summary

PhaseInLastLearnedClauseSelectionStrategy()

Method Summary

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.
String	toString()
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.

Methods inherited from class java.lang.Object

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

Field Detail

phase

protected int[] phase

Constructor Detail

PhaseInLastLearnedClauseSelectionStrategy

public PhaseInLastLearnedClauseSelectionStrategy()

Method Detail

updateVar

public void updateVar(int p)

Description copied from interface: IPhaseSelectionStrategy

To be called when the activity of a literal changed.

Parameters:

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

toString

public String toString()

Overrides:

toString in class Object

assignLiteral

public void assignLiteral(int p)

Description copied from interface: IPhaseSelectionStrategy

indicate that a literal has been satisfied.

updateVarAtDecisionLevel

public void updateVarAtDecisionLevel(int q)

Description copied from interface: IPhaseSelectionStrategy

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

Parameters:

q - a literal

init

public void init(int nlength)

Description copied from interface: IPhaseSelectionStrategy

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

Specified by:

init in interface IPhaseSelectionStrategy

Parameters:

nlength - the number of variables managed by the heuristics.

init

public void init(int var,
                 int p)

Description copied from interface: IPhaseSelectionStrategy

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

Specified by:

init in interface IPhaseSelectionStrategy

Parameters:

var - a variable

p - it's initial phase

select

public int select(int var)

Description copied from interface: IPhaseSelectionStrategy

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

Specified by:

select in interface IPhaseSelectionStrategy

Parameters:

var - a variable chosen by the heuristics

Returns:

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