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