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.maxsat;
31
32 import org.apache.commons.cli.CommandLine;
33 import org.apache.commons.cli.HelpFormatter;
34 import org.apache.commons.cli.Options;
35 import org.apache.commons.cli.ParseException;
36 import org.apache.commons.cli.PosixParser;
37 import org.sat4j.AbstractLauncher;
38 import org.sat4j.AbstractOptimizationLauncher;
39 import org.sat4j.maxsat.reader.WDimacsReader;
40 import org.sat4j.opt.MinOneDecorator;
41 import org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator;
42 import org.sat4j.pb.PseudoOptDecorator;
43 import org.sat4j.reader.DimacsReader;
44 import org.sat4j.reader.Reader;
45 import org.sat4j.specs.ISolver;
46
47
48
49
50
51
52
53
54 public class GenericOptLauncher extends AbstractOptimizationLauncher {
55
56
57
58
59 private static final long serialVersionUID = 1L;
60
61 @SuppressWarnings("nls")
62 private Options createCLIOptions() {
63 Options options = new Options();
64 options.addOption("t", "timeout", true,
65 "specifies the timeout (in seconds)");
66 options.addOption("p", "parallel", false,
67 "uses CP and RES pseudo-boolean solvers in parallel");
68 options.addOption("T", "timeoutms", true,
69 "specifies the timeout (in milliseconds)");
70 options.addOption("k", "kind", true,
71 "kind of problem: minone, maxsat, etc.");
72 options.addOption("i", "incomplete", false,
73 "incomplete mode for maxsat");
74 options.addOption("c", "clean databases", false,
75 "clean up the database at root level");
76 options.addOption("k", "keep Hot", false,
77 "Keep heuristics accross calls to the SAT solver");
78 options.addOption("e", "equivalence", false,
79 "Use an equivalence instead of an implication for the selector variables");
80 options.addOption("n", "no solution line", false,
81 "Do not display a solution line (useful if the solution is large)");
82 options.addOption("l", "lower bounding", false,
83 "search solution by lower bounding instead of by upper bounding");
84 options.addOption("m", "mystery", false, "mystery option");
85 return options;
86 }
87
88 @Override
89 public void displayLicense() {
90 super.displayLicense();
91 log("This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details.");
92 }
93
94 @Override
95 public void usage() {
96 this.out.println("java -jar sat4j-maxsat.jar instance-name");
97 }
98
99 @Override
100 protected Reader createReader(ISolver aSolver, String problemname) {
101 Reader reader;
102 if (problemname.contains(".wcnf")) {
103 reader = new WDimacsReader(this.wmsd);
104 } else {
105 reader = new DimacsReader(this.wmsd);
106 }
107 reader.setVerbosity(true);
108 return reader;
109 }
110
111 @Override
112 protected String getInstanceName(String[] args) {
113 return args[args.length - 1];
114 }
115
116 private WeightedMaxSatDecorator wmsd;
117
118 @Override
119 protected ISolver configureSolver(String[] args) {
120 ISolver asolver = null;
121 Options options = createCLIOptions();
122 if (args.length == 0) {
123 HelpFormatter helpf = new HelpFormatter();
124 helpf.printHelp("java -jar sat4j-maxsat.jar", options, true);
125 } else {
126 try {
127 CommandLine cmd = new PosixParser().parse(options, args);
128 int problemindex = args.length - 1;
129 setDisplaySolutionLine(!cmd.hasOption("n"));
130 boolean equivalence = cmd.hasOption("e");
131 String kind = cmd.getOptionValue("k");
132 if (kind == null) {
133 kind = "maxsat";
134 }
135 if ("minone".equalsIgnoreCase(kind)) {
136 asolver = new MinOneDecorator(SolverFactory.newDefault());
137 } else if ("mincost".equalsIgnoreCase(kind)
138 || args[problemindex].endsWith(".p2cnf")) {
139 asolver = new MinCostDecorator(SolverFactory.newDefault());
140 } else {
141 assert "maxsat".equalsIgnoreCase(kind);
142 if (cmd.hasOption("m")) {
143 this.wmsd = new WeightedMaxSatDecorator(
144 org.sat4j.pb.SolverFactory.newSATUNSAT(),
145 equivalence);
146 } else if (cmd.hasOption("p")) {
147 this.wmsd = new WeightedMaxSatDecorator(
148 org.sat4j.pb.SolverFactory.newBoth(),
149 equivalence);
150 } else {
151 this.wmsd = new WeightedMaxSatDecorator(
152 SolverFactory.newDefault(), equivalence);
153 }
154 if (cmd.hasOption("l")) {
155 asolver = new ConstraintRelaxingPseudoOptDecorator(
156 this.wmsd);
157 } else {
158 asolver = new PseudoOptDecorator(this.wmsd,false,!equivalence);
159 }
160 }
161 if (cmd.hasOption("i")) {
162 setIncomplete(true);
163 }
164 if (cmd.hasOption("c")) {
165 asolver.setDBSimplificationAllowed(true);
166 }
167 if (cmd.hasOption("k")) {
168 asolver.setKeepSolverHot(true);
169 }
170 String timeout = cmd.getOptionValue("t");
171 if (timeout == null) {
172 timeout = cmd.getOptionValue("T");
173 if (timeout != null) {
174 asolver.setTimeoutMs(Long.parseLong(timeout));
175 }
176 } else {
177 asolver.setTimeout(Integer.parseInt(timeout));
178 }
179 getLogWriter().println(asolver.toString(COMMENT_PREFIX));
180 } catch (ParseException e1) {
181 HelpFormatter helpf = new HelpFormatter();
182 helpf.printHelp("java -jar sat4jopt.jar", options, true);
183 }
184 }
185 return asolver;
186 }
187
188 public static void main(String[] args) {
189 AbstractLauncher lanceur = new GenericOptLauncher();
190 lanceur.run(args);
191 }
192 }