org.sat4j.minisat.orders

Class RandomWalkDecorator

java.lang.Object

org.sat4j.minisat.orders.RandomWalkDecorator

All Implemented Interfaces:

Serializable, IOrder

Direct Known Subclasses:

RandomWalkDecoratorObjective

public class RandomWalkDecorator
extends Object
implements IOrder, Serializable

Since:

2.2

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
RandomWalkDecorator(VarOrderHeap order)
RandomWalkDecorator(VarOrderHeap order, double p)

Method Summary

Methods

Modifier and Type	Method and Description
void	assignLiteral(int q) indicate that a literal has been satisfied.
IPhaseSelectionStrategy	getPhaseSelectionStrategy()
double	getProbability()
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	setProbability(double p)
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

getProbability

public double getProbability()

setProbability

public void setProbability(double p)

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

getVariableHeuristics

public double[] getVariableHeuristics()

Description copied from interface: IOrder

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.

Specified by:

getVariableHeuristics in interface IOrder

Returns:

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