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.sat;
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52 import java.io.FileNotFoundException;
53 import java.io.IOException;
54 import java.io.PrintWriter;
55 import java.lang.reflect.Method;
56
57 import org.apache.commons.beanutils.BeanUtils;
58 import org.apache.commons.cli.CommandLine;
59 import org.apache.commons.cli.HelpFormatter;
60 import org.apache.commons.cli.Option;
61 import org.apache.commons.cli.Options;
62 import org.apache.commons.cli.ParseException;
63 import org.apache.commons.cli.PosixParser;
64 import org.sat4j.AbstractLauncher;
65 import org.sat4j.ExitCode;
66 import org.sat4j.ILauncherMode;
67 import org.sat4j.core.VecInt;
68 import org.sat4j.minisat.core.ICDCL;
69 import org.sat4j.pb.IPBSolver;
70 import org.sat4j.pb.PseudoOptDecorator;
71 import org.sat4j.pb.core.IPBCDCLSolver;
72 import org.sat4j.pb.reader.PBInstanceReader;
73 import org.sat4j.reader.InstanceReader;
74 import org.sat4j.reader.ParseFormatException;
75 import org.sat4j.reader.Reader;
76 import org.sat4j.specs.ContradictionException;
77 import org.sat4j.specs.ILogAble;
78 import org.sat4j.specs.IOptimizationProblem;
79 import org.sat4j.specs.IProblem;
80 import org.sat4j.specs.ISolver;
81 import org.sat4j.specs.IVecInt;
82 import org.sat4j.specs.TimeoutException;
83 import org.sat4j.tools.ConflictDepthTracing;
84 import org.sat4j.tools.ConflictLevelTracing;
85 import org.sat4j.tools.DecisionTracing;
86 import org.sat4j.tools.DotSearchTracing;
87 import org.sat4j.tools.FileBasedVisualizationTool;
88 import org.sat4j.tools.LearnedClausesSizeTracing;
89 import org.sat4j.tools.MultiTracing;
90
91 @Deprecated
92 public class Lanceur extends AbstractLauncher implements ILogAble {
93
94 private static final String NUMBER = "number";
95
96
97
98
99 private static final long serialVersionUID = 1L;
100
101 private static final String CURRENT_OPTIMUM_VALUE_PREFIX = "o ";
102
103 private boolean incomplete = false;
104
105 private boolean isModeOptimization = false;
106
107 private IProblem problem;
108
109 private boolean modeTracing = false;
110
111 private boolean launchRemoteControl;
112
113 private static AbstractLauncher lanceur;
114
115 public static void main(final String[] args) {
116 lanceur = new Lanceur();
117 lanceur.run(args);
118
119 }
120
121 private String filename;
122
123 private int k = -1;
124
125
126
127
128
129
130
131
132 @SuppressWarnings({ "nls", "unchecked" })
133 @Override
134 protected ICDCL configureSolver(String[] args) {
135 Options options = createCLIOptions();
136
137 try {
138 CommandLine cmd = new PosixParser().parse(options, args);
139
140 if (cmd.hasOption("opt")) {
141 this.isModeOptimization = true;
142 }
143
144 String framework = cmd.getOptionValue("l");
145 if (this.isModeOptimization) {
146 framework = "pb";
147 } else if (framework == null) {
148 framework = "minisat";
149 }
150
151 try {
152 Class<?> clazz = Class
153 .forName("org.sat4j." + framework + ".SolverFactory");
154 Class<?>[] params = {};
155 Method m = clazz.getMethod("instance", params);
156 } catch (Exception e) {
157 log("Wrong framework: " + framework
158 + ". Using minisat instead.");
159 }
160
161 ICDCL asolver = Solvers.configureSolver(args, this);
162
163 this.launchRemoteControl = cmd.hasOption("remote");
164
165 this.filename = cmd.getOptionValue("f");
166
167 if (cmd.hasOption("d")) {
168 String dotfilename = null;
169 if (this.filename != null) {
170 dotfilename = cmd.getOptionValue("d");
171 }
172 if (dotfilename == null) {
173 dotfilename = "sat4j.dot";
174 }
175 asolver.setSearchListener(new DotSearchTracing(dotfilename,
176 null));
177 }
178
179 if (cmd.hasOption("m")) {
180 setSilent(true);
181 }
182
183 if (cmd.hasOption("k")) {
184 Integer myk = Integer.valueOf(cmd.getOptionValue("k"));
185 if (myk != null) {
186 this.k = myk.intValue();
187 }
188 }
189
190 if (this.isModeOptimization) {
191 assert asolver instanceof IPBSolver;
192 this.problem = new PseudoOptDecorator((IPBCDCLSolver) asolver);
193 }
194
195 int others = 0;
196 String[] rargs = cmd.getArgs();
197 if (this.filename == null && rargs.length > 0) {
198 this.filename = rargs[others++];
199 }
200
201 if (cmd.hasOption("r")) {
202 this.modeTracing = true;
203 if (!cmd.hasOption("remote")) {
204 asolver.setSearchListener(new MultiTracing(
205 new ConflictLevelTracing(
206 new FileBasedVisualizationTool(
207 this.filename + "-conflict-level"),
208 new FileBasedVisualizationTool(
209 this.filename
210 + "-conflict-level-restart"),
211 new FileBasedVisualizationTool(
212 this.filename
213 + "-conflict-level-clean")),
214 new DecisionTracing(
215 new FileBasedVisualizationTool(
216 this.filename
217 + "-decision-indexes-pos"),
218 new FileBasedVisualizationTool(
219 this.filename
220 + "-decision-indexes-neg"),
221 new FileBasedVisualizationTool(
222 this.filename
223 + "-decision-indexes-restart"),
224 new FileBasedVisualizationTool(
225 this.filename
226 + "-decision-indexes-clean")),
227 new LearnedClausesSizeTracing(
228 new FileBasedVisualizationTool(
229 this.filename
230 + "-learned-clauses-size"),
231 new FileBasedVisualizationTool(
232 this.filename
233 + "-learned-clauses-size-restart"),
234 new FileBasedVisualizationTool(
235 this.filename
236 + "-learned-clauses-size-clean")),
237 new ConflictDepthTracing(
238 new FileBasedVisualizationTool(
239 this.filename + "-conflict-depth"),
240 new FileBasedVisualizationTool(
241 this.filename
242 + "-conflict-depth-restart"),
243 new FileBasedVisualizationTool(
244 this.filename
245 + "-conflict-depth-clean"))));
246 }
247 }
248
249
250 while (others < rargs.length) {
251 String[] param = rargs[others].split("=");
252 assert param.length == 2;
253 log("setting " + param[0] + " to " + param[1]);
254 try {
255 BeanUtils.setProperty(asolver, param[0], param[1]);
256 } catch (Exception e) {
257 log("Cannot set parameter : "
258 + args[others]);
259 }
260 others++;
261 }
262
263 getLogWriter().println(asolver.toString(COMMENT_PREFIX));
264 return asolver;
265 } catch (ParseException e1) {
266 HelpFormatter helpf = new HelpFormatter();
267 helpf.printHelp("java -jar sat4j.jar", options, true);
268 usage();
269 }
270 return null;
271 }
272
273 @Override
274 protected Reader createReader(ISolver theSolver, String problemname) {
275 if (theSolver instanceof IPBSolver) {
276 return new PBInstanceReader((IPBSolver) theSolver);
277 }
278 return new InstanceReader(theSolver);
279 }
280
281 @Override
282 public void displayLicense() {
283 super.displayLicense();
284 log("This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details.");
285 }
286
287 @Override
288 protected String getInstanceName(String[] args) {
289 return this.filename;
290 }
291
292 @Override
293 protected IProblem readProblem(String problemname)
294 throws ParseFormatException, IOException, ContradictionException {
295 ISolver theSolver = (ISolver) super.readProblem(problemname);
296 if (this.k > 0) {
297 IVecInt literals = new VecInt();
298 for (int i = 1; i <= theSolver.nVars(); i++) {
299 literals.push(-i);
300 }
301 theSolver.addAtLeast(literals, this.k);
302 log("Limiting solutions to those having at least " + this.k
303 + " variables assigned to false");
304 }
305 return theSolver;
306 }
307
308 @Override
309 protected void solve(IProblem problem) throws TimeoutException {
310 if (this.isModeOptimization) {
311 boolean isSatisfiable = false;
312
313 IOptimizationProblem optproblem = (IOptimizationProblem) problem;
314
315 try {
316 while (optproblem.admitABetterSolution()) {
317 if (!isSatisfiable) {
318 if (optproblem.nonOptimalMeansSatisfiable()) {
319 setExitCode(ExitCode.SATISFIABLE);
320 if (optproblem.hasNoObjectiveFunction()) {
321 return;
322 }
323 log("SATISFIABLE");
324 } else if (this.incomplete) {
325 setExitCode(ExitCode.UPPER_BOUND);
326 }
327 isSatisfiable = true;
328 log("OPTIMIZING...");
329 }
330 log("Got one! Elapsed wall clock time (in seconds):"
331 + (System.currentTimeMillis() - getBeginTime())
332 / 1000.0);
333 getLogWriter().println(
334 CURRENT_OPTIMUM_VALUE_PREFIX
335 + optproblem.getObjectiveValue());
336 optproblem.discardCurrentSolution();
337 }
338 if (isSatisfiable) {
339 setExitCode(ExitCode.OPTIMUM_FOUND);
340 } else {
341 setExitCode(ExitCode.UNSATISFIABLE);
342 }
343 } catch (ContradictionException ex) {
344 assert isSatisfiable;
345 setExitCode(ExitCode.OPTIMUM_FOUND);
346 }
347 } else {
348 this.exitCode = problem.isSatisfiable() ? ExitCode.SATISFIABLE
349 : ExitCode.UNSATISFIABLE;
350 }
351 }
352
353 @Override
354 protected void displayResult() {
355 if (this.isModeOptimization) {
356 displayAnswer();
357
358 log("Total wall clock time (in seconds): "
359 + (System.currentTimeMillis() - getBeginTime()) / 1000.0);
360 } else {
361 super.displayResult();
362 }
363 }
364
365 protected void displayAnswer() {
366 if (this.solver == null) {
367 return;
368 }
369 System.out.flush();
370 PrintWriter out = getLogWriter();
371 out.flush();
372 this.solver.printStat(out, COMMENT_PREFIX);
373 this.solver.printInfos(out, COMMENT_PREFIX);
374 ExitCode exitCode = getExitCode();
375 out.println(ILauncherMode.ANSWER_PREFIX + exitCode);
376 if (exitCode == ExitCode.SATISFIABLE
377 || exitCode == ExitCode.OPTIMUM_FOUND || this.incomplete
378 && exitCode == ExitCode.UPPER_BOUND) {
379 out.print(ILauncherMode.SOLUTION_PREFIX);
380 getReader().decode(this.problem.model(), out);
381 out.println();
382 if (this.isModeOptimization) {
383 IOptimizationProblem optproblem = (IOptimizationProblem) this.problem;
384 if (!optproblem.hasNoObjectiveFunction()) {
385 log("objective function=" + optproblem.getObjectiveValue());
386 }
387 }
388 }
389 }
390
391 @Override
392 public void run(String[] args) {
393 try {
394 displayHeader();
395 this.solver = configureSolver(args);
396 if (this.solver == null) {
397 usage();
398 return;
399 }
400 if (!this.silent) {
401 this.solver.setVerbose(true);
402 }
403 String instanceName = getInstanceName(args);
404 if (instanceName == null) {
405 usage();
406 return;
407 }
408 this.beginTime = System.currentTimeMillis();
409 if (!this.launchRemoteControl) {
410 readProblem(instanceName);
411 try {
412 if (this.problem != null) {
413 solve(this.problem);
414 } else {
415 solve(this.solver);
416 }
417 } catch (TimeoutException e) {
418 log("timeout");
419 }
420 System.exit(lanceur.getExitCode().value());
421 } else {
422 RemoteControlFrame frame = new RemoteControlFrame(
423 this.filename, "", args);
424 frame.activateTracing(this.modeTracing);
425 frame.setOptimisationMode(this.isModeOptimization);
426 }
427 } catch (FileNotFoundException e) {
428 System.err.println("FATAL " + e.getLocalizedMessage());
429 } catch (IOException e) {
430 System.err.println("FATAL " + e.getLocalizedMessage());
431 } catch (ContradictionException e) {
432 this.exitCode = ExitCode.UNSATISFIABLE;
433 log("(trivial inconsistency)");
434 } catch (ParseFormatException e) {
435 System.err.println("FATAL " + e.getLocalizedMessage());
436 }
437 }
438
439 @Override
440 public void usage() {
441 Solvers.usage(this);
442 }
443
444 public static Options createCLIOptions() {
445 Options options = new Options();
446 options.addOption("l", "library", true,
447 "specifies the name of the library used (minisat by default)");
448 options.addOption("s", "solver", true,
449 "specifies the name of a prebuilt solver from the library");
450 options.addOption("S", "Solver", true,
451 "setup a solver using a solver config string");
452 options.addOption("t", "timeout", true,
453 "specifies the timeout (in seconds)");
454 options.addOption("T", "timeoutms", true,
455 "specifies the timeout (in milliseconds)");
456 options.addOption("C", "conflictbased", false,
457 "conflict based timeout (for deterministic behavior)");
458 options.addOption("d", "dot", true,
459 "creates a sat4j.dot file in current directory representing the search");
460 options.addOption("f", "filename", true,
461 "specifies the file to use (in conjunction with -d for instance)");
462 options.addOption("m", "mute", false, "Set launcher in silent mode");
463 options.addOption("k", "kleast", true,
464 "limit the search to models having at least k variables set to false");
465 options.addOption("r", "trace", false,
466 "traces the behavior of the solver");
467 options.addOption("opt", "optimize", false,
468 "uses solver in optimize mode instead of sat mode (default)");
469 options.addOption("rw", "randomWalk", true,
470 "specifies the random walk probability ");
471 options.addOption("remote", "remoteControl", false,
472 "launches remote control");
473 options.addOption("H", "hot", false,
474 "keep the solver hot (do not reset heuristics) when a model is found");
475 options.addOption("y", "simplify", false,
476 "simplify the set of clauses is possible");
477 Option op = options.getOption("l");
478 op.setArgName("libname");
479 op = options.getOption("s");
480 op.setArgName("solvername");
481 op = options.getOption("S");
482 op.setArgName("solverStringDefinition");
483 op = options.getOption("t");
484 op.setArgName(NUMBER);
485 op = options.getOption("T");
486 op.setArgName(NUMBER);
487 op = options.getOption("C");
488 op.setArgName(NUMBER);
489 op = options.getOption("k");
490 op.setArgName(NUMBER);
491 op = options.getOption("d");
492 op.setArgName("filename");
493 op = options.getOption("f");
494 op.setArgName("filename");
495 op = options.getOption("r");
496 op.setArgName("searchlistener");
497 op = options.getOption("rw");
498 op.setArgName(NUMBER);
499 return options;
500 }
501
502 }