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

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

All Implemented Interfaces:

java.io.Serializable, IOrder<L>

Direct Known Subclasses:

JWOrder, MyOrder, PureOrder

public class VarOrder<L extends ILits>
extends java.lang.Object
implements java.io.Serializable, IOrder<L>

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

Constructor Summary

VarOrder()

Method Summary

void	assignLiteral(int p) indicate that a literal has been satisfied.
ILits	getVocabulary()
void	init() that method has the responsability to initialize all arrays in the heuristics.
void	newVar() Method called each time Solver.newVar() is called.
void	newVar(int howmany) Method called when Solver.newVar(int) is called.
int	numberOfInterestingVariables()
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) Change la valeur de varDecay.
java.lang.String	toString() Affiche les litteraux dans l'ordre de l'heuristique, la valeur de l'activite entre ().
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.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

VarOrder

public VarOrder()

Method Detail

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

newVar

public void newVar()

Description copied from interface: IOrder

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

Specified by:

newVar in interface IOrder<L extends ILits>

newVar

public void newVar(int howmany)

Description copied from interface: IOrder

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

Specified by:

newVar in interface IOrder<L extends ILits>

Parameters:

howmany - the maximum number of variables

See Also:

Solver.newVar(int)

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

Returns:

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

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)

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

Parameters:

x - a variable.

updateVar

public void updateVar(int p)

Description copied from interface: IOrder

To be called when the activity of a literal changed.

Specified by:

updateVar in interface IOrder<L extends ILits>

Parameters:

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

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

Description copied from interface: IOrder

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

Affiche les litteraux dans l'ordre de l'heuristique, la valeur de l'activite entre ().

Overrides:

toString in class java.lang.Object

Returns:

les litteraux dans l'ordre courant.

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>