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 removed
int	LEARNT_CLAUSES_NUMBER_THRESHOLD
private java.util.LinkedList<java.lang.Integer>[]	learntClauses

Constructor Summary

Constructors

Constructor	Description
HeuristicForgetModule()

Method Summary

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

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