org.sat4j.minisat.core
Class DotSearchListener<T>

java.lang.Object
  org.sat4j.minisat.core.DotSearchListener<T>

All Implemented Interfaces:

java.io.Serializable, SearchListener

public class DotSearchListener<T>
extends java.lang.Object
implements SearchListener

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.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

DotSearchListener(java.lang.String fileNameToSave, java.util.Map<java.lang.Integer,T> mapping)

Method Summary

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

DotSearchListener

public DotSearchListener(java.lang.String fileNameToSave,
                         java.util.Map<java.lang.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

propagating

public final void propagating(int p,
                              IConstr reason)

Description copied from interface: SearchListener

Unit propagation

Specified by:

propagating in interface SearchListener

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

adding

public final void adding(int p)

Description copied from interface: SearchListener

adding forced variable (conflict driven assignment)

Specified by:

adding in interface SearchListener

learn

public final void learn(IConstr clause)

Description copied from interface: SearchListener

learning a new clause

Specified by:

learn in interface SearchListener

Since:

2.1

delete

public final void delete(int[] clause)

Description copied from interface: SearchListener

delete a clause

Specified by:

delete in interface SearchListener

conflictFound

public final void conflictFound(IConstr confl)

Description copied from interface: SearchListener

a conflict has been found.

Specified by:

conflictFound in interface SearchListener

Parameters:

confl - 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

Parameters:

p - the conflicting value.

Since:

2.1

solutionFound

public final void solutionFound()

Description copied from interface: SearchListener

a solution is found.

Specified by:

solutionFound in interface SearchListener

beginLoop

public final void beginLoop()

Description copied from interface: SearchListener

starts a propagation

Specified by:

beginLoop in interface SearchListener

start

public final void start()

Description copied from interface: SearchListener

Start the search.

Specified by:

start in interface SearchListener

end

public final void end(Lbool result)

Description copied from interface: SearchListener

End the search.

Specified by:

end in interface SearchListener

Parameters:

result - the result of the search.

Since:

2.1