org.sat4j.tools

Class DotSearchTracing<T>

java.lang.Object

org.sat4j.tools.SearchListenerAdapter<ISolverService>

org.sat4j.tools.DotSearchTracing<T>

All Implemented Interfaces:

Serializable, SearchListener<ISolverService>

public class DotSearchTracing<T>
extends SearchListenerAdapter<ISolverService>

Class allowing to express the search as a tree in the dot language. The resulting file can be viewed in a tool like Graphviz To use only on small benchmarks. Note that also does not make sense to use such a listener on a distributed or remote solver.

Since:

2.2

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
DotSearchTracing(String fileNameToSave, Map<Integer,T> mapping)

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	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 clause) learning a new clause
void	propagating(int p, IConstr reason) Unit propagation
void	solutionFound(int[] model, RandomAccessModel lazyModel) a solution is found.
void	start() Start the search.

Methods inherited from class org.sat4j.tools.SearchListenerAdapter

backjump, cleaning, init, learnUnit, restarting

Methods inherited from class java.lang.Object

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

Constructor Detail

DotSearchTracing

public DotSearchTracing(String fileNameToSave,
                Map<Integer,T> mapping)

Since:

2.1

Method Detail

assuming

public final void assuming(int p)

Description copied from interface: SearchListener

decision variable

Specified by:

assuming in interface SearchListener<ISolverService>

Overrides:

assuming in class SearchListenerAdapter<ISolverService>

propagating

public final void propagating(int p,
               IConstr reason)

Description copied from interface: SearchListener

Unit propagation

Specified by:

propagating in interface SearchListener<ISolverService>

Overrides:

propagating in class SearchListenerAdapter<ISolverService>

reason - TODO

Since:

2.1

backtracking

public final void backtracking(int p)

Description copied from interface: SearchListener

backtrack on a decision variable

Specified by:

backtracking in interface SearchListener<ISolverService>

Overrides:

backtracking in class SearchListenerAdapter<ISolverService>

adding

public final void adding(int p)

Description copied from interface: SearchListener

adding forced variable (conflict driven assignment)

Specified by:

adding in interface SearchListener<ISolverService>

Overrides:

adding in class SearchListenerAdapter<ISolverService>

learn

public final void learn(IConstr clause)

Description copied from interface: SearchListener

learning a new clause

Specified by:

learn in interface SearchListener<ISolverService>

Overrides:

learn in class SearchListenerAdapter<ISolverService>

Since:

2.1

delete

public final void delete(int[] clause)

Description copied from interface: SearchListener

delete a clause

Specified by:

delete in interface SearchListener<ISolverService>

Overrides:

delete in class SearchListenerAdapter<ISolverService>

conflictFound

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

Description copied from interface: SearchListener

a conflict has been found.

Specified by:

conflictFound in interface SearchListener<ISolverService>

Overrides:

conflictFound in class SearchListenerAdapter<ISolverService>

Parameters:

confl - TODO

dlevel - TODO

trailLevel - TODO

Since:

2.1

conflictFound

public final void conflictFound(int p)

Description copied from interface: SearchListener

a conflict has been found while propagating values.

Specified by:

conflictFound in interface SearchListener<ISolverService>

Overrides:

conflictFound in class SearchListenerAdapter<ISolverService>

Parameters:

p - the conflicting value.

Since:

2.1

solutionFound

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

Description copied from interface: SearchListener

a solution is found.

Specified by:

solutionFound in interface SearchListener<ISolverService>

Overrides:

solutionFound in class SearchListenerAdapter<ISolverService>

Parameters:

model - the model found

lazyModel - TODO

beginLoop

public final void beginLoop()

Description copied from interface: SearchListener

starts a propagation

Specified by:

beginLoop in interface SearchListener<ISolverService>

Overrides:

beginLoop in class SearchListenerAdapter<ISolverService>

start

public final void start()

Description copied from interface: SearchListener

Start the search.

Specified by:

start in interface SearchListener<ISolverService>

Overrides:

start in class SearchListenerAdapter<ISolverService>

end

public final void end(Lbool result)

Description copied from interface: SearchListener

End the search.

Specified by:

end in interface SearchListener<ISolverService>

Overrides:

end in class SearchListenerAdapter<ISolverService>

Parameters:

result - the result of the search.

Since:

2.1