org.sat4j.minisat.orders
Class VarOrderHeap

java.lang.Object
  extended by 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).


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.