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