New feature in SAT4J: dot file generation

[Daniel Le Berre <leberre@xxxxxxxxxxxxxxxxxxx>]

Dear all,

I just included in CVS a new feature in SAT4J implemented by Laurent  
Stemmer and Nizar Salhaji:
a graphical view of the search space explored by the SAT solver.

The generated dot file can be interpreted by Graphviz for instance:
http://www.graphviz.org/

Here is an example of tree developed for solving a satisfiable aim-50  
instance with the default SAT solver.

The command line was:
java -jar sat4j-nightly.jar -d aim-50.dot -f test/benchs/aim/ 
aim-50-1_6-yes1-1.cnf.gz

Bleu circles denote decision nodes, green edges denote BCP and orange  
edges denote forced variables.

Red rectangles denote conflicts while the green square denote that a  
model has been found.

Let me know if you find that feature useful and if you have any idea  
how to improve it.

As a side effect, I updated the launcher command line. It know uses  
usual unix like syntax.

Cheers,

        Daniel

Attachment: aim-50.dot
Description: Binary data