Class ActivityModule

java.lang.Object
org.jacop.jasat.modules.ActivityModule
All Implemented Interfaces:
SolverComponent, BackjumpListener, ClauseListener, ConflictListener

public final class ActivityModule extends Object implements ClauseListener, BackjumpListener, ConflictListener
counts the activity of literals
Version:
4.8
  • Field Details

    • BUMP_INCREASE_FACTOR

      private int BUMP_INCREASE_FACTOR
    • LEARNT_COUNT_TO_INCREASE

      private final int LEARNT_COUNT_TO_INCREASE
      See Also:
    • CONFLICT_COUNT_TO_SORT

      private final int CONFLICT_COUNT_TO_SORT
      See Also:
    • posActivities

      private int[] posActivities
    • negActivities

      private int[] negActivities
    • activitiesIndex

      private int activitiesIndex
    • currentBumpRate

      private int currentBumpRate
    • rebaseThreshold

      private int rebaseThreshold
    • learntCount

      private int learntCount
    • priorities

      private Integer[] priorities
    • prioritiesIndex

      private int prioritiesIndex
    • prioritizedVars

      private BitSet prioritizedVars
    • conflictCount

      private int conflictCount
    • core

      public Core core
    • comparator

      private final Comparator<Integer> comparator
      compares literals according to their activity. This stands for i > j and not i < j, because we want activities to be sorted in decreasing order
  • Constructor Details

    • ActivityModule

      public ActivityModule()
  • Method Details

    • onBackjump

      public void onBackjump(int oldLevel, int newLevel)
      Description copied from interface: BackjumpListener
      Called when the solver backtracks. It will also be called when the solver restarts.

      components that want to be warned about backjumps should put themselves in Core.backjumpModules.

      Specified by:
      onBackjump in interface BackjumpListener
      Parameters:
      oldLevel - the level at which the solver was before backtracking
      newLevel - the level to which the solver backtracks
    • onRestart

      public void onRestart(int oldLevel)
      Description copied from interface: BackjumpListener
      called when the solver restarts.

      components that want to be warned about restarts should put themselves in Core.restartModules.

      Specified by:
      onRestart in interface BackjumpListener
      Parameters:
      oldLevel - the level at which the solver was before restarting
    • onConflict

      public void onConflict(MapClause conflictClause, int level)
      Description copied from interface: ConflictListener
      called when a conflict occurs
      Specified by:
      onConflict in interface ConflictListener
      Parameters:
      conflictClause - the conflict (unsatisfiable) clause
      level - the level at which the conflict occurred
    • sortArray

      public void sortArray()
      sort the priorities array (useful after adding a lot of clauses)
    • onClauseAdd

      public final void onClauseAdd(int[] clause, int clauseId, boolean isModelClause)
      Description copied from interface: ClauseListener
      called when the given clause is added.
      Specified by:
      onClauseAdd in interface ClauseListener
      Parameters:
      clause - the clause
      clauseId - the clause's unique Id
      isModelClause - is this clause a model clause ?
    • onClauseRemoval

      public final void onClauseRemoval(int clauseId)
      Description copied from interface: ClauseListener
      called when the clause with unique Id @param clauseId is removed
      Specified by:
      onClauseRemoval in interface ClauseListener
      Parameters:
      clauseId - the id
    • getLiteralToAssert

      public final int getLiteralToAssert()
      returns the non-set literal with highest activity, if any
      Returns:
      a non set literal, or 0 if all known literals are set
    • getLiteralActivity

      private final int getLiteralActivity(int var, boolean polarity)
      gives activity of a (signed) literal
      Parameters:
      literal - the literal
      Returns:
      the activity of this (variable, polarity)
    • bumpVar

      private final int bumpVar(int literal)
      code that really performs variable and polarity activity bumping.
      Parameters:
      var - the variable
      Returns:
      the new activity of the variable
    • ensureVarSize

      private final void ensureVarSize(int var)
    • increaseBumpRate

      private final void increaseBumpRate()
      increases the bump rate, so that recent activity is more important than old activity
    • rebase

      private final void rebase(int value)
      rebases all values
      Parameters:
      value - the value that just overflowed
    • toString

      public String toString()
      Overrides:
      toString in class Object
    • initialize

      public void initialize(Core core)
      Description copied from interface: SolverComponent
      initializes the component with the given solver. May be called only once. This method must register the component to the solver for the run.
      Specified by:
      initialize in interface SolverComponent
      Parameters:
      core - core component to initialize