1 package org.sat4j.sat;
2
3 import java.lang.reflect.InvocationTargetException;
4 import java.lang.reflect.Method;
5 import java.util.ArrayList;
6 import java.util.Arrays;
7 import java.util.HashMap;
8 import java.util.List;
9 import java.util.Map;
10 import java.util.Properties;
11 import java.util.Set;
12 import java.util.StringTokenizer;
13
14 import org.apache.commons.beanutils.BeanUtils;
15 import org.apache.commons.cli.CommandLine;
16 import org.apache.commons.cli.HelpFormatter;
17 import org.apache.commons.cli.Option;
18 import org.apache.commons.cli.Options;
19 import org.apache.commons.cli.ParseException;
20 import org.apache.commons.cli.PosixParser;
21 import org.sat4j.core.ASolverFactory;
22 import org.sat4j.minisat.core.DataStructureFactory;
23 import org.sat4j.minisat.core.ICDCL;
24 import org.sat4j.minisat.core.IOrder;
25 import org.sat4j.minisat.core.IPhaseSelectionStrategy;
26 import org.sat4j.minisat.core.LearnedConstraintsEvaluationType;
27 import org.sat4j.minisat.core.LearningStrategy;
28 import org.sat4j.minisat.core.RestartStrategy;
29 import org.sat4j.minisat.core.SearchParams;
30 import org.sat4j.minisat.core.SimplificationType;
31 import org.sat4j.minisat.core.Solver;
32 import org.sat4j.minisat.orders.RandomWalkDecorator;
33 import org.sat4j.minisat.orders.VarOrderHeap;
34 import org.sat4j.pb.orders.RandomWalkDecoratorObjective;
35 import org.sat4j.pb.orders.VarOrderHeapObjective;
36 import org.sat4j.specs.ILogAble;
37 import org.sat4j.specs.ISolver;
38 import org.sat4j.tools.DotSearchTracing;
39
40 public final class Solvers {
41
42 private static final String SEPARATOR = "-------------------";
43 private static final String CLASS = "class";
44 private static final String OPB = "opb";
45 private static final String CNF = "cnf";
46 private static final String MAXSAT = "maxsat";
47 private static final String OPT = "opt";
48 private static final String FILENAME = "filename";
49 private static final String NUMBER = "number";
50 private static final String PROBLEM_WITH_COMPONENT = "Problem with component ";
51 private static final String PB = "pb";
52 private static final String MINISAT = "minisat";
53 public static final String ORDERS = "ORDERS";
54 public static final String LEARNING = "LEARNING";
55 public static final String RESTARTS = "RESTARTS";
56 public static final String PHASE = "PHASE";
57 public static final String PARAMS = "PARAMS";
58 public static final String SIMP = "SIMP";
59 public static final String CLEANING = "CLEANING";
60
61 private static final String PACKAGE_ORDERS = "org.sat4j.minisat.orders";
62 private static final String PACKAGE_LEARNING = "org.sat4j.minisat.learning";
63 private static final String PACKAGE_RESTARTS = "org.sat4j.minisat.restarts";
64 private static final String PACKAGE_PHASE = "org.sat4j.minisat.orders";
65 private static final String PACKAGE_PARAMS = "org.sat4j.minisat.core";
66
67 private static final String RESTART_STRATEGY_NAME = "org.sat4j.minisat.core.RestartStrategy";
68 private static final String ORDER_NAME = "org.sat4j.minisat.core.IOrder";
69 private static final String LEARNING_NAME = "org.sat4j.minisat.core.LearningStrategy";
70 private static final String PHASE_NAME = "org.sat4j.minisat.core.IPhaseSelectionStrategy";
71 private static final String PARAMS_NAME = "org.sat4j.minisat.core.SearchParams";
72
73 private static final Map<String, String> QUALIF = new HashMap<String, String>();
74 static {
75 QUALIF.put(ORDERS, PACKAGE_ORDERS);
76 QUALIF.put(LEARNING, PACKAGE_LEARNING);
77 QUALIF.put(RESTARTS, PACKAGE_RESTARTS);
78 QUALIF.put(PHASE, PACKAGE_PHASE);
79 QUALIF.put(PARAMS, PACKAGE_PARAMS);
80 }
81
82 private Solvers() {
83 }
84
85 protected static ICDCL configureFromString(String solverconfig,
86 ICDCL theSolver, ILogAble logger) {
87 assert theSolver != null;
88
89
90 StringTokenizer stk = new StringTokenizer(solverconfig, ",");
91 Properties pf = new Properties();
92 String token;
93 String[] couple;
94 while (stk.hasMoreElements()) {
95 token = stk.nextToken();
96 couple = token.split("=");
97 pf.setProperty(couple[0], couple[1]);
98 }
99
100 Solver aSolver = (Solver) theSolver;
101 DataStructureFactory dsf = setupObject("DSF", pf, logger);
102 if (dsf != null) {
103 theSolver.setDataStructureFactory(dsf);
104 }
105 LearningStrategy learning = setupObject(LEARNING, pf, logger);
106 if (learning != null) {
107 theSolver.setLearningStrategy(learning);
108 learning.setSolver(aSolver);
109 }
110 IOrder order = setupObject(ORDERS, pf, logger);
111 if (order != null) {
112 theSolver.setOrder(order);
113 }
114 IPhaseSelectionStrategy pss = setupObject(PHASE, pf, logger);
115 if (pss != null) {
116 theSolver.getOrder().setPhaseSelectionStrategy(pss);
117 }
118 RestartStrategy restarter = setupObject(RESTARTS, pf, logger);
119 if (restarter != null) {
120 theSolver.setRestartStrategy(restarter);
121 }
122 String simp = pf.getProperty(SIMP);
123 if (simp != null) {
124 logger.log("read " + simp);
125 logger.log("configuring " + SIMP);
126 theSolver.setSimplifier(SimplificationType.valueOf(simp));
127 }
128 SearchParams params = setupObject(PARAMS, pf, logger);
129 if (params != null) {
130 theSolver.setSearchParams(params);
131 }
132 String memory = pf.getProperty(CLEANING);
133 if (memory != null) {
134 try {
135 logger.log("configuring "+CLEANING);
136 LearnedConstraintsEvaluationType memoryType = LearnedConstraintsEvaluationType
137 .valueOf(memory);
138 theSolver.setLearnedConstraintsDeletionStrategy(memoryType);
139 } catch (IllegalArgumentException iae) {
140 logger.log("wrong memory management setting: " + memory);
141 showAvailableConstraintsCleaningStrategies(logger);
142 }
143 }
144 return theSolver;
145 }
146
147 private static <T> T setupObject(String component, Properties pf,
148 ILogAble logger) {
149 try {
150 String configline = pf.getProperty(component);
151 String qualification = QUALIF.get(component);
152
153 if (configline == null) {
154 return null;
155 }
156 if (qualification != null) {
157 logger.log("read " + qualification + "." + configline);
158 if (configline.contains("Objective")
159 && qualification.contains(MINISAT)) {
160 qualification = qualification.replaceFirst(MINISAT, PB);
161 }
162 configline = qualification + "." + configline;
163 }
164
165 logger.log("configuring " + component);
166 String[] config = configline.split("/");
167 T comp = (T) Class.forName(config[0]).newInstance();
168 for (int i = 1; i < config.length; i++) {
169 String[] param = config[i].split(":");
170 assert param.length == 2;
171 try {
172
173 BeanUtils.getProperty(comp, param[0]);
174 BeanUtils.setProperty(comp, param[0], param[1]);
175 } catch (Exception e) {
176 logger.log(PROBLEM_WITH_COMPONENT + config[0] + " " + e);
177 }
178 }
179 return comp;
180 } catch (InstantiationException e) {
181 logger.log(PROBLEM_WITH_COMPONENT + component + " " + e);
182 } catch (IllegalAccessException e) {
183 logger.log(PROBLEM_WITH_COMPONENT + component + " " + e);
184 } catch (ClassNotFoundException e) {
185 logger.log(PROBLEM_WITH_COMPONENT + component + " " + e);
186 }
187 return null;
188 }
189
190 public static Options createCLIOptions() {
191 Options options = new Options();
192 options.addOption(
193 "l",
194 "library",
195 true,
196 "specifies the name of the library used (if not present, the library depends on the file extension)");
197 options.addOption("s", "solver", true,
198 "specifies the name of a prebuilt solver from the library");
199 options.addOption("S", "Solver", true,
200 "setup a solver using a solver config string");
201 options.addOption("t", "timeout", true,
202 "specifies the timeout (in seconds)");
203 options.addOption("T", "timeoutms", true,
204 "specifies the timeout (in milliseconds)");
205 options.addOption("C", "conflictbased", false,
206 "conflict based timeout (for deterministic behavior)");
207 options.addOption("d", "dot", true,
208 "creates a sat4j.dot file in current directory representing the search");
209 options.addOption("f", FILENAME, true,
210 "specifies the file to use (in conjunction with -d for instance)");
211 options.addOption("m", "mute", false, "Set launcher in silent mode");
212 options.addOption("k", "kleast", true,
213 "limit the search to models having at least k variables set to false");
214 options.addOption("tr", "trace", false,
215 "traces the behavior of the solver");
216 options.addOption(OPT, "optimize", false,
217 "uses solver in optimize mode instead of sat mode (default)");
218 options.addOption("rw", "randomWalk", true,
219 "specifies the random walk probability ");
220 options.addOption("remote", "remoteControl", false,
221 "launches remote control");
222 options.addOption("r", "trace", false,
223 "traces the behavior of the solver");
224 options.addOption("H", "hot", false,
225 "keep the solver hot (do not reset heuristics) when a model is found");
226 options.addOption("y", "simplify", false,
227 "simplify the set of clauses if possible");
228 options.addOption("lo", "lower", false,
229 "search solution by lower bounding instead of by upper bounding");
230 options.addOption("e", "equivalence", false,
231 "Use an equivalence instead of an implication for the selector variables");
232 options.addOption("i", "incomplete", false,
233 "incomplete mode for maxsat");
234 options.addOption("n", "no solution line", false,
235 "Do not display a solution line (useful if the solution is large)");
236 Option op = options.getOption("l");
237 op.setArgName("libname");
238 op = options.getOption("s");
239 op.setArgName("solvername");
240 op = options.getOption("S");
241 op.setArgName("solverStringDefinition");
242 op = options.getOption("t");
243 op.setArgName(NUMBER);
244 op = options.getOption("T");
245 op.setArgName(NUMBER);
246 op = options.getOption("C");
247 op.setArgName(NUMBER);
248 op = options.getOption("k");
249 op.setArgName(NUMBER);
250 op = options.getOption("d");
251 op.setArgName(FILENAME);
252 op = options.getOption("f");
253 op.setArgName(FILENAME);
254 op = options.getOption("rw");
255 op.setArgName(NUMBER);
256 return options;
257 }
258
259 public static void stringUsage(ILogAble logger) {
260 logger.log("Available building blocks: DSF, LEARNING, ORDERS, PHASE, RESTARTS, SIMP, PARAMS, CLEANING");
261 logger.log("Example: -S RESTARTS=LubyRestarts/factor:512,LEARNING=MiniSATLearning");
262 }
263
264 public static boolean containsOptValue(String[] args) {
265 Options options = createCLIOptions();
266 try {
267 CommandLine cmd = new PosixParser().parse(options, args);
268 return cmd.hasOption(OPT);
269 } catch (ParseException e) {
270 return false;
271 }
272 }
273
274 public static ICDCL configureSolver(String[] args, ILogAble logger) {
275 Options options = createCLIOptions();
276 if (args.length == 0) {
277 HelpFormatter helpf = new HelpFormatter();
278 helpf.printHelp("java -jar sat4j.jar", options, true);
279
280 return null;
281 }
282 try {
283 CommandLine cmd = new PosixParser().parse(options, args);
284
285 boolean isModeOptimization = false;
286 ASolverFactory<ISolver> factory;
287
288 if (cmd.hasOption(OPT)) {
289 isModeOptimization = true;
290 }
291
292 String filename = cmd.getOptionValue("f");
293
294 String[] rargs = cmd.getArgs();
295 if (filename == null && rargs.length > 0) {
296 filename = rargs[0];
297 }
298 String unzipped = uncompressed(filename);
299
300 String framework = cmd.getOptionValue("l");
301 if (framework == null) {
302 if (isModeOptimization) {
303 if (unzipped != null && unzipped.endsWith(CNF)) {
304 framework = MAXSAT;
305 } else {
306 framework = PB;
307 }
308 } else if (unzipped != null && unzipped.endsWith(OPB)) {
309 framework = PB;
310 } else {
311 framework = MINISAT;
312 }
313 }
314
315 try {
316 Class<?> clazz = Class
317 .forName("org.sat4j." + framework + ".SolverFactory");
318 Class<?>[] params = {};
319 Method m = clazz.getMethod("instance", params);
320 factory = (ASolverFactory) m.invoke(null, (Object[]) null);
321 } catch (Exception e) {
322 logger.log("Wrong framework: " + framework
323 + ". Using minisat instead.");
324 factory = org.sat4j.minisat.SolverFactory.instance();
325 }
326
327 ICDCL asolver;
328 if (cmd.hasOption("s")) {
329 String solvername = cmd.getOptionValue("s");
330 if (solvername == null) {
331 logger.log("No solver for option s. Launching default solver.");
332 logger.log("Available solvers: "
333 + Arrays.asList(factory.solverNames()));
334 asolver = (Solver) factory.defaultSolver();
335 } else {
336 asolver = (Solver) factory.createSolverByName(solvername);
337 }
338 } else {
339 asolver = (Solver) factory.defaultSolver();
340 }
341
342 if (cmd.hasOption("S")) {
343 String configuredSolver = cmd.getOptionValue("S");
344 if (configuredSolver == null) {
345 stringUsage(logger);
346 return null;
347 }
348 asolver = Solvers.configureFromString(configuredSolver,
349 asolver, logger);
350 }
351
352 if (cmd.hasOption("rw")) {
353 double proba = Double.parseDouble(cmd.getOptionValue("rw"));
354 IOrder order = asolver.getOrder();
355 if (isModeOptimization
356 && order instanceof VarOrderHeapObjective) {
357 order = new RandomWalkDecoratorObjective(
358 (VarOrderHeapObjective) order, proba);
359 } else {
360 order = new RandomWalkDecorator((VarOrderHeap) order, proba);
361 }
362 asolver.setOrder(order);
363 }
364
365 String timeout = cmd.getOptionValue("t");
366 if (timeout == null) {
367 timeout = cmd.getOptionValue("T");
368 if (timeout != null) {
369 asolver.setTimeoutMs(Long.parseLong(timeout));
370 }
371 } else {
372 if (cmd.hasOption("C")) {
373 asolver.setTimeoutOnConflicts(Integer.parseInt(timeout));
374 } else {
375 asolver.setTimeout(Integer.parseInt(timeout));
376 }
377 }
378
379 if (cmd.hasOption("H")) {
380 asolver.setKeepSolverHot(true);
381 }
382
383 if (cmd.hasOption("y")) {
384 asolver.setDBSimplificationAllowed(true);
385 }
386
387 if (cmd.hasOption("d")) {
388 String dotfilename = null;
389 if (filename != null) {
390 dotfilename = cmd.getOptionValue("d");
391 }
392 if (dotfilename == null) {
393 dotfilename = "sat4j.dot";
394 }
395 asolver.setSearchListener(new DotSearchTracing(dotfilename,
396 null));
397 }
398
399 return asolver;
400 } catch (ParseException e1) {
401 HelpFormatter helpf = new HelpFormatter();
402 helpf.printHelp("java -jar sat4j.jar", options, true);
403 usage(logger);
404 }
405 return null;
406 }
407
408 public static String uncompressed(String filename) {
409 if (filename != null
410 && (filename.endsWith(".bz2") || filename.endsWith(".gz"))) {
411 return filename.substring(0, filename.lastIndexOf('.'));
412 }
413 return filename;
414 }
415
416 public static void showAvailableRestarts(ILogAble logger) {
417 List<String> classNames = new ArrayList<String>();
418 List<String> resultRTSI = RTSI.find(RESTART_STRATEGY_NAME);
419 Set<String> keySet;
420 for (String name : resultRTSI) {
421 if (!name.contains("Remote")) {
422 try {
423 keySet = BeanUtils
424 .describe(
425 Class.forName(
426 Solvers.PACKAGE_RESTARTS + "."
427 + name).newInstance())
428 .keySet();
429 keySet.remove(CLASS);
430 if (keySet.size() > 0) {
431 classNames.add(name + keySet);
432 } else {
433 classNames.add(name);
434 }
435 } catch (IllegalAccessException e) {
436 logger.log(e.getMessage());
437 } catch (InvocationTargetException e) {
438 logger.log(e.getMessage());
439 } catch (NoSuchMethodException e) {
440 logger.log(e.getMessage());
441 } catch (InstantiationException e) {
442 logger.log(e.getMessage());
443 } catch (ClassNotFoundException e) {
444 logger.log(e.getMessage());
445 }
446 }
447 }
448 logger.log("Available restart strategies (" + Solvers.RESTARTS + "): "
449 + classNames);
450 }
451
452 public static void showAvailablePhase(ILogAble logger) {
453 List<String> classNames = new ArrayList<String>();
454 List<String> resultRTSI = RTSI.find(PHASE_NAME);
455 Set<String> keySet;
456 for (String name : resultRTSI) {
457 if (!name.contains("Remote")) {
458 try {
459
460 keySet = BeanUtils.describe(
461 Class.forName(PACKAGE_PHASE + "." + name)
462 .newInstance()).keySet();
463 keySet.remove(CLASS);
464 if (keySet.size() > 0) {
465 classNames.add(name + keySet);
466 } else {
467 classNames.add(name);
468 }
469 } catch (IllegalAccessException e) {
470 logger.log(e.getMessage());
471 } catch (InvocationTargetException e) {
472 logger.log(e.getMessage());
473 } catch (NoSuchMethodException e) {
474 logger.log(e.getMessage());
475 } catch (InstantiationException e) {
476 logger.log(e.getMessage());
477 } catch (ClassNotFoundException e) {
478 logger.log(e.getMessage());
479 }
480 }
481 }
482 logger.log("Available phase strategies (" + Solvers.PHASE + "): "
483 + classNames);
484 }
485
486 public static void showAvailableLearning(ILogAble logger) {
487 List<String> classNames = new ArrayList<String>();
488 List<String> resultRTSI = RTSI.find(LEARNING_NAME);
489 Set<String> keySet;
490 for (String name : resultRTSI) {
491 try {
492 keySet = BeanUtils.describe(
493 Class.forName(PACKAGE_LEARNING + "." + name)
494 .newInstance()).keySet();
495 keySet.remove(CLASS);
496 if (keySet.size() > 0) {
497 classNames.add(name + keySet);
498 } else {
499 classNames.add(name);
500 }
501 } catch (IllegalAccessException e) {
502 logger.log(e.getMessage());
503 } catch (InvocationTargetException e) {
504 logger.log(e.getMessage());
505 } catch (NoSuchMethodException e) {
506 logger.log(e.getMessage());
507 } catch (InstantiationException e) {
508 classNames.add(name);
509 } catch (ClassNotFoundException e) {
510 logger.log(e.getMessage());
511 } catch (NoClassDefFoundError cnfex) {
512 logger.log(cnfex.getMessage());
513 }
514 }
515 logger.log("Available learning (" + Solvers.LEARNING + "): "
516 + classNames);
517 }
518
519 public static void showAvailableOrders(ILogAble logger) {
520 List<String> classNames = new ArrayList<String>();
521 List<String> resultRTSI = RTSI.find(ORDER_NAME);
522 Set<String> keySet = null;
523 for (String name : resultRTSI) {
524 if (!name.contains("Remote")) {
525 try {
526 if (name.contains("Objective")) {
527 String namePackage = Solvers.PACKAGE_ORDERS
528 .replaceFirst(MINISAT, PB);
529 keySet = BeanUtils.describe(
530 Class.forName(namePackage + "." + name)
531 .newInstance()).keySet();
532 } else {
533 keySet = BeanUtils.describe(
534 Class.forName(
535 Solvers.PACKAGE_ORDERS + "." + name)
536 .newInstance()).keySet();
537 }
538 keySet.remove(CLASS);
539
540 if (keySet.size() > 0) {
541 classNames.add(name + keySet);
542 } else {
543 classNames.add(name);
544 }
545
546 } catch (IllegalAccessException e) {
547 logger.log(e.getMessage());
548 } catch (InvocationTargetException e) {
549 logger.log(e.getMessage());
550 } catch (NoSuchMethodException e) {
551 logger.log(e.getMessage());
552 } catch (InstantiationException e) {
553 logger.log(e.getMessage());
554 } catch (ClassNotFoundException e) {
555 logger.log(e.getMessage());
556 }
557 }
558 }
559 logger.log("Available orders (" + Solvers.ORDERS + "): " + classNames);
560 }
561
562 public static void showParams(ILogAble logger) {
563
564 Set<String> keySet = null;
565 try {
566 keySet = BeanUtils.describe(
567 Class.forName(PARAMS_NAME).newInstance()).keySet();
568 keySet.remove(CLASS);
569 } catch (IllegalAccessException e) {
570 logger.log(e.getMessage());
571 } catch (InvocationTargetException e) {
572 logger.log(e.getMessage());
573 } catch (NoSuchMethodException e) {
574 logger.log(e.getMessage());
575 } catch (InstantiationException e) {
576 logger.log(e.getMessage());
577 } catch (ClassNotFoundException e) {
578 logger.log(e.getMessage());
579 }
580 logger.log("Available search params (" + Solvers.PARAMS
581 + "): [SearchParams" + keySet + "]");
582 }
583
584 public static void showSimplifiers(ILogAble logger) {
585 logger.log("Available simplifiers ("+Solvers.SIMP+"): [NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION]");
586 }
587
588 public static void showAvailableConstraintsCleaningStrategies(
589 ILogAble logger) {
590 logger.log("Available learned constraints cleaning strategies ("+Solvers.CLEANING+"): "
591 + Arrays.asList(LearnedConstraintsEvaluationType.values()));
592 }
593
594 public static <T extends ISolver> void showAvailableSolvers(
595 ASolverFactory<T> afactory, ILogAble logger) {
596 showAvailableSolvers(afactory, "", logger);
597 }
598
599 public static <T extends ISolver> void showAvailableSolvers(
600 ASolverFactory<T> afactory, String framework, ILogAble logger) {
601 if (afactory != null) {
602 if (framework.length() > 0) {
603 logger.log("Available solvers for " + framework + ": ");
604 } else {
605 logger.log("Available solvers: ");
606 }
607 String[] names = afactory.solverNames();
608 for (String name : names) {
609 logger.log(name);
610 }
611 }
612 }
613
614 public static void usage(ILogAble logger) {
615 ASolverFactory<ISolver> factory;
616 factory = org.sat4j.minisat.SolverFactory.instance();
617 showAvailableSolvers(factory, "sat", logger);
618 logger.log(SEPARATOR);
619 factory = (ASolverFactory) org.sat4j.pb.SolverFactory.instance();
620 showAvailableSolvers(factory, PB, logger);
621 logger.log(SEPARATOR);
622 factory = (ASolverFactory) org.sat4j.maxsat.SolverFactory.instance();
623 showAvailableSolvers(factory, MAXSAT, logger);
624 logger.log(SEPARATOR);
625 showAvailableRestarts(logger);
626 logger.log(SEPARATOR);
627 showAvailableOrders(logger);
628 logger.log(SEPARATOR);
629 showAvailableLearning(logger);
630 logger.log(SEPARATOR);
631 showAvailablePhase(logger);
632 logger.log(SEPARATOR);
633 showParams(logger);
634 logger.log(SEPARATOR);
635 showSimplifiers(logger);
636 logger.log(SEPARATOR);
637 showAvailableConstraintsCleaningStrategies(logger);
638 logger.log(SEPARATOR);
639 stringUsage(logger);
640 }
641
642 }