Package org.jacop.jasat.modules

Class HeuristicForgetModule

java.lang.Object
org.jacop.jasat.modules.HeuristicForgetModule
All Implemented Interfaces:
SolverComponent, BackjumpListener, ExplanationListener, ForgetListener
public final class HeuristicForgetModule extends Object implements ForgetListener, ExplanationListener, BackjumpListener
A component that selects clauses to forget when solver.forget() is called. It may also call forget() after a restart. Heuristic is from glucose.
Version:
4.10

  • Field Details

    • LEARNT_CLAUSES_NUMBER_THRESHOLD

      public int LEARNT_CLAUSES_NUMBER_THRESHOLD

    • FORGET_THRESHOLD

      public double FORGET_THRESHOLD
      threshold of activity under which a clause is removed

    • core

      private Core core

    • learntClauses

      private LinkedList<Integer>[] learntClauses

  • Constructor Details

    • HeuristicForgetModule

      public HeuristicForgetModule()

  • Method Details

    • onForget

      public void onForget()
      When a forget() event occurs, this component will try to find clauses that can be forgotten, i.e. that are : - not very active (useless) - not the explanation for a currently set literal
      Specified by:
      onForget in interface ForgetListener

    • onRestart

      public void onRestart(int level)
      when a restart occurs, it may be a good occasion to forget clauses
      Specified by:
      onRestart in interface BackjumpListener
      Parameters:
      level - the level at which the solver was before restarting

    • 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

    • onExplain

      public void onExplain(MapClause explanation)
      Description copied from interface: ExplanationListener
      called when the conflict clause is explained
      Specified by:
      onExplain in interface ExplanationListener
      Parameters:
      explanation - the explanation clause

    • shouldTriggerForget

      public final boolean shouldTriggerForget()
      should we forget now ? Will always return false if the current level is not 0
      Returns:
      true if the heuristic advises to forget AND the level is 0

    • numberOfLearntClauses

      private int numberOfLearntClauses()
      Returns:
      the number of learnt clauses one can hope to delete

    • computeLBD

      private int computeLBD(MapClause clause)
      compute the LBD (Literal Block Distance) of a clause
      Parameters:
      clause - the clause
      Returns:
      the LBD of this clause

    • 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