org.sat4j.tools
Class DotSearchTracing<T>

java.lang.Object
  extended by org.sat4j.tools.DotSearchTracing<T>
All Implemented Interfaces:
Serializable, SearchListener

public class DotSearchTracing<T>
extends 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.

Since:
2.2
Author:
daniel
See Also:
Serialized Form

Constructor Summary
DotSearchTracing(String fileNameToSave, Map<Integer,T> mapping)
           
 
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 clause)
          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.
 
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

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,
                                int dlevel,
                                int trailLevel)
Description copied from interface: SearchListener
a conflict has been found.

Specified by:
conflictFound in interface SearchListener
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
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

restarting

public void restarting()
Description copied from interface: SearchListener
The solver restarts the search.

Specified by:
restarting in interface SearchListener

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


Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.