VarOrderHeap (Sat4j)

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

All Implemented Interfaces:

java.io.Serializable, IOrder

Direct Known Subclasses:

PureOrder, SubsetVarOrder, VarOrderHeapObjective
```
public class VarOrderHeap
extends java.lang.Object
implements IOrder, 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

Fields
Modifier and Type	Field and Description
`protected double[]`	`activity` mesure heuristique de l'activite d'une variable.
`protected Heap`	`heap`
`protected ILits`	`lits`
`protected IPhaseSelectionStrategy`	`phaseStrategy`

Constructor Summary

Constructors
Constructor and Description

VarOrderHeap()

VarOrderHeap(IPhaseSelectionStrategy strategy)

Constructors
Constructor and Description
`VarOrderHeap()`
`VarOrderHeap(IPhaseSelectionStrategy strategy)`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`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(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(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.
`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.
`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 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
    
    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).

Class VarOrderHeap

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

activity

lits

heap

phaseStrategy

Constructor Detail

VarOrderHeap

VarOrderHeap

Method Detail

setPhaseSelectionStrategy

getPhaseSelectionStrategy

setLits

select

setVarDecay

undo

updateVar

updateActivity

varDecayActivity

varActivity

numberOfInterestingVariables

init

toString

getVocabulary

printStat

assignLiteral

updateVarAtDecisionLevel

getVariableHeuristics