Package org.jacop.jasat.modules

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

  • 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:
      var - 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:
      literal - 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