org.sat4j.specs

Interface SearchListener<S extends ISolverService>

All Superinterfaces:

Serializable

All Known Implementing Classes:

ConflictDepthTracing, ConflictLevelTracing, ConflictTracing, DecisionLevelTracing, DecisionTracing, DetailedCommandPanel, DotSearchTracing, HeuristicsTracing, LBDTracing, LearnedClauseSizeTracing, LearnedClausesSizeTracing, LearnedTracing, ManyCore, ManyCorePB, MultiTracing, RupSearchListener, SearchEnumeratorListener, SearchListenerAdapter, SearchMinOneListener, SearchOptimizerListener, SpeedTracing, TextOutputTracing

public interface SearchListener<S extends ISolverService>
extends Serializable

Interface to the solver main steps. Useful for integrating search visualization or debugging. (that class moved from org.sat4j.minisat.core in earlier version of SAT4J).

Since:

2.1

Author:

daniel

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.

Method Detail

init

void init(S solverService)

Provide access to the solver's controllable interface.

Parameters:

solverService - a way to safely control the solver.

Since:

2.3.2

assuming

void assuming(int p)

decision variable

Parameters:

p -

propagating

void propagating(int p,
               IConstr reason)

Unit propagation

Parameters:

p -

reason - TODO

backtracking

void backtracking(int p)

backtrack on a decision variable

Parameters:

p -

adding

void adding(int p)

adding forced variable (conflict driven assignment)

learn

void learn(IConstr c)

learning a new clause

Parameters:

c -

learnUnit

void learnUnit(int p)

learn a new unit clause (a literal)

Parameters:

p - a literal in Dimacs format.

Since:

2.3.4

delete

void delete(int[] clause)

delete a clause

conflictFound

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

a conflict has been found.

Parameters:

confl - TODO

dlevel - TODO

trailLevel - TODO

conflictFound

void conflictFound(int p)

a conflict has been found while propagating values.

Parameters:

p - the conflicting value.

solutionFound

void solutionFound(int[] model,
                 RandomAccessModel lazyModel)

a solution is found.

Parameters:

model - the model found

lazyModel - TODO

beginLoop

void beginLoop()

starts a propagation

start

void start()

Start the search.

end

void end(Lbool result)

End the search.

Parameters:

result - the result of the search.

restarting

void restarting()

The solver restarts the search.

backjump

void backjump(int backjumpLevel)

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

Parameters:

backjumpLevel -

cleaning

void cleaning()

The solver is going to delete some learned clauses.