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;
26  
27  import java.io.BufferedReader;
28  import java.io.FileNotFoundException;
29  import java.io.IOException;
30  import java.io.InputStreamReader;
31  import java.io.ObjectInputStream;
32  import java.io.PrintWriter;
33  import java.io.Serializable;
34  import java.lang.management.ManagementFactory;
35  import java.net.URL;
36  import java.util.Properties;
37  
38  import org.sat4j.reader.ParseFormatException;
39  import org.sat4j.reader.Reader;
40  import org.sat4j.specs.ContradictionException;
41  import org.sat4j.specs.IProblem;
42  import org.sat4j.specs.ISolver;
43  import org.sat4j.specs.TimeoutException;
44  
45  /**
46   * That class is used by launchers used to solve decision problems, i.e.
47   * problems with YES/NO/UNKNOWN answers.
48   * 
49   * @author leberre
50   * 
51   */
52  public abstract class AbstractLauncher implements Serializable {
53  
54      public static final String SOLUTION_PREFIX = "v "; //$NON-NLS-1$
55  
56      public static final String ANSWER_PREFIX = "s "; //$NON-NLS-1$
57  
58      public static final String COMMENT_PREFIX = "c "; //$NON-NLS-1$
59  
60      private long beginTime;
61      
62      private ExitCode exitCode = ExitCode.UNKNOWN;
63  
64      protected Reader reader;
65  
66      private transient PrintWriter out = new PrintWriter(System.out, true);
67  
68      private static final boolean cputimesupported = ManagementFactory.getThreadMXBean().isCurrentThreadCpuTimeSupported();
69      
70      protected transient Thread shutdownHook = new Thread() {
71          @Override
72          public void run() {
73              displayResult();
74          }
75      };
76  
77      protected ISolver solver;
78  
79      private boolean silent = false;
80  
81      private double cputime;
82  
83      protected AbstractLauncher() {
84          Runtime.getRuntime().addShutdownHook(shutdownHook);
85      }
86  
87      protected void displayResult() {
88          if (solver != null) {
89              double wallclocktime = (System.currentTimeMillis() - beginTime) / 1000.0;
90              solver.printStat(out, COMMENT_PREFIX);
91              out.println(ANSWER_PREFIX + exitCode);
92              if (exitCode == ExitCode.SATISFIABLE) {
93                  int[] model = solver.model();
94                  out.print(SOLUTION_PREFIX);
95                  reader.decode(model, out);
96                  out.println();
97              }
98              log("Total wall clock time (in seconds) : " + wallclocktime); //$NON-NLS-1$
99              if (cputimesupported) {
100                 log("Total CPU time (experimental, in seconds) : " + cputime) ; //$NON-NLS-1$
101             }
102         }
103     }
104 
105     protected abstract void usage();
106 
107     /**
108      * @throws IOException
109      */
110     protected final void displayHeader() {
111         log("SAT4J: a SATisfiability library for Java (c) 2004-2007 Daniel Le Berre"); //$NON-NLS-1$
112         log("This is free software under the GNU LGPL licence. See www.sat4j.org for details."); //$NON-NLS-1$
113         log("This software uses some libraries from the Jakarta project. See jakarta.apache.org for details."); //$NON-NLS-1$
114         URL url = Lanceur.class.getResource("/sat4j.version"); //$NON-NLS-1$
115         if (url == null) {
116             log("no version file found!!!"); //$NON-NLS-1$			
117         } else {
118             BufferedReader in = null;
119             try {
120                 in = new BufferedReader(new InputStreamReader(url
121                         .openStream()));
122                 log("version " + in.readLine()); //$NON-NLS-1$
123             } catch (IOException e) {
124                  log("c ERROR: "+e.getMessage());
125             } finally {
126                 if (in!=null) {
127                     try {
128                         in.close();
129                     } catch (IOException e) {
130                         log("c ERROR: "+e.getMessage());
131                     }
132                 }
133             }
134         }
135         Properties prop = System.getProperties();
136         String[] infoskeys = {
137                 "sun.arch.data.model", "java.version", "os.name", "os.version", "os.arch" }; //$NON-NLS-1$//$NON-NLS-2$ //$NON-NLS-3$ //$NON-NLS-4$//$NON-NLS-5$
138         for (String key : infoskeys) {
139             log(key + "\t" + prop.getProperty(key)); //$NON-NLS-1$
140         }
141         Runtime runtime = Runtime.getRuntime();
142         log("Free memory " + runtime.freeMemory()); //$NON-NLS-1$
143         log("Max memory " + runtime.maxMemory()); //$NON-NLS-1$
144         log("Total memory " + runtime.totalMemory()); //$NON-NLS-1$
145         log("Number of processors " + runtime.availableProcessors()); //$NON-NLS-1$
146     }
147 
148     /**
149      * Reads a problem file from the command line.
150      * 
151      * @param problemname
152      *            the fully qualified name of the problem.
153      * @return a reference to the problem to solve
154      * @throws FileNotFoundException
155      *             if the file is not found
156      * @throws ParseFormatException
157      *             if the problem is not expressed using the right format
158      * @throws IOException
159      *             for other IO problems
160      * @throws ContradictionException
161      *             if the problem is found trivially unsat
162      */
163     protected IProblem readProblem(String problemname)
164             throws FileNotFoundException, ParseFormatException, IOException,
165             ContradictionException {
166         log("solving " + problemname); //$NON-NLS-1$
167         log("reading problem ... "); //$NON-NLS-1$
168         reader = createReader(solver, problemname);
169         IProblem problem = reader.parseInstance(problemname);
170         log("... done. Wall clock time " //$NON-NLS-1$
171                 + (System.currentTimeMillis() - beginTime) / 1000.0 + "s."); //$NON-NLS-1$
172         if (cputimesupported) {
173             log("CPU time (experimental) "+ManagementFactory.getThreadMXBean().getCurrentThreadCpuTime() /1000000000.0+"s.");
174         }
175         log("#vars     " + solver.nVars()); //$NON-NLS-1$
176         log("#constraints  " + solver.nConstraints()); //$NON-NLS-1$
177         return problem;
178     }
179 
180     protected abstract Reader createReader(ISolver solver, String problemname);
181 
182     public void run(String[] args) {
183 
184         try {
185             displayHeader();
186             solver = configureSolver(args);
187             if (solver == null)
188                 return;
189             String instanceName = getInstanceName(args);
190             beginTime = System.currentTimeMillis();
191             IProblem problem = readProblem(instanceName);
192             try {
193                 solve(problem);
194             } catch (TimeoutException e) {
195                 log("timeout"); //$NON-NLS-1$
196             }
197         } catch (FileNotFoundException e) {
198             log("FATAL");
199             e.printStackTrace();
200         } catch (IOException e) {
201             log("FATAL");
202             e.printStackTrace();
203         } catch (ContradictionException e) {
204             exitCode = ExitCode.UNSATISFIABLE;
205             log("(trivial inconsistency)"); //$NON-NLS-1$
206         } catch (ParseFormatException e) {
207             log("FATAL");
208             e.printStackTrace();
209         }
210         if (cputimesupported) {
211             cputime = ManagementFactory.getThreadMXBean().getCurrentThreadCpuTime() /1000000000.0;
212         }
213     }
214 
215     protected abstract String getInstanceName(String[] args);
216 
217     protected abstract ISolver configureSolver(String[] args);
218 
219     /**
220      * Display messages as comments on STDOUT
221      * 
222      * @param message
223      */
224     protected void log(String message) {
225         if (!silent)
226             out.println(COMMENT_PREFIX + message);
227     }
228 
229     protected void solve(IProblem problem) throws TimeoutException {
230         exitCode = problem.isSatisfiable() ? ExitCode.SATISFIABLE
231                 : ExitCode.UNSATISFIABLE;
232     }
233 
234     /**
235      * Change the value of the exit code in the Launcher
236      * 
237      * @param exitCode
238      *            the new ExitCode
239      */
240     public final void setExitCode(ExitCode exitCode) {
241         this.exitCode = exitCode;
242     }
243 
244     /**
245      * Get the value of the ExitCode
246      * 
247      * @return the current value of the Exitcode
248      */
249     public final ExitCode getExitCode() {
250         return exitCode;
251     }
252 
253     /**
254      * Obtaining the current time spent since the beginning of the solving
255      * process.
256      * 
257      * @return the time signature at the beginning of the run() method.
258      */
259     public final long getBeginTime() {
260         return beginTime;
261     }
262 
263     /**
264      * 
265      * @return the reader used to parse the instance
266      */
267     public final Reader getReader() {
268         return reader;
269     }
270 
271     /**
272      * To change the output stream on which statistics are displayed. By
273      * default, the solver displays everything on System.out.
274      * 
275      * @param out
276      */
277     public void setLogWriter(PrintWriter out) {
278         this.out = out;
279     }
280 
281     public PrintWriter getLogWriter() {
282         return out;
283     }
284 
285     protected void setSilent(boolean b) {
286         silent = b;
287     }
288     
289     private void readObject(ObjectInputStream stream) throws IOException, ClassNotFoundException {
290         stream.defaultReadObject();
291         out = new PrintWriter(System.out, true);
292         shutdownHook = new Thread() {
293             @Override
294             public void run() {
295                 displayResult();
296             }
297         };
298     }
299 }