org.sat4j.minisat.core
Interface IOrder

All Known Implementing Classes:

PureOrder, RandomWalkDecorator, SubsetVarOrder, TabuListDecorator, VarOrderHeap

public interface IOrder

Interface for the variable ordering heuristics. It has both the responsibility to choose the next variable to branch on and the phase of the literal (positive or negative one).

Author:

daniel

Method Summary

void	assignLiteral(int p) indicate that a literal has been satisfied.
IPhaseSelectionStrategy	getPhaseSelectionStrategy()
double[]	getVariableHeuristics() Read-Only access to the value of the heuristics for each variable.
void	init() that method has the responsibility to initialize all arrays in the heuristics.
void	printStat(PrintWriter out, String prefix) Display statistics regarding the heuristics.
int	select() Selects the next "best" unassigned literal.
void	setLits(ILits lits) Method used to provide an easy access the the solver vocabulary.
void	setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy)
void	setVarDecay(double d) Sets the variable activity decay as a growing factor for the next variable activity.
void	undo(int x) Method called when a variable is unassigned.
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.
double	varActivity(int p) To obtain the current activity of a variable.
void	varDecayActivity() Decay the variables activities.

Method Detail

setLits

void setLits(ILits lits)

Method used to provide an easy access the the solver vocabulary.

Parameters:

lits - the vocabulary

select

int select()

Selects the next "best" unassigned literal. Note that it means selecting the best variable and the phase to branch on first.

Returns:

an unassigned literal or Lit.UNDEFINED no such literal exists.

undo

void undo(int x)

Method called when a variable is unassigned. It is useful to add back a variable in the pool of variables to order.

Parameters:

x - a variable.

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()

that method has the responsibility to initialize all arrays in the heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.

printStat

void printStat(PrintWriter out,
               String prefix)

Display statistics regarding the heuristics.

Parameters:

out - the writer to display the information in

prefix - to be used in front of each newline.

setVarDecay

void setVarDecay(double d)

Sets the variable activity decay as a growing factor for the next variable activity.

Parameters:

d - a number bigger than 1 that will increase the activity of the variables involved in future conflict. This is similar but more efficient than decaying all the activities by a similar factor.

varDecayActivity

void varDecayActivity()

Decay the variables activities.

varActivity

double varActivity(int p)

To obtain the current activity of a variable.

Parameters:

p - a literal

Returns:

the activity of the variable associated to that literal.

assignLiteral

void assignLiteral(int p)

indicate that a literal has been satisfied.

Parameters:

p -

setPhaseSelectionStrategy

void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy)

getPhaseSelectionStrategy

IPhaseSelectionStrategy getPhaseSelectionStrategy()

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

getVariableHeuristics

double[] getVariableHeuristics()

Read-Only access to the value of the heuristics for each variable. Note that for efficiency reason, the real array storing the value of the heuristics is returned. DO NOT CHANGE THE VALUES IN THAT ARRAY.

Returns:

the value of the heuristics for each variable (using Dimacs index).

Since:

2.3.2