View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3   *
4   * All rights reserved. This program and the accompanying materials
5   * are made available under the terms of the Eclipse Public License v1.0
6   * which accompanies this distribution, and is available at
7   * http://www.eclipse.org/legal/epl-v10.html
8   *
9   * Alternatively, the contents of this file may be used under the terms of
10  * either the GNU Lesser General Public License Version 2.1 or later (the
11  * "LGPL"), in which case the provisions of the LGPL are applicable instead
12  * of those above. If you wish to allow use of your version of this file only
13  * under the terms of the LGPL, and not to allow others to use your version of
14  * this file under the terms of the EPL, indicate your decision by deleting
15  * the provisions above and replace them with the notice and other provisions
16  * required by the LGPL. If you do not delete the provisions above, a recipient
17  * may use your version of this file under the terms of the EPL or the LGPL.
18  * 
19  * Based on the original MiniSat specification from:
20  * 
21  * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22  * Sixth International Conference on Theory and Applications of Satisfiability
23  * Testing, LNCS 2919, pp 502-518, 2003.
24  *
25  * See www.minisat.se for the original solver in C++.
26  * 
27  *******************************************************************************/
28  package org.sat4j;
29  
30  import java.io.BufferedReader;
31  import java.io.FileNotFoundException;
32  import java.io.IOException;
33  import java.io.InputStreamReader;
34  import java.io.ObjectInputStream;
35  import java.io.PrintWriter;
36  import java.io.Serializable;
37  import java.net.URL;
38  import java.util.Properties;
39  
40  import org.sat4j.core.ASolverFactory;
41  import org.sat4j.reader.ParseFormatException;
42  import org.sat4j.reader.Reader;
43  import org.sat4j.specs.ContradictionException;
44  import org.sat4j.specs.IProblem;
45  import org.sat4j.specs.ISolver;
46  import org.sat4j.specs.TimeoutException;
47  
48  /**
49   * That class is used by launchers used to solve decision problems, i.e.
50   * problems with YES/NO/UNKNOWN answers.
51   * 
52   * @author leberre
53   * 
54   */
55  public abstract class AbstractLauncher implements Serializable {
56  
57      /**
58  	 * 
59  	 */
60  	private static final long serialVersionUID = 1L;
61  
62  	public static final String SOLUTION_PREFIX = "v "; //$NON-NLS-1$
63  
64      public static final String ANSWER_PREFIX = "s "; //$NON-NLS-1$
65  
66      public static final String COMMENT_PREFIX = "c "; //$NON-NLS-1$
67  
68      private long beginTime;
69      
70      private ExitCode exitCode = ExitCode.UNKNOWN;
71  
72      protected Reader reader;
73  
74      private transient PrintWriter out = new PrintWriter(System.out, true);
75      
76      protected transient Thread shutdownHook = new Thread() {
77          @Override
78          public void run() {
79              displayResult();
80          }
81      };
82  
83      protected ISolver solver;
84  
85      private boolean silent = false;
86  
87      protected AbstractLauncher() {
88          Runtime.getRuntime().addShutdownHook(shutdownHook);
89      }
90  
91      protected void displayResult() {
92          if (solver != null) {
93              double wallclocktime = (System.currentTimeMillis() - beginTime) / 1000.0;
94              solver.printStat(out, COMMENT_PREFIX);
95              out.println(ANSWER_PREFIX + exitCode);
96              if (exitCode == ExitCode.SATISFIABLE) {
97                  int[] model = solver.model();
98                  out.print(SOLUTION_PREFIX);
99                  reader.decode(model, out);
100                 out.println();
101             }
102             log("Total wall clock time (in seconds) : " + wallclocktime); //$NON-NLS-1$
103         }
104     }
105 
106     public abstract void usage();
107 
108     /**
109      * @throws IOException
110      */
111     protected final void displayHeader() {
112         displayLicense();
113         URL url = AbstractLauncher.class.getResource("/sat4j.version"); //$NON-NLS-1$
114         if (url == null) {
115             log("no version file found!!!"); //$NON-NLS-1$			
116         } else {
117             BufferedReader in = null;
118             try {
119                 in = new BufferedReader(new InputStreamReader(url
120                         .openStream()));
121                 log("version " + in.readLine()); //$NON-NLS-1$
122             } catch (IOException e) {
123                  log("c ERROR: "+e.getMessage());
124             } finally {
125                 if (in!=null) {
126                     try {
127                         in.close();
128                     } catch (IOException e) {
129                         log("c ERROR: "+e.getMessage());
130                     }
131                 }
132             }
133         }
134         Properties prop = System.getProperties();
135         String[] infoskeys = {
136                 "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$
137         for (String key : infoskeys) {
138             log(key + "\t" + prop.getProperty(key)); //$NON-NLS-1$
139         }
140         Runtime runtime = Runtime.getRuntime();
141         log("Free memory " + runtime.freeMemory()); //$NON-NLS-1$
142         log("Max memory " + runtime.maxMemory()); //$NON-NLS-1$
143         log("Total memory " + runtime.totalMemory()); //$NON-NLS-1$
144         log("Number of processors " + runtime.availableProcessors()); //$NON-NLS-1$
145     }
146 
147     public void displayLicense() {
148         log("SAT4J: a SATisfiability library for Java (c) 2004-2008 Daniel Le Berre"); //$NON-NLS-1$
149         log("This is free software under the dual EPL/GNU LGPL licenses."); //$NON-NLS-1$
150         log("See www.sat4j.org for details."); //$NON-NLS-1$
151     }
152 
153     /**
154      * Reads a problem file from the command line.
155      * 
156      * @param problemname
157      *            the fully qualified name of the problem.
158      * @return a reference to the problem to solve
159      * @throws FileNotFoundException
160      *             if the file is not found
161      * @throws ParseFormatException
162      *             if the problem is not expressed using the right format
163      * @throws IOException
164      *             for other IO problems
165      * @throws ContradictionException
166      *             if the problem is found trivially unsat
167      */
168     protected IProblem readProblem(String problemname)
169             throws FileNotFoundException, ParseFormatException, IOException,
170             ContradictionException {
171         log("solving " + problemname); //$NON-NLS-1$
172         log("reading problem ... "); //$NON-NLS-1$
173         reader = createReader(solver, problemname);
174         IProblem problem = reader.parseInstance(problemname);
175         log("... done. Wall clock time " //$NON-NLS-1$
176                 + (System.currentTimeMillis() - beginTime) / 1000.0 + "s."); //$NON-NLS-1$
177         log("#vars     " + problem.nVars()); //$NON-NLS-1$
178         log("#constraints  " + problem.nConstraints()); //$NON-NLS-1$
179         problem.printInfos(out,COMMENT_PREFIX);    
180         return problem;
181     }
182 
183     protected abstract Reader createReader(ISolver theSolver, String problemname);
184 
185     public void run(String[] args) {
186 
187         try {
188             displayHeader();
189             solver = configureSolver(args);
190             if (solver == null)
191                 return;
192             String instanceName = getInstanceName(args);
193             beginTime = System.currentTimeMillis();
194             IProblem problem = readProblem(instanceName);
195             try {
196                 solve(problem);
197             } catch (TimeoutException e) {
198                 log("timeout"); //$NON-NLS-1$
199             }
200         } catch (FileNotFoundException e) {
201             log("FATAL");
202             e.printStackTrace();
203         } catch (IOException e) {
204             log("FATAL");
205             e.printStackTrace();
206         } catch (ContradictionException e) {
207             exitCode = ExitCode.UNSATISFIABLE;
208             log("(trivial inconsistency)"); //$NON-NLS-1$
209         } catch (ParseFormatException e) {
210             log("FATAL");
211             e.printStackTrace();
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     public 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 
300     protected <T extends ISolver> void showAvailableSolvers(ASolverFactory<T> afactory) {
301         if (afactory != null) {
302             log("Available solvers: "); //$NON-NLS-1$
303             String[] names = afactory.solverNames();
304             for (int i = 0; i < names.length; i++) {
305                 log(names[i]);
306             }
307         }
308     }
309 }