org.sat4j.minisat.orders
Class VarOrderHeap

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

All Implemented Interfaces:

Serializable, IOrder

Direct Known Subclasses:

PureOrder, SubsetVarOrder

public class VarOrderHeap
extends Object
implements IOrder, Serializable

Author:

leberre Heuristique du prouveur. Changement par rapport au MiniSAT original : la gestion activity est faite ici et non plus dans Solver.

See Also:

Serialized Form

Field Summary

protected double[]	activity mesure heuristique de l'activite d'une variable.
protected Heap	heap
protected ILits	lits
protected IPhaseSelectionStrategy	phaseStrategy

Constructor Summary

VarOrderHeap()

VarOrderHeap(IPhaseSelectionStrategy strategy)

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.
ILits	getVocabulary()
void	init() that method has the responsability to initialize all arrays in the heuristics.
int	numberOfInterestingVariables()
void	printStat(PrintWriter out, String prefix) Display statistics regarding the heuristics.
int	select() Selectionne une nouvelle variable, non affectee, ayant l'activite la plus elevee.
void	setLits(ILits lits) Method used to provide an easy access the the solver vocabulary.
void	setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy) Change the selection strategy.
void	setVarDecay(double d) Change la valeur de varDecay.
String	toString()
void	undo(int x) Methode appelee quand la variable x est desaffectee.
protected void	updateActivity(int var)
void	updateVar(int p) Appelee lorsque l'activite de la variable x a change.
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.

Methods inherited from class java.lang.Object

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

Field Detail

activity

protected double[] activity

mesure heuristique de l'activite d'une variable.

lits

protected ILits lits

heap

protected Heap heap

phaseStrategy

protected IPhaseSelectionStrategy phaseStrategy

Constructor Detail

VarOrderHeap

public VarOrderHeap()

VarOrderHeap

public VarOrderHeap(IPhaseSelectionStrategy strategy)

Method Detail

setPhaseSelectionStrategy

public void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy)

Change the selection strategy.

Specified by:

setPhaseSelectionStrategy in interface IOrder

Parameters:

strategy -

getPhaseSelectionStrategy

public IPhaseSelectionStrategy getPhaseSelectionStrategy()

Specified by:

getPhaseSelectionStrategy in interface IOrder

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

select

public int select()

Selectionne une nouvelle variable, non affectee, ayant l'activite la plus elevee.

Specified by:

select in interface IOrder

Returns:

Lit.UNDEFINED si aucune variable n'est trouvee

setVarDecay

public void setVarDecay(double d)

Change la valeur de varDecay.

Specified by:

setVarDecay in interface IOrder

Parameters:

d - la nouvelle valeur de varDecay

undo

public void undo(int x)

Methode appelee quand la variable x est desaffectee.

Specified by:

undo in interface IOrder

Parameters:

x -

updateVar

public void updateVar(int p)

Appelee lorsque l'activite de la variable x a change.

Specified by:

updateVar in interface IOrder

Parameters:

p - a literal

updateActivity

protected void updateActivity(int var)

varDecayActivity

public void varDecayActivity()

Description copied from interface: IOrder

Decay the variables activities.

Specified by:

varDecayActivity in interface IOrder

varActivity

public double varActivity(int p)

Description copied from interface: IOrder

To obtain the current activity of a variable.

Specified by:

varActivity in interface IOrder

Parameters:

p - a literal

Returns:

the activity of the variable associated to that literal.

numberOfInterestingVariables

public int numberOfInterestingVariables()

init

public void init()

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

Specified by:

init in interface IOrder

toString

public String toString()

Overrides:

toString in class Object

getVocabulary

public ILits getVocabulary()

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.

assignLiteral

public void assignLiteral(int p)

Description copied from interface: IOrder

indicate that a literal has been satisfied.

Specified by:

assignLiteral 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

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