View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  package org.sat4j;
26  
27  import static java.lang.System.out;
28  
29  import org.apache.commons.cli.CommandLine;
30  import org.apache.commons.cli.HelpFormatter;
31  import org.apache.commons.cli.Options;
32  import org.apache.commons.cli.ParseException;
33  import org.apache.commons.cli.PosixParser;
34  import org.sat4j.minisat.SolverFactory;
35  import org.sat4j.opt.MaxSatDecorator;
36  import org.sat4j.opt.MinCostDecorator;
37  import org.sat4j.opt.MinOneDecorator;
38  import org.sat4j.opt.WeightedMaxSatDecorator;
39  import org.sat4j.reader.DimacsReader;
40  import org.sat4j.reader.Reader;
41  import org.sat4j.specs.ISolver;
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  
54          options.addOption("l", "library", true,
55                  "specifies the name of the library used (minisat by default)");
56          options.addOption("s", "solver", true,
57                  "specifies the name of the solver to use");
58          options.addOption("t", "timeout", true,
59                  "specifies the timeout (in seconds)");
60          options.addOption("k", "kind", true,
61                  "kind of problem: minone, maxsat, etc.");
62          return options;
63      }
64  
65      @Override
66      protected void usage() {
67          out.println("java -jar sat4jopt instance-name"); //$NON-NLS-1$
68      }
69  
70      @Override
71      protected Reader createReader(ISolver solver, String problemname) {
72          if (problemname.endsWith(".wcnf")) { //$NON-NLS-1$
73              return new DimacsReader(solver, "wcnf"); //$NON-NLS-1$
74          }
75          return new DimacsReader(solver);
76      }
77  
78      @Override
79      protected String getInstanceName(String[] args) {
80          return args[args.length - 1];
81      }
82  
83      @Override
84      protected ISolver configureSolver(String[] args) {
85          ISolver asolver = null;
86          Options options = createCLIOptions();
87          if (args.length == 0) {
88              HelpFormatter helpf = new HelpFormatter();
89              helpf.printHelp("java -jar sat4jopt.jar", options, true);
90          } else {
91              try {
92                  CommandLine cmd = new PosixParser().parse(options, args);
93  
94                  String kind = cmd.getOptionValue("k"); //$NON-NLS-1$
95                  if (kind == null) { //$NON-NLS-1$
96                      kind = "maxsat";
97                  }
98                  if ("minone".equalsIgnoreCase(kind)) {
99                      asolver = new MinOneDecorator(SolverFactory.newDefault());
100                 } else if ("mincost".equalsIgnoreCase(kind)) {
101                     asolver = new MinCostDecorator(SolverFactory
102                             .newMiniOPBClauseCardConstrMax());
103                 } else {
104                     assert "maxsat".equalsIgnoreCase(kind);
105                     int problemindex = args.length - 1;
106                     if (args[problemindex].endsWith(".wcnf")) { //$NON-NLS-1$
107                         asolver = new WeightedMaxSatDecorator(SolverFactory
108                                 .newMinimalOPBClauseCardConstrMaxSpecificOrder());
109                     } else {
110                         asolver = new MaxSatDecorator(SolverFactory
111                                 .newMiniMaxSAT());
112                     }
113                 }
114                 log(asolver.toString(COMMENT_PREFIX));
115             } catch (ParseException e1) {
116                 HelpFormatter helpf = new HelpFormatter();
117                 helpf.printHelp("java -jar sat4jopt.jar", options, true);
118             }
119         }
120         return asolver;
121     }
122 
123     public static void main(String[] args) {
124         AbstractLauncher lanceur = new GenericOptLauncher();
125         lanceur.run(args);
126     }
127 }