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
60 private static final String PACKAGE_ORDERS = "org.sat4j.minisat.orders";
61 private static final String PACKAGE_LEARNING = "org.sat4j.minisat.learning";
62 private static final String PACKAGE_RESTARTS = "org.sat4j.minisat.restarts";
63 private static final String PACKAGE_PHASE = "org.sat4j.minisat.orders";
64 private static final String PACKAGE_PARAMS = "org.sat4j.minisat.core";
65
66 private static final String RESTART_STRATEGY_NAME = "org.sat4j.minisat.core.RestartStrategy";
67 private static final String ORDER_NAME = "org.sat4j.minisat.core.IOrder";
68 private static final String LEARNING_NAME = "org.sat4j.minisat.core.LearningStrategy";
69 private static final String PHASE_NAME = "org.sat4j.minisat.core.IPhaseSelectionStrategy";
70 private static final String PARAMS_NAME = "org.sat4j.minisat.core.SearchParams";
71
72 private static final Map<String, String> QUALIF = new HashMap<String, String>();
73 static {
74 QUALIF.put(ORDERS, PACKAGE_ORDERS);
75 QUALIF.put(LEARNING, PACKAGE_LEARNING);
76 QUALIF.put(RESTARTS, PACKAGE_RESTARTS);
77 QUALIF.put(PHASE, PACKAGE_PHASE);
78 QUALIF.put(PARAMS, PACKAGE_PARAMS);
79 }
80
81 private Solvers() {
82 }
83
84 protected static ICDCL configureFromString(String solverconfig,
85 ICDCL theSolver, ILogAble logger) {
86 assert theSolver != null;
87
88
89 StringTokenizer stk = new StringTokenizer(solverconfig, ",");
90 Properties pf = new Properties();
91 String token;
92 String[] couple;
93 while (stk.hasMoreElements()) {
94 token = stk.nextToken();
95 couple = token.split("=");
96 pf.setProperty(couple[0], couple[1]);
97 }
98
99 Solver aSolver = (Solver) theSolver;
100 DataStructureFactory dsf = setupObject("DSF", pf, logger);
101 if (dsf != null) {
102 theSolver.setDataStructureFactory(dsf);
103 }
104 LearningStrategy learning = setupObject(LEARNING, pf, logger);
105 if (learning != null) {
106 theSolver.setLearningStrategy(learning);
107 learning.setSolver(aSolver);
108 }
109 IOrder order = setupObject(ORDERS, pf, logger);
110 if (order != null) {
111 theSolver.setOrder(order);
112 }
113 IPhaseSelectionStrategy pss = setupObject(PHASE, pf, logger);
114 if (pss != null) {
115 theSolver.getOrder().setPhaseSelectionStrategy(pss);
116 }
117 RestartStrategy restarter = setupObject(RESTARTS, pf, logger);
118 if (restarter != null) {
119 theSolver.setRestartStrategy(restarter);
120 }
121 String simp = pf.getProperty(SIMP);
122 if (simp != null) {
123 logger.log("read " + simp);
124 logger.log("configuring " + SIMP);
125 theSolver.setSimplifier(SimplificationType.valueOf(simp));
126 }
127 SearchParams params = setupObject(PARAMS, pf, logger);
128 if (params != null) {
129 theSolver.setSearchParams(params);
130 }
131 String memory = pf.getProperty("CLEANING");
132 if (memory != null) {
133 try {
134 logger.log("configuring CLEANING");
135 LearnedConstraintsEvaluationType memoryType = LearnedConstraintsEvaluationType
136 .valueOf(memory);
137 theSolver.setLearnedConstraintsDeletionStrategy(memoryType);
138 } catch (IllegalArgumentException iae) {
139 logger.log("wrong memory management setting: " + memory);
140 showAvailableConstraintsCleaningStrategies(logger);
141 }
142 }
143 return theSolver;
144 }
145
146 private static <T> T setupObject(String component, Properties pf,
147 ILogAble logger) {
148 try {
149 String configline = pf.getProperty(component);
150 String qualification = QUALIF.get(component);
151
152 if (configline == null) {
153 return null;
154 }
155 if (qualification != null) {
156 logger.log("read " + qualification + "." + configline);
157 if (configline.contains("Objective")
158 && qualification.contains(MINISAT)) {
159 qualification = qualification.replaceFirst(MINISAT, PB);
160 }
161 configline = qualification + "." + configline;
162 }
163
164 logger.log("configuring " + component);
165 String[] config = configline.split("/");
166 T comp = (T) Class.forName(config[0]).newInstance();
167 for (int i = 1; i < config.length; i++) {
168 String[] param = config[i].split(":");
169 assert param.length == 2;
170 try {
171
172 BeanUtils.getProperty(comp, param[0]);
173 BeanUtils.setProperty(comp, param[0], param[1]);
174 } catch (Exception e) {
175 logger.log(PROBLEM_WITH_COMPONENT + config[0] + " " + e);
176 }
177 }
178 return comp;
179 } catch (InstantiationException e) {
180 logger.log(PROBLEM_WITH_COMPONENT + component + " " + e);
181 } catch (IllegalAccessException e) {
182 logger.log(PROBLEM_WITH_COMPONENT + component + " " + e);
183 } catch (ClassNotFoundException e) {
184 logger.log(PROBLEM_WITH_COMPONENT + component + " " + e);
185 }
186 return null;
187 }
188
189 public static Options createCLIOptions() {
190 Options options = new Options();
191 options.addOption(
192 "l",
193 "library",
194 true,
195 "specifies the name of the library used (if not present, the library depends on the file extension)");
196 options.addOption("s", "solver", true,
197 "specifies the name of a prebuilt solver from the library");
198 options.addOption("S", "Solver", true,
199 "setup a solver using a solver config string");
200 options.addOption("t", "timeout", true,
201 "specifies the timeout (in seconds)");
202 options.addOption("T", "timeoutms", true,
203 "specifies the timeout (in milliseconds)");
204 options.addOption("C", "conflictbased", false,
205 "conflict based timeout (for deterministic behavior)");
206 options.addOption("d", "dot", true,
207 "creates a sat4j.dot file in current directory representing the search");
208 options.addOption("f", FILENAME, true,
209 "specifies the file to use (in conjunction with -d for instance)");
210 options.addOption("m", "mute", false, "Set launcher in silent mode");
211 options.addOption("k", "kleast", true,
212 "limit the search to models having at least k variables set to false");
213 options.addOption("tr", "trace", false,
214 "traces the behavior of the solver");
215 options.addOption(OPT, "optimize", false,
216 "uses solver in optimize mode instead of sat mode (default)");
217 options.addOption("rw", "randomWalk", true,
218 "specifies the random walk probability ");
219 options.addOption("remote", "remoteControl", false,
220 "launches remote control");
221 options.addOption("r", "trace", false,
222 "traces the behavior of the solver");
223 options.addOption("H", "hot", false,
224 "keep the solver hot (do not reset heuristics) when a model is found");
225 options.addOption("y", "simplify", false,
226 "simplify the set of clauses if possible");
227 options.addOption("lo", "lower", false,
228 "search solution by lower bounding instead of by upper bounding");
229 options.addOption("e", "equivalence", false,
230 "Use an equivalence instead of an implication for the selector variables");
231 options.addOption("i", "incomplete", false,
232 "incomplete mode for maxsat");
233 options.addOption("n", "no solution line", false,
234 "Do not display a solution line (useful if the solution is large)");
235 Option op = options.getOption("l");
236 op.setArgName("libname");
237 op = options.getOption("s");
238 op.setArgName("solvername");
239 op = options.getOption("S");
240 op.setArgName("solverStringDefinition");
241 op = options.getOption("t");
242 op.setArgName(NUMBER);
243 op = options.getOption("T");
244 op.setArgName(NUMBER);
245 op = options.getOption("C");
246 op.setArgName(NUMBER);
247 op = options.getOption("k");
248 op.setArgName(NUMBER);
249 op = options.getOption("d");
250 op.setArgName(FILENAME);
251 op = options.getOption("f");
252 op.setArgName(FILENAME);
253 op = options.getOption("rw");
254 op.setArgName(NUMBER);
255 return options;
256 }
257
258 public static void stringUsage(ILogAble logger) {
259 logger.log("Available building blocks: DSF, LEARNING, ORDERS, PHASE, RESTARTS, SIMP, PARAMS, CLEANING");
260 logger.log("Example: -S RESTARTS=LubyRestarts/factor:512,LEARNING=MiniSATLearning");
261 }
262
263 public static boolean containsOptValue(String[] args) {
264 Options options = createCLIOptions();
265 try {
266 CommandLine cmd = new PosixParser().parse(options, args);
267 return cmd.hasOption(OPT);
268 } catch (ParseException e) {
269 return false;
270 }
271 }
272
273 public static ICDCL configureSolver(String[] args, ILogAble logger) {
274 Options options = createCLIOptions();
275 if (args.length == 0) {
276 HelpFormatter helpf = new HelpFormatter();
277 helpf.printHelp("java -jar sat4j.jar", options, true);
278
279 return null;
280 }
281 try {
282 CommandLine cmd = new PosixParser().parse(options, args);
283
284 boolean isModeOptimization = false;
285 ASolverFactory<ISolver> factory;
286
287 if (cmd.hasOption(OPT)) {
288 isModeOptimization = true;
289 }
290
291 String filename = cmd.getOptionValue("f");
292
293 String[] rargs = cmd.getArgs();
294 if (filename == null && rargs.length > 0) {
295 filename = rargs[0];
296 }
297 String unzipped = uncompressed(filename);
298
299 String framework = cmd.getOptionValue("l");
300 if (framework == null) {
301 if (isModeOptimization) {
302 if (unzipped != null && unzipped.endsWith(CNF)) {
303 framework = MAXSAT;
304 } else {
305 framework = PB;
306 }
307 } else if (unzipped != null && unzipped.endsWith(OPB)) {
308 framework = PB;
309 } else {
310 framework = MINISAT;
311 }
312 }
313
314 try {
315 Class<?> clazz = Class
316 .forName("org.sat4j." + framework + ".SolverFactory");
317 Class<?>[] params = {};
318 Method m = clazz.getMethod("instance", params);
319 factory = (ASolverFactory) m.invoke(null, (Object[]) null);
320 } catch (Exception e) {
321 logger.log("Wrong framework: " + framework
322 + ". Using minisat instead.");
323 factory = org.sat4j.minisat.SolverFactory.instance();
324 }
325
326 ICDCL asolver;
327 if (cmd.hasOption("s")) {
328 String solvername = cmd.getOptionValue("s");
329 if (solvername == null) {
330 logger.log("No solver for option s. Launching default solver.");
331 logger.log("Available solvers: "
332 + Arrays.asList(factory.solverNames()));
333 asolver = (Solver) factory.defaultSolver();
334 } else {
335 asolver = (Solver) factory.createSolverByName(solvername);
336 }
337 } else {
338 asolver = (Solver) factory.defaultSolver();
339 }
340
341 if (cmd.hasOption("S")) {
342 String configuredSolver = cmd.getOptionValue("S");
343 if (configuredSolver == null) {
344 stringUsage(logger);
345 return null;
346 }
347 asolver = Solvers.configureFromString(configuredSolver,
348 asolver, logger);
349 }
350
351 if (cmd.hasOption("rw")) {
352 double proba = Double.parseDouble(cmd.getOptionValue("rw"));
353 IOrder order = asolver.getOrder();
354 if (isModeOptimization
355 && order instanceof VarOrderHeapObjective) {
356 order = new RandomWalkDecoratorObjective(
357 (VarOrderHeapObjective) order, proba);
358 } else {
359 order = new RandomWalkDecorator((VarOrderHeap) order, proba);
360 }
361 asolver.setOrder(order);
362 }
363
364 String timeout = cmd.getOptionValue("t");
365 if (timeout == null) {
366 timeout = cmd.getOptionValue("T");
367 if (timeout != null) {
368 asolver.setTimeoutMs(Long.parseLong(timeout));
369 }
370 } else {
371 if (cmd.hasOption("C")) {
372 asolver.setTimeoutOnConflicts(Integer.parseInt(timeout));
373 } else {
374 asolver.setTimeout(Integer.parseInt(timeout));
375 }
376 }
377
378 if (cmd.hasOption("H")) {
379 asolver.setKeepSolverHot(true);
380 }
381
382 if (cmd.hasOption("y")) {
383 asolver.setDBSimplificationAllowed(true);
384 }
385
386 if (cmd.hasOption("d")) {
387 String dotfilename = null;
388 if (filename != null) {
389 dotfilename = cmd.getOptionValue("d");
390 }
391 if (dotfilename == null) {
392 dotfilename = "sat4j.dot";
393 }
394 asolver.setSearchListener(new DotSearchTracing(dotfilename,
395 null));
396 }
397
398 return asolver;
399 } catch (ParseException e1) {
400 HelpFormatter helpf = new HelpFormatter();
401 helpf.printHelp("java -jar sat4j.jar", options, true);
402 usage(logger);
403 }
404 return null;
405 }
406
407 public static String uncompressed(String filename) {
408 if (filename != null
409 && (filename.endsWith(".bz2") || filename.endsWith(".gz"))) {
410 return filename.substring(0, filename.lastIndexOf('.'));
411 }
412 return filename;
413 }
414
415 public static void showAvailableRestarts(ILogAble logger) {
416 List<String> classNames = new ArrayList<String>();
417 List<String> resultRTSI = RTSI.find(RESTART_STRATEGY_NAME);
418 Set<String> keySet;
419 for (String name : resultRTSI) {
420 if (!name.contains("Remote")) {
421 try {
422 keySet = BeanUtils
423 .describe(
424 Class.forName(
425 Solvers.PACKAGE_RESTARTS + "."
426 + name).newInstance())
427 .keySet();
428 keySet.remove(CLASS);
429 if (keySet.size() > 0) {
430 classNames.add(name + keySet);
431 } else {
432 classNames.add(name);
433 }
434 } catch (IllegalAccessException e) {
435 logger.log(e.getMessage());
436 } catch (InvocationTargetException e) {
437 logger.log(e.getMessage());
438 } catch (NoSuchMethodException e) {
439 logger.log(e.getMessage());
440 } catch (InstantiationException e) {
441 logger.log(e.getMessage());
442 } catch (ClassNotFoundException e) {
443 logger.log(e.getMessage());
444 }
445 }
446 }
447 classNames.add("Glucose21Restarts");
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 : [NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION]");
586 }
587
588 public static void showAvailableConstraintsCleaningStrategies(
589 ILogAble logger) {
590 logger.log("Available learned constraints cleaning strategies"
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 stringUsage(logger);
638 }
639
640 }