org.sat4j.minisat.orders
Class VarOrderHeap<L extends ILits>

java.lang.Object
  org.sat4j.minisat.orders.VarOrderHeap<L>

All Implemented Interfaces:

java.io.Serializable, IOrder<L>

public class VarOrderHeap<L extends ILits>
extends java.lang.Object
implements IOrder<L>, java.io.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 L	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()
ILits	getVocabulary()
void	init() that method has the responsability to initialize all arrays in the heuristics.
int	numberOfInterestingVariables()
void	printStat(java.io.PrintWriter out, java.lang.String prefix) Display statistics regarding the heuristics.
int	select() Selectionne une nouvelle variable, non affectee, ayant l'activite la plus elevee.
void	setLits(L 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.
java.lang.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.
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 L extends 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<L extends ILits>

Parameters:

strategy -

getPhaseSelectionStrategy

public IPhaseSelectionStrategy getPhaseSelectionStrategy()

Specified by:

getPhaseSelectionStrategy in interface IOrder<L extends ILits>

setLits

public void setLits(L lits)

Description copied from interface: IOrder

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

Specified by:

setLits in interface IOrder<L extends ILits>

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<L extends ILits>

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<L extends ILits>

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<L extends ILits>

Parameters:

x -

updateVar

public void updateVar(int p)

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

Specified by:

updateVar in interface IOrder<L extends ILits>

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<L extends ILits>

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<L extends ILits>

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<L extends ILits>

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getVocabulary

public ILits getVocabulary()

printStat

public void printStat(java.io.PrintWriter out,
                      java.lang.String prefix)

Description copied from interface: IOrder

Display statistics regarding the heuristics.

Specified by:

printStat in interface IOrder<L extends ILits>

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<L extends ILits>