org.sat4j.minisat.core

Interface RestartStrategy

All Superinterfaces:

ConflictTimer, Serializable

All Known Implementing Classes:

ArminRestarts, FixedPeriodRestarts, Glucose21Restarts, LubyRestarts, MiniSATRestarts, NoRestarts

public interface RestartStrategy
extends Serializable, ConflictTimer

Abstraction allowing to choose various restarts strategies.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
void	init(SearchParams params, SolverStats stats) Hook method called just before the search starts.
void	newLearnedClause(Constr learned, int trailLevel) Callback method called when a new clause is learned by the solver, after conflict analysis.
long	nextRestartNumberOfConflict() Deprecated.
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).
boolean	shouldRestart() Ask the strategy if the solver should restart.

Methods inherited from interface org.sat4j.minisat.core.ConflictTimer

newConflict, reset

Method Detail

init

void init(SearchParams params,
        SolverStats stats)

Hook method called just before the search starts.

Parameters:

params - the user's search parameters.

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

nextRestartNumberOfConflict

@Deprecated
long nextRestartNumberOfConflict()

Deprecated.

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

Returns:

the delay in conflicts before the next restart.

shouldRestart

boolean shouldRestart()

Ask the strategy if the solver should restart.

Returns:

true if the solver should restart, else false.

onRestart

void onRestart()

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

onBackjumpToRootLevel

void onBackjumpToRootLevel()

Called when the solver backjumps to the root level.

Since:

2.3.2

newLearnedClause

void newLearnedClause(Constr learned,
                    int trailLevel)

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

Parameters:

learned - the new clause

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

Since:

2.3.3