View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
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   * Contributors:
28   *   CRIL - initial API and implementation
29   *******************************************************************************/
30  package org.sat4j.sat;
31  
32  import java.io.FileNotFoundException;
33  import java.io.IOException;
34  
35  import org.apache.commons.beanutils.BeanUtils;
36  import org.apache.commons.cli.CommandLine;
37  import org.apache.commons.cli.HelpFormatter;
38  import org.apache.commons.cli.Options;
39  import org.apache.commons.cli.ParseException;
40  import org.apache.commons.cli.PosixParser;
41  import org.sat4j.AbstractLauncher;
42  import org.sat4j.ExitCode;
43  import org.sat4j.ILauncherMode;
44  import org.sat4j.maxsat.WeightedMaxSatDecorator;
45  import org.sat4j.maxsat.reader.MSInstanceReader;
46  import org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator;
47  import org.sat4j.pb.IPBSolver;
48  import org.sat4j.pb.PseudoOptDecorator;
49  import org.sat4j.pb.core.IPBCDCLSolver;
50  import org.sat4j.pb.reader.PBInstanceReader;
51  import org.sat4j.reader.InstanceReader;
52  import org.sat4j.reader.ParseFormatException;
53  import org.sat4j.reader.Reader;
54  import org.sat4j.specs.ContradictionException;
55  import org.sat4j.specs.ILogAble;
56  import org.sat4j.specs.ISolver;
57  import org.sat4j.specs.TimeoutException;
58  import org.sat4j.tools.ConflictDepthTracing;
59  import org.sat4j.tools.ConflictLevelTracing;
60  import org.sat4j.tools.DecisionTracing;
61  import org.sat4j.tools.FileBasedVisualizationTool;
62  import org.sat4j.tools.LearnedClausesSizeTracing;
63  import org.sat4j.tools.MultiTracing;
64  
65  /**
66   * 
67   * This class is used to launch the SAT solvers from the command line. It is
68   * compliant with the SAT competition (www.satcompetition.org) I/O format. The
69   * launcher is to be used as follows:
70   * 
71   * <pre>
72   *                [solvername] filename [key=value]*
73   * </pre>
74   * 
75   * If no solver name is given, then the default solver of the solver factory is
76   * used (@see org.sat4j.core.ASolverFactory#defaultSolver()).
77   * 
78   * This class allows to solve sat, pb and maxsat problems.
79   * 
80   * @author sroussel
81   * @since 2.3.3
82   */
83  public class Launcher extends AbstractLauncher implements ILogAble {
84  
85      /**
86       * 
87       */
88      private static final long serialVersionUID = 1L;
89  
90      private boolean isModeOptimization = false;
91  
92      private boolean modeTracing = false;
93  
94      private boolean launchRemoteControl;
95  
96      private static AbstractLauncher launcher;
97  
98      public static void main(final String[] args) {
99          launcher = new Launcher();
100         launcher.run(args);
101 
102     }
103 
104     private String filename;
105 
106     private ProblemType typeProbleme = ProblemType.CNF_SAT;
107 
108     @Override
109     public void usage() {
110         Solvers.usage(this);
111     }
112 
113     @Override
114     protected Reader createReader(ISolver theSolver, String problemname) {
115         InstanceReader instance = new InstanceReader(theSolver);
116         switch (typeProbleme) {
117         case CNF_MAXSAT:
118         case WCNF_MAXSAT:
119             instance = new MSInstanceReader((WeightedMaxSatDecorator) theSolver);
120             break;
121         case PB_OPT:
122         case PB_SAT:
123             instance = new PBInstanceReader((IPBSolver) theSolver);
124             break;
125         case CNF_SAT:
126             instance = new InstanceReader(theSolver);
127             break;
128         }
129 
130         return instance;
131     }
132 
133     @Override
134     protected String getInstanceName(String[] args) {
135         return this.filename;
136     }
137 
138     /**
139      * Configure the solver according to the command line parameters.
140      * 
141      * @param args
142      *            the command line
143      * @return a solver properly configured.
144      */
145     @SuppressWarnings({ "nls", "unchecked" })
146     @Override
147     protected ISolver configureSolver(String[] args) {
148         Options options = Solvers.createCLIOptions();
149 
150         try {
151             CommandLine cmd = new PosixParser().parse(options, args);
152 
153             this.isModeOptimization = cmd.hasOption("opt");
154 
155             this.filename = cmd.getOptionValue("f");
156 
157             boolean equivalence = cmd.hasOption("e");
158 
159             int others = 0;
160             String[] rargs = cmd.getArgs();
161             if (this.filename == null && rargs.length > 0) {
162                 this.filename = rargs[others++];
163             }
164 
165             if (filename != null) {
166                 String unzipped = Solvers.uncompressed(filename);
167 
168                 if (unzipped.endsWith(".cnf") && isModeOptimization) {
169                     typeProbleme = ProblemType.CNF_MAXSAT;
170                 } else if (unzipped.endsWith(".wcnf")) {
171                     typeProbleme = ProblemType.WCNF_MAXSAT;
172                     isModeOptimization = true;
173                 } else if (unzipped.endsWith(".opb")) {
174                     if (isModeOptimization) {
175                         typeProbleme = ProblemType.PB_OPT;
176                     } else {
177                         typeProbleme = ProblemType.PB_SAT;
178                     }
179                 } else {
180                     typeProbleme = ProblemType.CNF_SAT;
181                 }
182             } else {
183                 typeProbleme = ProblemType.CNF_SAT;
184             }
185 
186             ISolver asolver = Solvers.configureSolver(args, this);
187 
188             this.launchRemoteControl = cmd.hasOption("remote");
189 
190             if (cmd.hasOption("m")) {
191                 setSilent(true);
192             }
193 
194             if (cmd.hasOption("k")) {
195                 Integer myk = Integer.valueOf(cmd.getOptionValue("k"));
196             }
197 
198             if (cmd.hasOption("r")) {
199                 this.modeTracing = true;
200                 if (!cmd.hasOption("remote")) {
201                     asolver.setSearchListener(new MultiTracing(
202                             new ConflictLevelTracing(
203                                     new FileBasedVisualizationTool(
204                                             this.filename + "-conflict-level"),
205                                     new FileBasedVisualizationTool(
206                                             this.filename
207                                                     + "-conflict-level-restart"),
208                                     new FileBasedVisualizationTool(
209                                             this.filename
210                                                     + "-conflict-level-clean")),
211                             new DecisionTracing(
212                                     new FileBasedVisualizationTool(
213                                             this.filename
214                                                     + "-decision-indexes-pos"),
215                                     new FileBasedVisualizationTool(
216                                             this.filename
217                                                     + "-decision-indexes-neg"),
218                                     new FileBasedVisualizationTool(
219                                             this.filename
220                                                     + "-decision-indexes-restart"),
221                                     new FileBasedVisualizationTool(
222                                             this.filename
223                                                     + "-decision-indexes-clean")),
224                             new LearnedClausesSizeTracing(
225                                     new FileBasedVisualizationTool(
226                                             this.filename
227                                                     + "-learned-clauses-size"),
228                                     new FileBasedVisualizationTool(
229                                             this.filename
230                                                     + "-learned-clauses-size-restart"),
231                                     new FileBasedVisualizationTool(
232                                             this.filename
233                                                     + "-learned-clauses-size-clean")),
234                             new ConflictDepthTracing(
235                                     new FileBasedVisualizationTool(
236                                             this.filename + "-conflict-depth"),
237                                     new FileBasedVisualizationTool(
238                                             this.filename
239                                                     + "-conflict-depth-restart"),
240                                     new FileBasedVisualizationTool(
241                                             this.filename
242                                                     + "-conflict-depth-clean"))));
243                 }
244             }
245 
246             switch (typeProbleme) {
247             case PB_OPT:
248                 setLauncherMode(ILauncherMode.OPTIMIZATION);
249                 if (cmd.hasOption("lo")) {
250                     this.problem = new ConstraintRelaxingPseudoOptDecorator(
251                             (IPBSolver) asolver);
252                 } else {
253                     this.problem = new PseudoOptDecorator((IPBSolver) asolver);
254                 }
255                 break;
256             case CNF_MAXSAT:
257             case WCNF_MAXSAT:
258                 setLauncherMode(ILauncherMode.OPTIMIZATION);
259                 asolver = new WeightedMaxSatDecorator((IPBCDCLSolver) asolver,
260                         equivalence);
261                 if (cmd.hasOption("lo")) {
262                     this.problem = new ConstraintRelaxingPseudoOptDecorator(
263                             (WeightedMaxSatDecorator) asolver);
264                 } else {
265                     this.problem = new PseudoOptDecorator(
266                             (WeightedMaxSatDecorator) asolver, false,
267                             !equivalence);
268                 }
269                 break;
270             default:
271                 setLauncherMode(ILauncherMode.DECISION);
272                 break;
273             }
274 
275             setIncomplete(cmd.hasOption("i"));
276 
277             setDisplaySolutionLine(!cmd.hasOption("n"));
278 
279             // use remaining data to configure the solver
280             while (others < rargs.length) {
281                 String[] param = rargs[others].split("="); //$NON-NLS-1$
282                 assert param.length == 2;
283                 log("setting " + param[0] + " to " + param[1]); //$NON-NLS-1$ //$NON-NLS-2$
284                 try {
285                     BeanUtils.setProperty(asolver, param[0], param[1]);
286                 } catch (Exception e) {
287                     log("Cannot set parameter : " //$NON-NLS-1$
288                             + args[others]);
289                 }
290                 others++;
291             }
292 
293             if (asolver != null) {
294                 getLogWriter().println(asolver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
295             }
296             return asolver;
297         } catch (ParseException e1) {
298             HelpFormatter helpf = new HelpFormatter();
299             helpf.printHelp("java -jar sat4j.jar", options, true);
300             usage();
301             System.exit(0);
302         }
303         return null;
304     }
305 
306     @Override
307     public void run(String[] args) {
308         try {
309             displayHeader();
310             this.solver = configureSolver(args);
311             if (this.solver == null) {
312                 usage();
313                 System.exit(0);
314             }
315             if (!this.silent) {
316                 this.solver.setVerbose(true);
317             }
318             String instanceName = getInstanceName(args);
319             if (instanceName == null) {
320                 usage();
321                 System.exit(0);
322             }
323             this.beginTime = System.currentTimeMillis();
324             if (!this.launchRemoteControl) {
325                 readProblem(instanceName);
326                 try {
327                     if (this.problem != null) {
328                         solve(this.problem);
329                     } else {
330                         solve(this.solver);
331                     }
332                 } catch (TimeoutException e) {
333                     log("timeout"); //$NON-NLS-1$
334                 }
335                 System.exit(launcher.getExitCode().value());
336             } else {
337                 RemoteControlFrame frame = new RemoteControlFrame(
338                         this.filename, "", args);
339                 frame.activateTracing(this.modeTracing);
340                 frame.setOptimisationMode(this.isModeOptimization);
341             }
342         } catch (FileNotFoundException e) {
343             System.err.println("FATAL " + e.getLocalizedMessage());
344         } catch (IOException e) {
345             System.err.println("FATAL " + e.getLocalizedMessage());
346         } catch (ContradictionException e) {
347             this.exitCode = ExitCode.UNSATISFIABLE;
348             log("(trivial inconsistency)"); //$NON-NLS-1$
349         } catch (ParseFormatException e) {
350             System.err.println("FATAL " + e.getLocalizedMessage());
351         }
352     }
353 
354 }