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;
31
32 import org.sat4j.minisat.SolverFactory;
33 import org.sat4j.reader.GroupedCNFReader;
34 import org.sat4j.reader.LecteurDimacs;
35 import org.sat4j.reader.Reader;
36 import org.sat4j.specs.ISolver;
37 import org.sat4j.specs.IVecInt;
38 import org.sat4j.specs.TimeoutException;
39 import org.sat4j.tools.AllMUSes;
40 import org.sat4j.tools.SolutionFoundListener;
41 import org.sat4j.tools.xplain.Explainer;
42 import org.sat4j.tools.xplain.HighLevelXplain;
43 import org.sat4j.tools.xplain.MinimizationStrategy;
44 import org.sat4j.tools.xplain.Xplain;
45
46 public class MUSLauncher extends AbstractLauncher {
47
48
49
50
51 private static final long serialVersionUID = 1L;
52
53 private int[] mus;
54
55 private Explainer xplain;
56
57 private boolean highLevel = false;
58
59 private AllMUSes allMuses;
60
61 @Override
62 public void usage() {
63 log("java -jar sat4j-mus.jar [Insertion|Deletion|QuickXplain] <cnffile>|<gcnffile>");
64 }
65
66 @Override
67 protected Reader createReader(ISolver theSolver, String problemname) {
68 if (this.highLevel) {
69 return new GroupedCNFReader((HighLevelXplain<ISolver>) theSolver);
70 }
71 return new LecteurDimacs(theSolver);
72 }
73
74 @Override
75 protected String getInstanceName(String[] args) {
76 if (args.length == 0) {
77 return null;
78 }
79 return args[args.length - 1];
80 }
81
82 @Override
83 protected ISolver configureSolver(String[] args) {
84 String problemName = args[args.length - 1];
85 if (problemName.endsWith(".gcnf")) {
86 this.highLevel = true;
87 }
88 ISolver solver;
89 if (this.highLevel) {
90 HighLevelXplain<ISolver> hlxp = new HighLevelXplain<ISolver>(
91 SolverFactory.newDefault());
92 this.xplain = hlxp;
93 solver = hlxp;
94 } else {
95 Xplain<ISolver> xp = new Xplain<ISolver>(
96 SolverFactory.newDefault(), false);
97 this.xplain = xp;
98 solver = xp;
99 }
100 solver.setDBSimplificationAllowed(true);
101 if (args.length == 2) {
102
103 if ("all".equals(args[0])) {
104 allMuses = new AllMUSes(highLevel, SolverFactory.instance());
105 solver = allMuses.getSolverInstance();
106 } else {
107 String className = "org.sat4j.tools.xplain." + args[0]
108 + "Strategy";
109 try {
110 this.xplain
111 .setMinimizationStrategy((MinimizationStrategy) Class
112 .forName(className).newInstance());
113 } catch (Exception e) {
114 log(e.getMessage());
115 }
116 }
117 }
118 solver.setTimeout(Integer.MAX_VALUE);
119 getLogWriter().println(solver.toString(COMMENT_PREFIX));
120 return solver;
121 }
122
123 @Override
124 protected void displayResult() {
125 if (this.solver != null) {
126 double wallclocktime = (System.currentTimeMillis() - this.beginTime) / 1000.0;
127 this.solver.printStat(this.out);
128 this.solver.printInfos(this.out);
129 this.out.println(ILauncherMode.ANSWER_PREFIX + this.exitCode);
130 if (this.exitCode == ExitCode.SATISFIABLE) {
131 int[] model = this.solver.model();
132 this.out.print(ILauncherMode.SOLUTION_PREFIX);
133 this.reader.decode(model, this.out);
134 this.out.println();
135 } else if (this.exitCode == ExitCode.UNSATISFIABLE
136 && this.mus != null) {
137 this.out.print(ILauncherMode.SOLUTION_PREFIX);
138 this.reader.decode(this.mus, this.out);
139 this.out.println();
140 }
141 log("Total wall clock time (in seconds) : " + wallclocktime);
142 }
143 }
144
145 @Override
146 public void run(String[] args) {
147 this.mus = null;
148 super.run(args);
149 double wallclocktime = (System.currentTimeMillis() - this.beginTime) / 1000.0;
150 if (this.exitCode == ExitCode.UNSATISFIABLE) {
151 try {
152 log("Unsat detection wall clock time (in seconds) : "
153 + wallclocktime);
154 double beginmus = System.currentTimeMillis();
155 if (allMuses != null) {
156 SolutionFoundListener mssListener = new SolutionFoundListener() {
157 private int msscount = 0;
158
159 public void onUnsatTermination() {
160 throw new UnsupportedOperationException(
161 "Not implemented yet!");
162 }
163
164 public void onSolutionFound(IVecInt solution) {
165 System.out.print("\r" + solver.getLogPrefix()
166 + "found mss number " + ++msscount);
167 }
168
169 public void onSolutionFound(int[] solution) {
170 throw new UnsupportedOperationException(
171 "Not implemented yet!");
172 }
173 };
174 SolutionFoundListener musListener = new SolutionFoundListener() {
175 public void onSolutionFound(int[] solution) {
176 }
177
178 public void onSolutionFound(IVecInt solution) {
179 System.out.println(solver.getLogPrefix()
180 + "found mus number " + ++muscount);
181 out.print(ILauncherMode.SOLUTION_PREFIX);
182 int[] localMus = new int[solution.size()];
183 solution.copyTo(localMus);
184 reader.decode(localMus, out);
185 out.println();
186 }
187
188 public void onUnsatTermination() {
189 }
190 };
191 allMuses.computeAllMSS(mssListener);
192 if ("card".equals(System.getProperty("min"))) {
193 allMuses.computeAllMUSesOrdered(musListener);
194 } else {
195 allMuses.computeAllMUSes(musListener);
196 }
197 log("All MUSes computation wall clock time (in seconds) : "
198 + (System.currentTimeMillis() - beginmus) / 1000.0);
199 } else {
200 log("Size of initial "
201 + (this.highLevel ? "high level " : "")
202 + "unsat subformula: "
203 + this.solver.unsatExplanation().size());
204 log("Computing " + (this.highLevel ? "high level " : "")
205 + "MUS ...");
206 this.mus = this.xplain.minimalExplanation();
207 log("Size of the " + (this.highLevel ? "high level " : "")
208 + "MUS: " + this.mus.length);
209 log("Unsat core computation wall clock time (in seconds) : "
210 + (System.currentTimeMillis() - beginmus) / 1000.0);
211 }
212 } catch (TimeoutException e) {
213 log("Cannot compute " + (this.highLevel ? "high level " : "")
214 + "MUS within the timeout.");
215 }
216 }
217
218 }
219
220 private int muscount = 0;
221
222 public static void main(final String[] args) {
223 MUSLauncher lanceur = new MUSLauncher();
224 if (args.length < 1 || args.length > 2) {
225 lanceur.usage();
226 return;
227 }
228 lanceur.run(args);
229 System.exit(lanceur.getExitCode().value());
230 }
231 }