org.sat4j.sat
Class RemoteControlStrategy

java.lang.Object
  org.sat4j.sat.RemoteControlStrategy

All Implemented Interfaces:

Serializable, ConflictTimer, IPhaseSelectionStrategy, RestartStrategy

public class RemoteControlStrategy
extends Object
implements RestartStrategy, IPhaseSelectionStrategy

Strategy used by the solver when launched with the remote control.

Author:

sroussel

See Also:

Serialized Form

Constructor Summary

RemoteControlStrategy()

RemoteControlStrategy(ICDCLLogger log)

Method Summary

void	assignLiteral(int p) indicate that a literal has been satisfied.
void	clickedOnClean()
ICDCLLogger	getLogger()
int	getNbClausesAtWhichWeShouldClean()
IPhaseSelectionStrategy	getPhaseSelectionStrategy()
RestartStrategy	getRestartStrategy()
SearchParams	getSearchParams()
ICDCL	getSolver()
void	init(int nlength) that method has the responsibility to initialize all arrays in the heuristics.
void	init(int var, int p) initialize the phase of a given variable to the given value.
void	init(SearchParams params) Hook method called just before the search starts.
boolean	isHasClickedOnClean()
boolean	isHasClickedOnRestart()
boolean	isUseTelecomStrategyAsLearnedConstraintsDeletionStrategy()
void	newConflict()
void	newLearnedClause(Constr learned, int trailLevel)
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()
int	select(int var) selects the phase of the variable according to a phase selection strategy.
void	setHasClickedOnClean(boolean hasClickedOnClean)
void	setHasClickedOnRestart(boolean hasClickedOnRestart)
void	setInterrupted(boolean b)
void	setLogger(ICDCLLogger logger)
void	setNbClausesAtWhichWeShouldClean(int nbClausesAtWhichWeShouldClean)
void	setPhaseSelectionStrategy(IPhaseSelectionStrategy phaseSelectionStrategy)
void	setRestartStrategy(RestartStrategy restart)
void	setSolver(ICDCL solver)
void	setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy(boolean useTelecomStrategyAsLearnedConstraintsDeletionStrategy)
boolean	shouldRestart() Ask the strategy if the solver should restart.
String	toString()
void	updateVar(int p) To be called when the activity of a literal changed.
void	updateVarAtDecisionLevel(int q) Allow to perform a specific action when a literal of the current decision level is updated.

Methods inherited from class java.lang.Object

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

Constructor Detail

RemoteControlStrategy

public RemoteControlStrategy(ICDCLLogger log)

RemoteControlStrategy

public RemoteControlStrategy()

Method Detail

isHasClickedOnRestart

public boolean isHasClickedOnRestart()

setHasClickedOnRestart

public void setHasClickedOnRestart(boolean hasClickedOnRestart)

isHasClickedOnClean

public boolean isHasClickedOnClean()

setHasClickedOnClean

public void setHasClickedOnClean(boolean hasClickedOnClean)

isUseTelecomStrategyAsLearnedConstraintsDeletionStrategy

public boolean isUseTelecomStrategyAsLearnedConstraintsDeletionStrategy()

setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy

public void setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy(boolean useTelecomStrategyAsLearnedConstraintsDeletionStrategy)

clickedOnClean

public void clickedOnClean()

getRestartStrategy

public RestartStrategy getRestartStrategy()

getPhaseSelectionStrategy

public IPhaseSelectionStrategy getPhaseSelectionStrategy()

setPhaseSelectionStrategy

public void setPhaseSelectionStrategy(IPhaseSelectionStrategy phaseSelectionStrategy)

setRestartStrategy

public void setRestartStrategy(RestartStrategy restart)

getNbClausesAtWhichWeShouldClean

public int getNbClausesAtWhichWeShouldClean()

setNbClausesAtWhichWeShouldClean

public void setNbClausesAtWhichWeShouldClean(int nbClausesAtWhichWeShouldClean)

getLogger

public ICDCLLogger getLogger()

setLogger

public void setLogger(ICDCLLogger logger)

init

public void init(SearchParams params)

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.

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.

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.

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

onBackjumpToRootLevel

public void onBackjumpToRootLevel()

Description copied from interface: RestartStrategy

Called when the solver backjumps to the root level.

Specified by:

onBackjumpToRootLevel in interface RestartStrategy

getSearchParams

public SearchParams getSearchParams()

Specified by:

getSearchParams in interface RestartStrategy

getSolver

public ICDCL getSolver()

setSolver

public void setSolver(ICDCL solver)

reset

public void reset()

Specified by:

reset in interface ConflictTimer

newConflict

public void newConflict()

Specified by:

newConflict in interface ConflictTimer

updateVar

public void updateVar(int p)

Description copied from interface: IPhaseSelectionStrategy

To be called when the activity of a literal changed.

Specified by:

updateVar in interface IPhaseSelectionStrategy

Parameters:

p - a literal. The associated variable will be updated.

init

public void init(int nlength)

Description copied from interface: IPhaseSelectionStrategy

that method has the responsibility to initialize all arrays in the heuristics.

Specified by:

init in interface IPhaseSelectionStrategy

Parameters:

nlength - the number of variables managed by the heuristics.

init

public void init(int var,
                 int p)

Description copied from interface: IPhaseSelectionStrategy

initialize the phase of a given variable to the given value. That method is suppose to be called AFTER init(int).

Specified by:

init in interface IPhaseSelectionStrategy

Parameters:

var - a variable

p - it's initial phase

assignLiteral

public void assignLiteral(int p)

Description copied from interface: IPhaseSelectionStrategy

indicate that a literal has been satisfied.

Specified by:

assignLiteral in interface IPhaseSelectionStrategy

select

public int select(int var)

Description copied from interface: IPhaseSelectionStrategy

selects the phase of the variable according to a phase selection strategy.

Specified by:

select in interface IPhaseSelectionStrategy

Parameters:

var - a variable chosen by the heuristics

Returns:

either var or not var, depending of the selection strategy.

updateVarAtDecisionLevel

public void updateVarAtDecisionLevel(int q)

Description copied from interface: IPhaseSelectionStrategy

Allow to perform a specific action when a literal of the current decision level is updated. That method is called after IPhaseSelectionStrategy.updateVar(int).

Specified by:

updateVarAtDecisionLevel in interface IPhaseSelectionStrategy

Parameters:

q - a literal

toString

public String toString()

Overrides:

toString in class Object

setInterrupted

public void setInterrupted(boolean b)

newLearnedClause

public void newLearnedClause(Constr learned,
                             int trailLevel)

Specified by:

newLearnedClause in interface RestartStrategy