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