Package org.jacop.jasat.modules

Class ActivityModule

java.lang.Object

org.jacop.jasat.modules.ActivityModule

All Implemented Interfaces:

SolverComponent, BackjumpListener, ClauseListener, ConflictListener

public final class ActivityModule
extends java.lang.Object
implements ClauseListener, BackjumpListener, ConflictListener

counts the activity of literals

Version:

4.8

Field Summary

Fields

Modifier and Type	Field	Description
private int	activitiesIndex
private int	BUMP_INCREASE_FACTOR
private java.util.Comparator<java.lang.Integer>	comparator	compares literals according to their activity.
private int	CONFLICT_COUNT_TO_SORT
private int	conflictCount
Core	core
private int	currentBumpRate
private int	LEARNT_COUNT_TO_INCREASE
private int	learntCount
private int[]	negActivities
private int[]	posActivities
private java.lang.Integer[]	priorities
private int	prioritiesIndex
private java.util.BitSet	prioritizedVars
private int	rebaseThreshold

Constructor Summary

Constructors

Constructor	Description
ActivityModule()

Method Summary

Modifier and Type	Method	Description
private int	bumpVar(int literal)	code that really performs variable and polarity activity bumping.
private void	ensureVarSize(int var)
private int	getLiteralActivity(int var, boolean polarity)	gives activity of a (signed) literal
int	getLiteralToAssert()	returns the non-set literal with highest activity, if any
private void	increaseBumpRate()	increases the bump rate, so that recent activity is more important than old activity
void	initialize(Core core)	initializes the component with the given solver.
void	onBackjump(int oldLevel, int newLevel)	Called when the solver backtracks.
void	onClauseAdd(int[] clause, int clauseId, boolean isModelClause)	called when the given clause is added.
void	onClauseRemoval(int clauseId)	called when the clause with unique Id @param clauseId is removed
void	onConflict(MapClause conflictClause, int level)	called when a conflict occurs
void	onRestart(int oldLevel)	called when the solver restarts.
private void	rebase(int value)	rebases all values
void	sortArray()	sort the priorities array (useful after adding a lot of clauses)
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

BUMP_INCREASE_FACTOR

private int BUMP_INCREASE_FACTOR

LEARNT_COUNT_TO_INCREASE

private final int LEARNT_COUNT_TO_INCREASE

See Also:

Constant Field Values

CONFLICT_COUNT_TO_SORT

private final int CONFLICT_COUNT_TO_SORT

See Also:

Constant Field Values

posActivities

private int[] posActivities

negActivities

private int[] negActivities

activitiesIndex

private int activitiesIndex

currentBumpRate

private int currentBumpRate

rebaseThreshold

private int rebaseThreshold

learntCount

private int learntCount

priorities

private java.lang.Integer[] priorities

prioritiesIndex

private int prioritiesIndex

prioritizedVars

private java.util.BitSet prioritizedVars

conflictCount

private int conflictCount

core

public Core core

comparator

private final java.util.Comparator<java.lang.Integer> comparator

compares literals according to their activity. This stands for i > j and not i < j, because we want activities to be sorted in decreasing order

Constructor Detail

ActivityModule

public ActivityModule()

Method Detail

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

onRestart

public void onRestart(int oldLevel)

Description copied from interface: BackjumpListener

called when the solver restarts.

components that want to be warned about restarts should put themselves in Core.restartModules.

Specified by:

onRestart in interface BackjumpListener

Parameters:

oldLevel - the level at which the solver was before restarting

onConflict

public void onConflict(MapClause conflictClause,
                       int level)

Description copied from interface: ConflictListener

called when a conflict occurs

Specified by:

onConflict in interface ConflictListener

Parameters:

conflictClause - the conflict (unsatisfiable) clause

level - the level at which the conflict occurred

sortArray

public void sortArray()

sort the priorities array (useful after adding a lot of clauses)

onClauseAdd

public final void onClauseAdd(int[] clause,
                              int clauseId,
                              boolean isModelClause)

Description copied from interface: ClauseListener

called when the given clause is added.

Specified by:

onClauseAdd in interface ClauseListener

Parameters:

clause - the clause

clauseId - the clause's unique Id

isModelClause - is this clause a model clause ?

onClauseRemoval

public final void onClauseRemoval(int clauseId)

Description copied from interface: ClauseListener

called when the clause with unique Id @param clauseId is removed

Specified by:

onClauseRemoval in interface ClauseListener

Parameters:

clauseId - the id

getLiteralToAssert

public final int getLiteralToAssert()

returns the non-set literal with highest activity, if any

Returns:

a non set literal, or 0 if all known literals are set

getLiteralActivity

private final int getLiteralActivity(int var,
                                     boolean polarity)

gives activity of a (signed) literal

Parameters:

literal - the literal

Returns:

the activity of this (variable, polarity)

bumpVar

private final int bumpVar(int literal)

code that really performs variable and polarity activity bumping.

Parameters:

var - the variable

Returns:

the new activity of the variable

ensureVarSize

private final void ensureVarSize(int var)

increaseBumpRate

private final void increaseBumpRate()

increases the bump rate, so that recent activity is more important than old activity

rebase

private final void rebase(int value)

rebases all values

Parameters:

value - the value that just overflowed

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

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