Class HeuristicForgetModule

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      private int computeLBD​(MapClause clause)
      compute the LBD (Literal Block Distance) of a clause
      void initialize​(Core core)
      initializes the component with the given solver.
      private int numberOfLearntClauses()  
      void onBackjump​(int oldLevel, int newLevel)
      Called when the solver backtracks.
      void onExplain​(MapClause explanation)
      called when the conflict clause is explained
      void onForget()
      When a forget() event occurs, this component will try to find clauses that can be forgotten, i.e.
      void onRestart​(int level)
      when a restart occurs, it may be a good occasion to forget clauses
      boolean shouldTriggerForget()
      should we forget now ? Will always return false if the current level is not 0
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Field Detail

      • 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 java.util.LinkedList<java.lang.Integer>[] learntClauses
    • Constructor Detail

      • HeuristicForgetModule

        public HeuristicForgetModule()
    • Method Detail

      • 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
      • 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