1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
58
59
60
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.");
111 }
112
113 @Override
114 public void usage() {
115 this.out.println("java -jar sat4j-maxsat.jar instance-name");
116 }
117
118 @Override
119 protected Reader createReader(ISolver aSolver, String problemname) {
120 Reader reader;
121 if (problemname.contains(".wcnf")) {
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");
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 }