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 Summary
FieldsModifier and TypeFieldDescriptionprivate Core
double
threshold of activity under which a clause is removedint
private LinkedList<Integer>[]
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionprivate 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
void
onBackjump
(int oldLevel, int newLevel) Called when the solver backtracks.void
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 clausesfinal boolean
should we forget now ? Will always return false if the current level is not 0
-
Field Details
-
LEARNT_CLAUSES_NUMBER_THRESHOLD
public int LEARNT_CLAUSES_NUMBER_THRESHOLD -
FORGET_THRESHOLD
public double FORGET_THRESHOLDthreshold of activity under which a clause is removed -
core
-
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 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
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
compute the LBD (Literal Block Distance) of a clause- Parameters:
clause
- the clause- Returns:
- the LBD of this clause
-
initialize
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
-