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