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

Field Summary

protected double[]	activity mesure heuristique de l'activite d'une variable.
protected int	lastVar Derniere variable choisie
protected L	lits
protected int[]	order Ordre des variables
protected int[]	varpos position des variables

Constructor Summary

VarOrder()

Method Summary

void	assignLiteral(int p) indicate that a literal has been satisfied.
ILits	getVocabulary()
void	init() that method has the responsibility 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.
protected void	updateActivity(int var)
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

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

Field Detail

activity

protected double[] activity

mesure heuristique de l'activite d'une variable.

lastVar

protected int lastVar

Derniere variable choisie

order

protected int[] order

Ordre des variables

varpos

protected int[] varpos

position des variables

lits

protected L extends ILits lits

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.

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

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