org.sat4j.minisat.core
Interface IOrder<L extends ILits>

All Known Implementing Classes:

JWOrder, MyOrder, PureOrder, VarOrder, VarOrderHeap, VarOrderHeapObjective, VarOrderHeapRsat

public interface IOrder<L extends ILits>

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.
void	init() that method has the responsibility to initialize all arrays in the heuristics.
void	newVar() Deprecated.
void	newVar(int howmany) Method called when Solver.newVar(int) is called.
void	printStat(java.io.PrintWriter out, java.lang.String prefix) Display statistics regarding the heuristics.
int	select() Selects the next "best" unassigned literal.
void	setLits(L lits) Method used to provide an easy access the the solver vocabulary.
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.
double	varActivity(int p) To obtain the current activity of a variable.
void	varDecayActivity() Decay the variables activities.

Method Detail

setLits

void setLits(L lits)

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

Parameters:

lits - the vocabulary

newVar

@Deprecated
void newVar()

Deprecated.

Method called each time Solver.newVar() is called.

newVar

void newVar(int howmany)

Method called when Solver.newVar(int) is called.

Parameters:

howmany - the maximum number of variables

See Also:

Solver.newVar(int)

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(java.io.PrintWriter out,
               java.lang.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 -