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.maxsat;
31  
32  import java.io.IOException;
33  
34  import org.apache.commons.cli.CommandLine;
35  import org.apache.commons.cli.HelpFormatter;
36  import org.apache.commons.cli.Options;
37  import org.apache.commons.cli.ParseException;
38  import org.apache.commons.cli.PosixParser;
39  import org.sat4j.AbstractLauncher;
40  import org.sat4j.ILauncherMode;
41  import org.sat4j.maxsat.reader.WDimacsReader;
42  import org.sat4j.opt.MinOneDecorator;
43  import org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator;
44  import org.sat4j.pb.IPBSolver;
45  import org.sat4j.pb.OptToPBSATAdapter;
46  import org.sat4j.pb.PseudoOptDecorator;
47  import org.sat4j.pb.tools.ManyCorePB;
48  import org.sat4j.pb.tools.SearchOptimizerListener;
49  import org.sat4j.reader.LecteurDimacs;
50  import org.sat4j.reader.ParseFormatException;
51  import org.sat4j.reader.Reader;
52  import org.sat4j.specs.ContradictionException;
53  import org.sat4j.specs.IProblem;
54  import org.sat4j.specs.ISolver;
55  
56  /**
57   * Generic launcher to be used for solving optimization problems.
58   * 
59   * @author daniel
60   * @since 2.0
61   * 
62   */
63  public class GenericOptLauncher extends AbstractLauncher {
64  
65      /**
66       * 
67       */
68      private static final long serialVersionUID = 1L;
69  
70      public GenericOptLauncher() {
71          setLauncherMode(ILauncherMode.OPTIMIZATION);
72      }
73  
74      @SuppressWarnings("nls")
75      private Options createCLIOptions() {
76          Options options = new Options();
77          options.addOption("s", "solver", true,
78                  "specifies the name of a PB solver");
79          options.addOption("t", "timeout", true,
80                  "specifies the timeout (in seconds)");
81          options.addOption("p", "parallel", false,
82                  "uses CP and RES pseudo-boolean solvers in parallel");
83          options.addOption("T", "timeoutms", true,
84                  "specifies the timeout (in milliseconds)");
85          options.addOption("K", "kind", true,
86                  "kind of problem: minone, maxsat, etc.");
87          options.addOption("i", "incomplete", false,
88                  "incomplete mode for maxsat");
89          options.addOption("I", "inner mode", false, "optimize using inner mode");
90          options.addOption("c", "clean databases", false,
91                  "clean up the database at root level");
92          options.addOption("k", "keep Hot", false,
93                  "Keep heuristics accross calls to the SAT solver");
94          options.addOption("e", "equivalence", false,
95                  "Use an equivalence instead of an implication for the selector variables");
96          options.addOption("pi", "prime-implicant", false,
97                  "Use prime implicants instead of models for evaluating the objective function");
98          options.addOption("n", "no solution line", false,
99                  "Do not display a solution line (useful if the solution is large)");
100         options.addOption("l", "lower bounding", false,
101                 "search solution by lower bounding instead of by upper bounding");
102         options.addOption("m", "mystery", false, "mystery option");
103         options.addOption("B", "External&Internal", false, "External&Internal optimization");
104         return options;
105     }
106 
107     @Override
108     public void displayLicense() {
109         super.displayLicense();
110         log("This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details."); //$NON-NLS-1$
111     }
112 
113     @Override
114     public void usage() {
115         this.out.println("java -jar sat4j-maxsat.jar instance-name"); //$NON-NLS-1$
116     }
117 
118     @Override
119     protected Reader createReader(ISolver aSolver, String problemname) {
120         Reader reader;
121         if (problemname.contains(".wcnf")) { //$NON-NLS-1$
122             reader = new WDimacsReader(this.wmsd);
123         } else {
124             reader = new LecteurDimacs(aSolver);
125         }
126         reader.setVerbosity(true);
127         return reader;
128     }
129 
130     
131     @Override
132     protected String getInstanceName(String[] args) {
133         return args[args.length - 1];
134     }
135 
136     private WeightedMaxSatDecorator wmsd;
137 
138     @Override
139     protected ISolver configureSolver(String[] args) {
140         ISolver asolver = null;
141         Options options = createCLIOptions();
142         if (args.length == 0) {
143             HelpFormatter helpf = new HelpFormatter();
144             helpf.printHelp("java -jar sat4j-maxsat.jar", options, true);
145             System.exit(0);
146         } else {
147             try {
148                 CommandLine cmd = new PosixParser().parse(options, args);
149                 int problemindex = args.length - 1;
150                 setDisplaySolutionLine(!cmd.hasOption("n"));
151                 boolean equivalence = cmd.hasOption("e");
152                 String kind = cmd.getOptionValue("K"); //$NON-NLS-1$
153                 if (kind == null) {
154                     kind = "maxsat";
155                 }
156                 String aPBSolverName = cmd.getOptionValue("s");
157                 if (aPBSolverName==null) {
158                     aPBSolverName = "Default";
159                 }
160                 if ("minone".equalsIgnoreCase(kind)) {
161                     asolver = new MinOneDecorator(org.sat4j.minisat.SolverFactory.newDefault());
162                 } else if ("mincost".equalsIgnoreCase(kind)
163                         || args[problemindex].endsWith(".p2cnf")) {
164                     asolver = new MinCostDecorator(SolverFactory.newDefault());
165                 } else {
166                     assert "maxsat".equalsIgnoreCase(kind);
167                     if (cmd.hasOption("m")) {
168                         this.wmsd = new WeightedMaxSatDecorator(
169                                 org.sat4j.pb.SolverFactory.newSATUNSAT(),
170                                 equivalence);
171                     } else if (cmd.hasOption("p")) {
172                         this.wmsd = new WeightedMaxSatDecorator(
173                                 org.sat4j.pb.SolverFactory.newBoth(),
174                                 equivalence);
175                     } else {
176                         this.wmsd = new WeightedMaxSatDecorator(
177                                 org.sat4j.pb.SolverFactory.instance().createSolverByName(aPBSolverName), equivalence);
178                     }
179                     if (cmd.hasOption("l")) {
180                         asolver = new ConstraintRelaxingPseudoOptDecorator(
181                                 this.wmsd);
182                     } else if (cmd.hasOption("I")){
183                         this.wmsd.setSearchListener(new SearchOptimizerListener(ILauncherMode.DECISION));
184                         setLauncherMode(ILauncherMode.DECISION);
185                         asolver = this.wmsd;
186                     }else if(cmd.hasOption("B")){
187                         IPBSolver internal = org.sat4j.pb.SolverFactory.newDefault();
188                         internal.setSearchListener(new SearchOptimizerListener(ILauncherMode.DECISION));
189                         IPBSolver external = org.sat4j.pb.SolverFactory.newDefault();
190                         external = new OptToPBSATAdapter(new PseudoOptDecorator(external),ILauncherMode.DECISION);
191                         ManyCorePB mc = new ManyCorePB(external, internal);
192                         this.wmsd = new WeightedMaxSatDecorator(mc, equivalence);
193                         setLauncherMode(ILauncherMode.DECISION);
194                         asolver = this.wmsd;
195                     }else{
196                         asolver = new PseudoOptDecorator(this.wmsd, false,
197                                 cmd.hasOption("pi"));
198                     }
199                 }
200                 if (cmd.hasOption("i")) {
201                     setIncomplete(true);
202                 }
203                 if (cmd.hasOption("c")) {
204                     asolver.setDBSimplificationAllowed(true);
205                 }
206                 if (cmd.hasOption("k")) {
207                     asolver.setKeepSolverHot(true);
208                 }
209                 String timeout = cmd.getOptionValue("t");
210                 if (timeout == null) {
211                     timeout = cmd.getOptionValue("T");
212                     if (timeout != null) {
213                         asolver.setTimeoutMs(Long.parseLong(timeout));
214                     }
215                 } else {
216                     asolver.setTimeout(Integer.parseInt(timeout));
217                 }
218                 getLogWriter().println(asolver.toString(COMMENT_PREFIX));
219             } catch (ParseException e1) {
220                 HelpFormatter helpf = new HelpFormatter();
221                 helpf.printHelp("java -jar sat4jopt.jar", options, true);
222             }
223         }
224         return asolver;
225     }
226 
227     public static void main(String[] args) {
228         AbstractLauncher lanceur = new GenericOptLauncher();
229         lanceur.run(args);
230     }
231 
232     @Override
233     protected IProblem readProblem(String problemname)
234             throws ParseFormatException, IOException,
235             ContradictionException {
236         super.readProblem(problemname);
237         return solver;
238     }
239 }