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.tools;
31
32 import java.io.PrintStream;
33 import java.io.PrintWriter;
34 import java.util.HashMap;
35 import java.util.Map;
36
37 import org.sat4j.core.LiteralsUtils;
38 import org.sat4j.core.VecInt;
39 import org.sat4j.minisat.core.Counter;
40 import org.sat4j.specs.ContradictionException;
41 import org.sat4j.specs.IConstr;
42 import org.sat4j.specs.ISolver;
43 import org.sat4j.specs.ISolverService;
44 import org.sat4j.specs.IVec;
45 import org.sat4j.specs.IVecInt;
46 import org.sat4j.specs.IteratorInt;
47 import org.sat4j.specs.SearchListener;
48 import org.sat4j.specs.TimeoutException;
49 import org.sat4j.specs.UnitClauseProvider;
50
51 public class StatisticsSolver implements ISolver {
52
53 private static final String NOT_IMPLEMENTED_YET = "Not implemented yet!";
54
55 private static final String THAT_SOLVER_ONLY_COMPUTE_STATISTICS = "That solver only compute statistics";
56
57
58
59
60 private static final long serialVersionUID = 1L;
61
62
63
64
65 private int expectedNumberOfConstraints;
66
67
68
69
70 private int nbvars;
71
72
73
74
75 private IVecInt[] sizeoccurrences;
76
77 private int allpositive;
78
79 private int allnegative;
80
81 private int horn;
82
83 private int dualhorn;
84
85
86
87
88 private final Map<Integer, Counter> sizes = new HashMap<Integer, Counter>();
89
90 public int[] model() {
91 throw new UnsupportedOperationException(
92 THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
93 }
94
95 public boolean model(int var) {
96 throw new UnsupportedOperationException(
97 THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
98 }
99
100 public int[] primeImplicant() {
101 throw new UnsupportedOperationException(
102 THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
103 }
104
105 public boolean primeImplicant(int p) {
106 throw new UnsupportedOperationException(
107 THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
108 }
109
110 public boolean isSatisfiable() throws TimeoutException {
111 throw new TimeoutException(THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
112 }
113
114 public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
115 throws TimeoutException {
116 throw new TimeoutException(THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
117 }
118
119 public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
120 throw new TimeoutException(THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
121 }
122
123 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
124 throw new TimeoutException(THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
125 }
126
127 public int[] findModel() throws TimeoutException {
128 throw new TimeoutException(THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
129 }
130
131 public int[] findModel(IVecInt assumps) throws TimeoutException {
132 throw new TimeoutException(THAT_SOLVER_ONLY_COMPUTE_STATISTICS);
133 }
134
135 public int nConstraints() {
136 return expectedNumberOfConstraints;
137 }
138
139 public int newVar(int howmany) {
140 this.nbvars = howmany;
141 sizeoccurrences = new IVecInt[(howmany + 1) << 1];
142 return howmany;
143 }
144
145 public int nVars() {
146 return this.nbvars;
147 }
148
149 @Deprecated
150 public void printInfos(PrintWriter out, String prefix) {
151
152 }
153
154 public void printInfos(PrintWriter out) {
155 }
156
157 @Deprecated
158 public int newVar() {
159 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
160 }
161
162 public int nextFreeVarId(boolean reserve) {
163 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
164 }
165
166 public void registerLiteral(int p) {
167 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
168 }
169
170 public void setExpectedNumberOfClauses(int nb) {
171 this.expectedNumberOfConstraints = nb;
172 }
173
174 public IConstr addClause(IVecInt literals) throws ContradictionException {
175 int size = literals.size();
176 Counter counter = sizes.get(size);
177 if (counter == null) {
178 counter = new Counter(0);
179 sizes.put(size, counter);
180 }
181 counter.inc();
182 IVecInt list;
183 int x, p;
184 int pos = 0, neg = 0;
185 for (IteratorInt it = literals.iterator(); it.hasNext();) {
186 x = it.next();
187 if (x > 0) {
188 pos++;
189 } else {
190 neg++;
191 }
192 p = LiteralsUtils.toInternal(x);
193 list = sizeoccurrences[p];
194 if (list == null) {
195 list = new VecInt();
196 sizeoccurrences[p] = list;
197 }
198 list.push(size);
199 }
200 if (neg == 0) {
201 allpositive++;
202 } else if (pos == 0) {
203 allnegative++;
204 } else if (pos == 1) {
205 horn++;
206 } else if (neg == 1) {
207 dualhorn++;
208 }
209 return null;
210 }
211
212 public IConstr addBlockingClause(IVecInt literals)
213 throws ContradictionException {
214 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
215 }
216
217 public boolean removeConstr(IConstr c) {
218 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
219 }
220
221 public boolean removeSubsumedConstr(IConstr c) {
222 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
223 }
224
225 public void addAllClauses(IVec<IVecInt> clauses)
226 throws ContradictionException {
227 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
228 }
229
230 public IConstr addAtMost(IVecInt literals, int degree)
231 throws ContradictionException {
232 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
233 }
234
235 public IConstr addAtLeast(IVecInt literals, int degree)
236 throws ContradictionException {
237 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
238 }
239
240 public IConstr addExactly(IVecInt literals, int n)
241 throws ContradictionException {
242 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
243 }
244
245 public void setTimeout(int t) {
246 }
247
248 public void setTimeoutOnConflicts(int count) {
249 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
250 }
251
252 public void setTimeoutMs(long t) {
253 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
254 }
255
256 public int getTimeout() {
257 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
258 }
259
260 public long getTimeoutMs() {
261 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
262 }
263
264 public void expireTimeout() {
265 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
266 }
267
268 public void reset() {
269 }
270
271 @Deprecated
272 public void printStat(PrintStream out, String prefix) {
273 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
274 }
275
276 @Deprecated
277 public void printStat(PrintWriter out, String prefix) {
278 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
279 }
280
281 public void printStat(PrintWriter out) {
282 int realNumberOfVariables = 0;
283 int realNumberOfLiterals = 0;
284 int pureLiterals = 0;
285 int minOccV = Integer.MAX_VALUE;
286 int maxOccV = Integer.MIN_VALUE;
287 int sumV = 0;
288 int sizeL, sizeV;
289 int minOccL = Integer.MAX_VALUE;
290 int maxOccL = Integer.MIN_VALUE;
291 int sumL = 0;
292 IVecInt list;
293 boolean oneNull;
294 if (sizeoccurrences == null) {
295 return;
296 }
297 int max = sizeoccurrences.length - 1;
298 for (int i = 1; i < max; i += 2) {
299 sizeV = 0;
300 oneNull = false;
301 for (int k = 0; k < 2; k++) {
302 list = sizeoccurrences[i + k];
303 if (list == null) {
304 oneNull = true;
305 } else {
306 realNumberOfLiterals++;
307 sizeL = list.size();
308 sizeV += sizeL;
309 if (minOccL > sizeL) {
310 minOccL = sizeL;
311 }
312 if (sizeL > maxOccL) {
313 maxOccL = sizeL;
314 }
315 sumL += sizeL;
316 }
317 }
318
319 if (sizeV > 0) {
320 if (oneNull) {
321 pureLiterals++;
322 }
323 realNumberOfVariables++;
324 if (minOccV > sizeV) {
325 minOccV = sizeV;
326 }
327 if (sizeV > maxOccV) {
328 maxOccV = sizeV;
329 }
330 sumV += sizeV;
331 }
332
333 }
334 System.out.println("c Distribution of constraints size:");
335 int nbclauses = 0;
336 for (Map.Entry<Integer, Counter> entry : sizes.entrySet()) {
337 System.out.printf("c %d => %d%n", entry.getKey(), entry.getValue()
338 .getValue());
339 nbclauses += entry.getValue().getValue();
340 }
341
342 System.out
343 .printf("c Real number of variables, literals, number of clauses, #pureliterals, ");
344 System.out.printf("variable occurrences (min/max/avg) ");
345 System.out.printf("literals occurrences (min/max/avg) ");
346 System.out
347 .println("Specific clauses: #positive #negative #horn #dualhorn #remaining");
348
349 System.out.printf("%d %d %d %d %d %d %d %d %d %d ",
350 realNumberOfVariables, realNumberOfLiterals, nbclauses,
351 pureLiterals, minOccV, maxOccV, sumV / realNumberOfVariables,
352 minOccL, maxOccL, sumL / realNumberOfLiterals);
353 System.out.printf("%d %d %d %d %d%n", allpositive, allnegative, horn,
354 dualhorn, nbclauses - allpositive - allnegative - horn
355 - dualhorn);
356 }
357
358 public Map<String, Number> getStat() {
359 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
360 }
361
362 public String toString(String prefix) {
363 return prefix + "Statistics about the benchmarks";
364 }
365
366 public void clearLearntClauses() {
367 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
368 }
369
370 public void setDBSimplificationAllowed(boolean status) {
371 }
372
373 public boolean isDBSimplificationAllowed() {
374 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
375 }
376
377 public <S extends ISolverService> void setSearchListener(
378 SearchListener<S> sl) {
379 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
380 }
381
382 public <S extends ISolverService> SearchListener<S> getSearchListener() {
383 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
384 }
385
386 public boolean isVerbose() {
387 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
388 }
389
390 public void setVerbose(boolean value) {
391 }
392
393 public void setLogPrefix(String prefix) {
394 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
395 }
396
397 public String getLogPrefix() {
398 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
399 }
400
401 public IVecInt unsatExplanation() {
402 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
403 }
404
405 public int[] modelWithInternalVariables() {
406 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
407 }
408
409 public int realNumberOfVariables() {
410 return nbvars;
411 }
412
413 public boolean isSolverKeptHot() {
414 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
415 }
416
417 public void setKeepSolverHot(boolean keepHot) {
418 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
419 }
420
421 public ISolver getSolvingEngine() {
422 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
423 }
424
425 public void setUnitClauseProvider(UnitClauseProvider ucp) {
426 throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
427 }
428 }