org.sat4j.minisat.restarts

Class LubyRestarts

java.lang.Object

org.sat4j.minisat.restarts.LubyRestarts

All Implemented Interfaces:

Serializable, ConflictTimer, RestartStrategy

public final class LubyRestarts
extends Object
implements RestartStrategy

Luby series

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
static int	DEFAULT_LUBY_FACTOR

Constructor Summary

Constructors

Constructor and Description
LubyRestarts()
LubyRestarts(int factor)

Method Summary

Methods

Modifier and Type	Method and Description
int	getFactor()
void	init(SearchParams params, SolverStats stats) Hook method called just before the search starts.
int	luby() returns the current value of the luby sequence.
void	newConflict()
void	newLearnedClause(Constr learned, int trailLevel) Callback method called when a new clause is learned by the solver, after conflict analysis.
int	nextLuby() Computes and return the next value of the luby sequence.
long	nextRestartNumberOfConflict() Ask for the next restart in number of conflicts.
void	onBackjumpToRootLevel() Called when the solver backjumps to the root level.
void	onRestart() Hook method called when a restart occurs (once the solver has backtracked to top decision level).
void	reset()
void	setFactor(int factor)
boolean	shouldRestart() Ask the strategy if the solver should restart.
String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

DEFAULT_LUBY_FACTOR

public static final int DEFAULT_LUBY_FACTOR

See Also:

Constant Field Values

Constructor Detail

LubyRestarts

public LubyRestarts()

LubyRestarts

public LubyRestarts(int factor)

Parameters:

factor - the factor used for the Luby series.

Since:

2.1

Method Detail

luby

public int luby()

returns the current value of the luby sequence.

Returns:

the current value of the luby sequence.

nextLuby

public int nextLuby()

Computes and return the next value of the luby sequence. That method has a side effect of the value returned by luby(). luby()!=nextLuby() but nextLuby()==luby().

Returns:

the new current value of the luby sequence.

See Also:

luby()

setFactor

public void setFactor(int factor)

getFactor

public int getFactor()

init

public void init(SearchParams params,
        SolverStats stats)

Description copied from interface: RestartStrategy

Hook method called just before the search starts.

Specified by:

init in interface RestartStrategy

Parameters:

params - the user's search parameters.

stats - some statistics about the search (number of conflicts, restarts, etc).

nextRestartNumberOfConflict

public long nextRestartNumberOfConflict()

Description copied from interface: RestartStrategy

Ask for the next restart in number of conflicts. Deprecated since 2.3.2

Specified by:

nextRestartNumberOfConflict in interface RestartStrategy

Returns:

the delay in conflicts before the next restart.

onRestart

public void onRestart()

Description copied from interface: RestartStrategy

Hook method called when a restart occurs (once the solver has backtracked to top decision level).

Specified by:

onRestart in interface RestartStrategy

toString

public String toString()

Overrides:

toString in class Object

shouldRestart

public boolean shouldRestart()

Description copied from interface: RestartStrategy

Ask the strategy if the solver should restart.

Specified by:

shouldRestart in interface RestartStrategy

Returns:

true if the solver should restart, else false.

onBackjumpToRootLevel

public void onBackjumpToRootLevel()

Description copied from interface: RestartStrategy

Called when the solver backjumps to the root level.

Specified by:

onBackjumpToRootLevel in interface RestartStrategy

reset

public void reset()

Specified by:

reset in interface ConflictTimer

newConflict

public void newConflict()

Specified by:

newConflict in interface ConflictTimer

newLearnedClause

public void newLearnedClause(Constr learned,
                    int trailLevel)

Description copied from interface: RestartStrategy

Callback method called when a new clause is learned by the solver, after conflict analysis.

Specified by:

newLearnedClause in interface RestartStrategy

Parameters:

learned - the new clause

trailLevel - the number of literals assigned when the conflict occurred.