org.sat4j.tools

Class SearchListenerAdapter<S extends ISolverService>

java.lang.Object

org.sat4j.tools.SearchListenerAdapter<S>

All Implemented Interfaces:

Serializable, SearchListener<S>

Direct Known Subclasses:

ConflictDepthTracing, ConflictLevelTracing, ConflictTracing, DecisionLevelTracing, DecisionTracing, DotSearchTracing, HeuristicsTracing, LBDTracing, LearnedClauseSizeTracing, LearnedClausesSizeTracing, LearnedTracing, ManyCore, RupSearchListener, SearchEnumeratorListener, SearchMinOneListener, SearchOptimizerListener, SpeedTracing

public abstract class SearchListenerAdapter<S extends ISolverService>
extends Object
implements SearchListener<S>

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
SearchListenerAdapter()

Method Summary

Methods

Modifier and Type	Method and Description
void	adding(int p) adding forced variable (conflict driven assignment)
void	assuming(int p) decision variable
void	backjump(int backjumpLevel) The solver is asked to backjump to a given decision level.
void	backtracking(int p) backtrack on a decision variable
void	beginLoop() starts a propagation
void	cleaning() The solver is going to delete some learned clauses.
void	conflictFound(IConstr confl, int dlevel, int trailLevel) a conflict has been found.
void	conflictFound(int p) a conflict has been found while propagating values.
void	delete(int[] clause) delete a clause
void	end(Lbool result) End the search.
void	init(S solverService) Provide access to the solver's controllable interface.
void	learn(IConstr c) learning a new clause
void	learnUnit(int p) learn a new unit clause (a literal)
void	propagating(int p, IConstr reason) Unit propagation
void	restarting() The solver restarts the search.
void	solutionFound(int[] model, RandomAccessModel lazyModel) a solution is found.
void	start() Start the search.

Methods inherited from class java.lang.Object

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

Constructor Detail

SearchListenerAdapter

public SearchListenerAdapter()

Method Detail

init

public void init(S solverService)

Description copied from interface: SearchListener

Provide access to the solver's controllable interface.

Specified by:

init in interface SearchListener<S extends ISolverService>

Parameters:

solverService - a way to safely control the solver.

assuming

public void assuming(int p)

Description copied from interface: SearchListener

decision variable

Specified by:

assuming in interface SearchListener<S extends ISolverService>

propagating

public void propagating(int p,
               IConstr reason)

Description copied from interface: SearchListener

Unit propagation

Specified by:

propagating in interface SearchListener<S extends ISolverService>

reason - TODO

backtracking

public void backtracking(int p)

Description copied from interface: SearchListener

backtrack on a decision variable

Specified by:

backtracking in interface SearchListener<S extends ISolverService>

adding

public void adding(int p)

Description copied from interface: SearchListener

adding forced variable (conflict driven assignment)

Specified by:

adding in interface SearchListener<S extends ISolverService>

learn

public void learn(IConstr c)

Description copied from interface: SearchListener

learning a new clause

Specified by:

learn in interface SearchListener<S extends ISolverService>

learnUnit

public void learnUnit(int p)

Description copied from interface: SearchListener

learn a new unit clause (a literal)

Specified by:

learnUnit in interface SearchListener<S extends ISolverService>

Parameters:

p - a literal in Dimacs format.

delete

public void delete(int[] clause)

Description copied from interface: SearchListener

delete a clause

Specified by:

delete in interface SearchListener<S extends ISolverService>

conflictFound

public void conflictFound(IConstr confl,
                 int dlevel,
                 int trailLevel)

Description copied from interface: SearchListener

a conflict has been found.

Specified by:

conflictFound in interface SearchListener<S extends ISolverService>

Parameters:

confl - TODO

dlevel - TODO

trailLevel - TODO

conflictFound

public void conflictFound(int p)

Description copied from interface: SearchListener

a conflict has been found while propagating values.

Specified by:

conflictFound in interface SearchListener<S extends ISolverService>

Parameters:

p - the conflicting value.

solutionFound

public void solutionFound(int[] model,
                 RandomAccessModel lazyModel)

Description copied from interface: SearchListener

a solution is found.

Specified by:

solutionFound in interface SearchListener<S extends ISolverService>

Parameters:

model - the model found

lazyModel - TODO

beginLoop

public void beginLoop()

Description copied from interface: SearchListener

starts a propagation

Specified by:

beginLoop in interface SearchListener<S extends ISolverService>

start

public void start()

Description copied from interface: SearchListener

Start the search.

Specified by:

start in interface SearchListener<S extends ISolverService>

end

public void end(Lbool result)

Description copied from interface: SearchListener

End the search.

Specified by:

end in interface SearchListener<S extends ISolverService>

Parameters:

result - the result of the search.

restarting

public void restarting()

Description copied from interface: SearchListener

The solver restarts the search.

Specified by:

restarting in interface SearchListener<S extends ISolverService>

backjump

public void backjump(int backjumpLevel)

Description copied from interface: SearchListener

The solver is asked to backjump to a given decision level.

Specified by:

backjump in interface SearchListener<S extends ISolverService>

cleaning

public void cleaning()

Description copied from interface: SearchListener

The solver is going to delete some learned clauses.

Specified by:

cleaning in interface SearchListener<S extends ISolverService>