org.sat4j.specs
Interface SearchListener

All Superinterfaces:

Serializable

All Known Implementing Classes:

ConflictLevelTracing, ConflictTracing, DecisionLevelTracing, DecisionTracing, DotSearchTracing, LearnedClauseSizeTracing, TextOutputTracing

public interface SearchListener
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

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	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	learn(IConstr c) learning a new clause
void	propagating(int p, IConstr reason) Unit propagation
void	restarting() The solver restarts the search.
void	solutionFound() a solution is found.
void	start() Start the search.

Method Detail

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 -

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()

a solution is found.

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 -