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.TimeoutException;
38 import org.sat4j.tools.xplain.Explainer;
39 import org.sat4j.tools.xplain.HighLevelXplain;
40 import org.sat4j.tools.xplain.MinimizationStrategy;
41 import org.sat4j.tools.xplain.Xplain;
42
43 public class MUSLauncher extends AbstractLauncher {
44
45
46
47
48 private static final long serialVersionUID = 1L;
49
50 private int[] mus;
51
52 private Explainer xplain;
53
54 private boolean highLevel = false;
55
56 @Override
57 public void usage() {
58 log("java -jar sat4j-mus.jar [Insertion|Deletion|QuickXplain] <cnffile>|<gcnffile>");
59 }
60
61 @Override
62 protected Reader createReader(ISolver theSolver, String problemname) {
63 if (this.highLevel) {
64 return new GroupedCNFReader((HighLevelXplain<ISolver>) theSolver);
65 }
66 return new LecteurDimacs(theSolver);
67 }
68
69 @Override
70 protected String getInstanceName(String[] args) {
71 if (args.length == 0) {
72 return null;
73 }
74 return args[args.length - 1];
75 }
76
77 @Override
78 protected ISolver configureSolver(String[] args) {
79 String problemName = args[args.length - 1];
80 if (problemName.endsWith(".gcnf")) {
81 this.highLevel = true;
82 }
83 ISolver solver;
84 if (this.highLevel) {
85 HighLevelXplain<ISolver> hlxp = new HighLevelXplain<ISolver>(
86 SolverFactory.newDefault());
87 this.xplain = hlxp;
88 solver = hlxp;
89 } else {
90 Xplain<ISolver> xp = new Xplain<ISolver>(
91 SolverFactory.newDefault(), false);
92 this.xplain = xp;
93 solver = xp;
94 }
95 if (args.length == 2) {
96
97 String className = "org.sat4j.tools.xplain." + args[0] + "Strategy";
98 try {
99 this.xplain
100 .setMinimizationStrategy((MinimizationStrategy) Class
101 .forName(className).newInstance());
102 } catch (Exception e) {
103 log(e.getMessage());
104 }
105 }
106 solver.setTimeout(Integer.MAX_VALUE);
107 solver.setDBSimplificationAllowed(true);
108 getLogWriter().println(solver.toString(COMMENT_PREFIX));
109 return solver;
110 }
111
112 @Override
113 protected void displayResult() {
114 if (this.solver != null) {
115 double wallclocktime = (System.currentTimeMillis() - this.beginTime) / 1000.0;
116 this.solver.printStat(this.out, COMMENT_PREFIX);
117 this.solver.printInfos(this.out, COMMENT_PREFIX);
118 this.out.println(ANSWER_PREFIX + this.exitCode);
119 if (this.exitCode == ExitCode.SATISFIABLE) {
120 int[] model = this.solver.model();
121 this.out.print(SOLUTION_PREFIX);
122 this.reader.decode(model, this.out);
123 this.out.println();
124 } else if (this.exitCode == ExitCode.UNSATISFIABLE
125 && this.mus != null) {
126 this.out.print(SOLUTION_PREFIX);
127 this.reader.decode(this.mus, this.out);
128 this.out.println();
129 }
130 log("Total wall clock time (in seconds) : " + wallclocktime);
131 }
132 }
133
134 @Override
135 public void run(String[] args) {
136 this.mus = null;
137 super.run(args);
138 double wallclocktime = (System.currentTimeMillis() - this.beginTime) / 1000.0;
139 if (this.exitCode == ExitCode.UNSATISFIABLE) {
140 try {
141 log("Unsat detection wall clock time (in seconds) : "
142 + wallclocktime);
143 log("Size of initial " + (this.highLevel ? "high level " : "")
144 + "unsat subformula: "
145 + this.solver.unsatExplanation().size());
146 log("Computing " + (this.highLevel ? "high level " : "")
147 + "MUS ...");
148 double beginmus = System.currentTimeMillis();
149 this.mus = this.xplain.minimalExplanation();
150 log("Size of the " + (this.highLevel ? "high level " : "")
151 + "MUS: " + this.mus.length);
152 log("Unsat core computation wall clock time (in seconds) : "
153 + (System.currentTimeMillis() - beginmus) / 1000.0);
154 } catch (TimeoutException e) {
155 log("Cannot compute " + (this.highLevel ? "high level " : "")
156 + "MUS within the timeout.");
157 }
158 }
159
160 }
161
162 public static void main(final String[] args) {
163 MUSLauncher lanceur = new MUSLauncher();
164 if (args.length < 1 || args.length > 2) {
165 lanceur.usage();
166 return;
167 }
168 lanceur.run(args);
169 System.exit(lanceur.getExitCode().value());
170 }
171 }