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