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  package org.sat4j.maxsat;
20  
21  import static java.lang.System.out;
22  
23  import org.apache.commons.cli.CommandLine;
24  import org.apache.commons.cli.HelpFormatter;
25  import org.apache.commons.cli.Options;
26  import org.apache.commons.cli.ParseException;
27  import org.apache.commons.cli.PosixParser;
28  import org.sat4j.AbstractLauncher;
29  import org.sat4j.AbstractOptimizationLauncher;
30  import org.sat4j.maxsat.reader.WDimacsReader;
31  import org.sat4j.opt.MaxSatDecorator;
32  import org.sat4j.opt.MinOneDecorator;
33  import org.sat4j.reader.DimacsReader;
34  import org.sat4j.reader.Reader;
35  import org.sat4j.specs.ISolver;
36  
37  /**
38   * Generic launcher to be used for solving optimization problems.
39   * 
40   * @author daniel
41   * 
42   */
43  public class GenericOptLauncher extends AbstractOptimizationLauncher {
44  
45      /**
46       * 
47       */
48      private static final long serialVersionUID = 1L;
49  
50      @SuppressWarnings("nls")
51      private Options createCLIOptions() {
52          Options options = new Options();
53          options.addOption("t", "timeout", true,
54                  "specifies the timeout (in seconds)");
55          options.addOption("T", "timeoutms", true,
56                  "specifies the timeout (in milliseconds)");
57          options.addOption("k", "kind", true,
58                  "kind of problem: minone, maxsat, etc.");
59          return options;
60      }
61  
62      @Override
63      public void displayLicense() {
64          super.displayLicense();
65          log("This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details."); //$NON-NLS-1$
66      }
67      
68      @Override
69      public void usage() {
70          out.println("java -jar sat4j-maxsat.jar instance-name"); //$NON-NLS-1$
71      }
72  
73      @Override
74      protected Reader createReader(ISolver aSolver, String problemname) {
75          if (problemname.endsWith(".wcnf")) { //$NON-NLS-1$
76              return new WDimacsReader(( WeightedMaxSatDecorator)aSolver); //$NON-NLS-1$
77          } 
78          return new DimacsReader(aSolver);
79      }
80  
81      @Override
82      protected String getInstanceName(String[] args) {
83          return args[args.length - 1];
84      }
85  
86      @Override
87      protected ISolver configureSolver(String[] args) {
88          ISolver asolver = null;
89          Options options = createCLIOptions();
90          if (args.length == 0) {
91              HelpFormatter helpf = new HelpFormatter();
92              helpf.printHelp("java -jar sat4j-maxsat.jar", options, true);
93          } else {
94              try {
95                  CommandLine cmd = new PosixParser().parse(options, args);
96                  int problemindex = args.length - 1;
97                  String kind = cmd.getOptionValue("k"); //$NON-NLS-1$
98                  if (kind == null) { //$NON-NLS-1$
99                      kind = "maxsat";
100                 }
101                 if ("minone".equalsIgnoreCase(kind)) {
102                     asolver = new MinOneDecorator(SolverFactory.newDefault());
103                 } else if ("mincost".equalsIgnoreCase(kind)||args[problemindex].endsWith(".p2cnf")) {
104                     asolver = new MinCostDecorator(SolverFactory.newDefault());
105                 } else {
106                     assert "maxsat".equalsIgnoreCase(kind);
107 
108                     if (args[problemindex].endsWith(".wcnf")) { //$NON-NLS-1$
109                         asolver = new WeightedMaxSatDecorator(SolverFactory
110                                 .newDefault());
111                     } else {
112                         asolver = new MaxSatDecorator(SolverFactory
113                                 .newMiniMaxSAT());
114                     }
115                 }
116                 String timeout = cmd.getOptionValue("t");
117                 if (timeout == null) {
118                     timeout = cmd.getOptionValue("T");
119                     if (timeout != null) {
120                         asolver.setTimeoutMs(Long.parseLong(timeout));
121                     }
122                 } else {
123                     asolver.setTimeout(Integer.parseInt(timeout));
124                 }
125                 log(asolver.toString(COMMENT_PREFIX));
126             } catch (ParseException e1) {
127                 HelpFormatter helpf = new HelpFormatter();
128                 helpf.printHelp("java -jar sat4jopt.jar", options, true);
129             }
130         }
131         return asolver;
132     }
133 
134     public static void main(String[] args) {
135         AbstractLauncher lanceur = new GenericOptLauncher();
136         lanceur.run(args);
137     }
138 }