View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  package org.sat4j.minisat.core;
26  
27  import java.io.FileWriter;
28  import java.io.IOException;
29  import java.io.ObjectInputStream;
30  import java.io.PrintWriter;
31  import java.io.Writer;
32  
33  import org.sat4j.core.Vec;
34  
35  /**
36   * Class allowing to express the search as a tree in the dot language. The
37   * resulting file can be viewed in a tool like <a
38   * href="http://www.graphviz.org/">Graphviz</a>
39   * 
40   * To use only on small benchmarks.
41   * 
42   * Note that also does not make sense to use such a listener on a distributed or
43   * remote solver.
44   * 
45   * @author daniel
46   * 
47   */
48  public class DotSearchListener implements SearchListener {
49  
50      /**
51       * 
52       */
53      private static final long serialVersionUID = 1L;
54  
55      private final Vec<String> pile;
56  
57      private String currentNodeName = null;
58  
59      private transient Writer out;
60  
61      private boolean estOrange = false;
62  
63      public DotSearchListener(final String fileNameToSave) {
64          pile = new Vec<String>();
65          try {
66              out = new FileWriter(fileNameToSave);
67          } catch (IOException e) {
68              System.err.println("Problem when created file.");
69          }
70      }
71  
72      public final void assuming(final int p) {
73          final Integer absP = Math.abs(p);
74          String newName;
75  
76          if (currentNodeName == null) {
77              newName = absP.toString();
78              pile.push(newName);
79              saveLine(lineTab("\"" + newName + "\"" + "[label=\"" + newName
80                      + "\", shape=circle, color=blue, style=filled]"));
81          } else {
82              newName = currentNodeName;
83              pile.push(newName);
84              saveLine(lineTab("\"" + newName + "\"" + "[label=\""
85                      + absP.toString()
86                      + "\", shape=circle, color=blue, style=filled]"));
87          }
88          currentNodeName = newName;
89      }
90  
91      public final void propagating(final int p) {
92          String newName = currentNodeName + "." + p;
93  
94          if (currentNodeName == null) {
95              saveLine(lineTab("\"null\" [label=\"\", shape=point]"));
96          }
97          final String couleur = estOrange ? "orange" : "green";
98  
99          saveLine(lineTab("\"" + newName + "\"" + "[label=\""
100                 + Integer.toString(p) + "\",shape=point, color=black]"));
101         saveLine(lineTab("\"" + currentNodeName + "\"" + " -- " + "\""
102                 + newName + "\"" + "[label=" + "\" " + Integer.toString(p)
103                 + "\", fontcolor =" + couleur + ", color = " + couleur
104                 + ", style = bold]"));
105         currentNodeName = newName;
106         estOrange = false;
107     }
108 
109     public final void backtracking(final int p) {
110         final String temp = pile.last();
111         pile.pop();
112         saveLine("\"" + temp + "\"" + "--" + "\"" + currentNodeName + "\""
113                 + "[label=\"\", color=red, style=dotted]");
114         currentNodeName = temp;
115     }
116 
117     public final void adding(final int p) {
118         estOrange = true;
119     }
120 
121     public final void learn(final Constr clause) {
122     }
123 
124     public final void delete(final int[] clause) {
125     }
126 
127     public final void conflictFound() {
128         saveLine(lineTab("\"" + currentNodeName
129                 + "\" [label=\"\", shape=box, color=\"red\", style=filled]"));
130     }
131 
132     public final void solutionFound() {
133         saveLine(lineTab("\"" + currentNodeName
134                 + "\" [label=\"\", shape=box, color=\"green\", style=filled]"));
135     }
136 
137     public final void beginLoop() {
138     }
139 
140     public final void start() {
141         saveLine("graph G {");
142     }
143 
144     public final void end(Lbool result) {
145         saveLine("}");
146     }
147 
148     private final String lineTab(final String line) {
149         return "\t" + line;
150     }
151 
152     private final void saveLine(final String line) {
153         try {
154             out.write(line + '\n');
155             if ("}".equals(line)) {
156                 out.close();
157             }
158         } catch (IOException e) {
159             e.printStackTrace();
160         }
161     }
162     
163     private void readObject(ObjectInputStream stream) throws IOException,
164             ClassNotFoundException {
165         // if the solver is serialized, out is linked to stdout
166         stream.defaultReadObject();
167         out = new PrintWriter(System.out);
168     }
169 }