org.sat4j.minisat.orders
Class RandomWalkDecorator

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

All Implemented Interfaces:

IOrder

Direct Known Subclasses:

RandomWalkDecoratorObjective

public class RandomWalkDecorator
extends Object
implements IOrder

Since:

2.2

Constructor Summary

RandomWalkDecorator(VarOrderHeap order)

RandomWalkDecorator(VarOrderHeap order, double p)

Method Summary

void	assignLiteral(int q) indicate that a literal has been satisfied.
IPhaseSelectionStrategy	getPhaseSelectionStrategy()
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.
String	toString()
void	undo(int x) Method called when a variable is unassigned.
void	updateVar(int q) 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 q) To obtain the current activity of a variable.
void	varDecayActivity() Decay the variables activities.

Methods inherited from class java.lang.Object

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

Constructor Detail

RandomWalkDecorator

public RandomWalkDecorator(VarOrderHeap order)

RandomWalkDecorator

public RandomWalkDecorator(VarOrderHeap order,
                           double p)

Method Detail

assignLiteral

public void assignLiteral(int q)

Description copied from interface: IOrder

indicate that a literal has been satisfied.

Specified by:

assignLiteral in interface IOrder

getPhaseSelectionStrategy

public IPhaseSelectionStrategy getPhaseSelectionStrategy()

Specified by:

getPhaseSelectionStrategy in interface IOrder

init

public void init()

Description copied from interface: IOrder

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

Specified by:

init in interface IOrder

printStat

public void printStat(PrintWriter out,
                      String prefix)

Description copied from interface: IOrder

Display statistics regarding the heuristics.

Specified by:

printStat in interface IOrder

Parameters:

out - the writer to display the information in

prefix - to be used in front of each newline.

select

public int select()

Description copied from interface: IOrder

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

Specified by:

select in interface IOrder

Returns:

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

setLits

public void setLits(ILits lits)

Description copied from interface: IOrder

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

Specified by:

setLits in interface IOrder

Parameters:

lits - the vocabulary

setPhaseSelectionStrategy

public void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy)

Specified by:

setPhaseSelectionStrategy in interface IOrder

setVarDecay

public void setVarDecay(double d)

Description copied from interface: IOrder

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

Specified by:

setVarDecay in interface IOrder

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.

undo

public void undo(int x)

Description copied from interface: IOrder

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

Specified by:

undo in interface IOrder

Parameters:

x - a variable.

updateVar

public void updateVar(int q)

Description copied from interface: IOrder

To be called when the activity of a literal changed.

Specified by:

updateVar in interface IOrder

Parameters:

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

varActivity

public double varActivity(int q)

Description copied from interface: IOrder

To obtain the current activity of a variable.

Specified by:

varActivity in interface IOrder

Parameters:

q - a literal

Returns:

the activity of the variable associated to that literal.

varDecayActivity

public void varDecayActivity()

Description copied from interface: IOrder

Decay the variables activities.

Specified by:

varDecayActivity in interface IOrder

updateVarAtDecisionLevel

public void updateVarAtDecisionLevel(int q)

Description copied from interface: IOrder

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

Specified by:

updateVarAtDecisionLevel in interface IOrder

Parameters:

q - a literal

toString

public String toString()

Overrides:

toString in class Object