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 import java.io.FileNotFoundException;
33 import java.io.IOException;
34
35 import org.apache.commons.beanutils.BeanUtils;
36 import org.apache.commons.cli.CommandLine;
37 import org.apache.commons.cli.HelpFormatter;
38 import org.apache.commons.cli.Options;
39 import org.apache.commons.cli.ParseException;
40 import org.apache.commons.cli.PosixParser;
41 import org.sat4j.AbstractLauncher;
42 import org.sat4j.ExitCode;
43 import org.sat4j.ILauncherMode;
44 import org.sat4j.maxsat.WeightedMaxSatDecorator;
45 import org.sat4j.maxsat.reader.MSInstanceReader;
46 import org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator;
47 import org.sat4j.pb.IPBSolver;
48 import org.sat4j.pb.PseudoOptDecorator;
49 import org.sat4j.pb.core.IPBCDCLSolver;
50 import org.sat4j.pb.reader.PBInstanceReader;
51 import org.sat4j.reader.InstanceReader;
52 import org.sat4j.reader.ParseFormatException;
53 import org.sat4j.reader.Reader;
54 import org.sat4j.specs.ContradictionException;
55 import org.sat4j.specs.ILogAble;
56 import org.sat4j.specs.ISolver;
57 import org.sat4j.specs.TimeoutException;
58 import org.sat4j.tools.ConflictDepthTracing;
59 import org.sat4j.tools.ConflictLevelTracing;
60 import org.sat4j.tools.DecisionTracing;
61 import org.sat4j.tools.FileBasedVisualizationTool;
62 import org.sat4j.tools.LearnedClausesSizeTracing;
63 import org.sat4j.tools.MultiTracing;
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83 public class Launcher extends AbstractLauncher implements ILogAble {
84
85
86
87
88 private static final long serialVersionUID = 1L;
89
90 private boolean isModeOptimization = false;
91
92 private boolean modeTracing = false;
93
94 private boolean launchRemoteControl;
95
96 private static AbstractLauncher launcher;
97
98 public static void main(final String[] args) {
99 launcher = new Launcher();
100 launcher.run(args);
101
102 }
103
104 private String filename;
105
106 private ProblemType typeProbleme = ProblemType.CNF_SAT;
107
108 @Override
109 public void usage() {
110 Solvers.usage(this);
111 }
112
113 @Override
114 protected Reader createReader(ISolver theSolver, String problemname) {
115 InstanceReader instance = new InstanceReader(theSolver);
116 switch (typeProbleme) {
117 case CNF_MAXSAT:
118 case WCNF_MAXSAT:
119 instance = new MSInstanceReader((WeightedMaxSatDecorator) theSolver);
120 break;
121 case PB_OPT:
122 case PB_SAT:
123 instance = new PBInstanceReader((IPBSolver) theSolver);
124 break;
125 case CNF_SAT:
126 instance = new InstanceReader(theSolver);
127 break;
128 }
129
130 return instance;
131 }
132
133 @Override
134 protected String getInstanceName(String[] args) {
135 return this.filename;
136 }
137
138
139
140
141
142
143
144
145 @SuppressWarnings({ "nls", "unchecked" })
146 @Override
147 protected ISolver configureSolver(String[] args) {
148 Options options = Solvers.createCLIOptions();
149
150 try {
151 CommandLine cmd = new PosixParser().parse(options, args);
152
153 this.isModeOptimization = cmd.hasOption("opt");
154
155 this.filename = cmd.getOptionValue("f");
156
157 boolean equivalence = cmd.hasOption("e");
158
159 int others = 0;
160 String[] rargs = cmd.getArgs();
161 if (this.filename == null && rargs.length > 0) {
162 this.filename = rargs[others++];
163 }
164
165 if (filename != null) {
166 String unzipped = Solvers.uncompressed(filename);
167
168 if (unzipped.endsWith(".cnf") && isModeOptimization) {
169 typeProbleme = ProblemType.CNF_MAXSAT;
170 } else if (unzipped.endsWith(".wcnf")) {
171 typeProbleme = ProblemType.WCNF_MAXSAT;
172 isModeOptimization = true;
173 } else if (unzipped.endsWith(".opb")) {
174 if (isModeOptimization) {
175 typeProbleme = ProblemType.PB_OPT;
176 } else {
177 typeProbleme = ProblemType.PB_SAT;
178 }
179 } else {
180 typeProbleme = ProblemType.CNF_SAT;
181 }
182 } else {
183 typeProbleme = ProblemType.CNF_SAT;
184 }
185
186 ISolver asolver = Solvers.configureSolver(args, this);
187
188 this.launchRemoteControl = cmd.hasOption("remote");
189
190 if (cmd.hasOption("m")) {
191 setSilent(true);
192 }
193
194 if (cmd.hasOption("k")) {
195 Integer myk = Integer.valueOf(cmd.getOptionValue("k"));
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 switch (typeProbleme) {
247 case PB_OPT:
248 setLauncherMode(ILauncherMode.OPTIMIZATION);
249 if (cmd.hasOption("lo")) {
250 this.problem = new ConstraintRelaxingPseudoOptDecorator(
251 (IPBSolver) asolver);
252 } else {
253 this.problem = new PseudoOptDecorator((IPBSolver) asolver);
254 }
255 break;
256 case CNF_MAXSAT:
257 case WCNF_MAXSAT:
258 setLauncherMode(ILauncherMode.OPTIMIZATION);
259 asolver = new WeightedMaxSatDecorator((IPBCDCLSolver) asolver,
260 equivalence);
261 if (cmd.hasOption("lo")) {
262 this.problem = new ConstraintRelaxingPseudoOptDecorator(
263 (WeightedMaxSatDecorator) asolver);
264 } else {
265 this.problem = new PseudoOptDecorator(
266 (WeightedMaxSatDecorator) asolver, false,
267 false);
268 }
269 break;
270 default:
271 setLauncherMode(ILauncherMode.DECISION);
272 break;
273 }
274
275 setIncomplete(cmd.hasOption("i"));
276
277 setDisplaySolutionLine(!cmd.hasOption("n"));
278
279
280 while (others < rargs.length) {
281 String[] param = rargs[others].split("=");
282 assert param.length == 2;
283 log("setting " + param[0] + " to " + param[1]);
284 try {
285 BeanUtils.setProperty(asolver, param[0], param[1]);
286 } catch (Exception e) {
287 log("Cannot set parameter : "
288 + args[others]);
289 }
290 others++;
291 }
292
293 if (asolver != null) {
294 getLogWriter().println(asolver.toString(COMMENT_PREFIX));
295 }
296 return asolver;
297 } catch (ParseException e1) {
298 HelpFormatter helpf = new HelpFormatter();
299 helpf.printHelp("java -jar sat4j.jar", options, true);
300 usage();
301 System.exit(0);
302 }
303 return null;
304 }
305
306 @Override
307 public void run(String[] args) {
308 try {
309 displayHeader();
310 this.solver = configureSolver(args);
311 if (this.solver == null) {
312 usage();
313 System.exit(0);
314 }
315 if (!this.silent) {
316 this.solver.setVerbose(true);
317 }
318 String instanceName = getInstanceName(args);
319 if (instanceName == null) {
320 usage();
321 System.exit(0);
322 }
323 this.beginTime = System.currentTimeMillis();
324 if (!this.launchRemoteControl) {
325 readProblem(instanceName);
326 try {
327 if (this.problem != null) {
328 solve(this.problem);
329 } else {
330 solve(this.solver);
331 }
332 } catch (TimeoutException e) {
333 log("timeout");
334 }
335 System.exit(launcher.getExitCode().value());
336 } else {
337 RemoteControlFrame frame = new RemoteControlFrame(
338 this.filename, "", args);
339 frame.activateTracing(this.modeTracing);
340 frame.setOptimisationMode(this.isModeOptimization);
341 }
342 } catch (FileNotFoundException e) {
343 System.err.println("FATAL " + e.getLocalizedMessage());
344 } catch (IOException e) {
345 System.err.println("FATAL " + e.getLocalizedMessage());
346 } catch (ContradictionException e) {
347 this.exitCode = ExitCode.UNSATISFIABLE;
348 log("(trivial inconsistency)");
349 } catch (ParseFormatException e) {
350 System.err.println("FATAL " + e.getLocalizedMessage());
351 }
352 }
353
354 }