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 java.lang.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.8
-
-
Field Summary
Fields Modifier and Type Field Description private Core
core
double
FORGET_THRESHOLD
threshold of activity under which a clause is removedint
LEARNT_CLAUSES_NUMBER_THRESHOLD
private java.util.LinkedList<java.lang.Integer>[]
learntClauses
-
Constructor Summary
Constructors Constructor Description 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 clausevoid
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 explainedvoid
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 clausesboolean
shouldTriggerForget()
should we forget now ? Will always return false if the current level is not 0
-
-
-
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
-
-
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 interfaceForgetListener
-
onRestart
public void onRestart(int level)
when a restart occurs, it may be a good occasion to forget clauses- Specified by:
onRestart
in interfaceBackjumpListener
- 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 interfaceBackjumpListener
- Parameters:
oldLevel
- the level at which the solver was before backtrackingnewLevel
- 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 interfaceExplanationListener
- 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 interfaceSolverComponent
- Parameters:
core
- core component to initialize
-
-