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