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 package org.sat4j.tools;
29
30 import java.io.PrintStream;
31 import java.io.PrintWriter;
32 import java.util.ArrayList;
33 import java.util.List;
34 import java.util.Map;
35
36 import org.sat4j.core.ASolverFactory;
37 import org.sat4j.core.ConstrGroup;
38 import org.sat4j.core.VecInt;
39 import org.sat4j.specs.ContradictionException;
40 import org.sat4j.specs.IConstr;
41 import org.sat4j.specs.ISolver;
42 import org.sat4j.specs.IVec;
43 import org.sat4j.specs.IVecInt;
44 import org.sat4j.specs.SearchListener;
45 import org.sat4j.specs.TimeoutException;
46
47 public class ManyCore<S extends ISolver> implements ISolver, OutcomeListener {
48
49 private static final long MINIMAL_MEMORY_REQUIREMENT = 500000000L;
50
51 private static final int NORMAL_SLEEP = 500;
52
53 private static final int FAST_SLEEP = 50;
54
55
56
57
58 private static final long serialVersionUID = 1L;
59
60 private final String[] availableSolvers;
61
62 protected final List<S> solvers;
63 protected final int numberOfSolvers;
64 private int winnerId;
65 private boolean resultFound;
66 private volatile int remainingSolvers;
67 private volatile int sleepTime;
68 private volatile boolean solved;
69
70 public ManyCore(ASolverFactory<S> factory, String... solverNames) {
71 availableSolvers = solverNames;
72 numberOfSolvers = computeNumberOfSolversInParallel(solverNames.length);
73 solvers = new ArrayList<S>(numberOfSolvers);
74 for (int i = 0; i < numberOfSolvers; i++) {
75 solvers.add(factory.createSolverByName(availableSolvers[i]));
76 }
77 }
78
79 private int computeNumberOfSolversInParallel(int upperBound) {
80 Runtime runtime = Runtime.getRuntime();
81 long memory = runtime.maxMemory();
82 int numberOfCores = runtime.availableProcessors();
83 if (memory > MINIMAL_MEMORY_REQUIREMENT) {
84 return upperBound < numberOfCores ? upperBound : numberOfCores;
85 } else {
86 return 1;
87 }
88 }
89
90
91
92
93
94
95
96
97
98 public ManyCore(String[] names, S... solverObjects) {
99 this(solverObjects);
100 for (int i = 0; i < names.length; i++) {
101 availableSolvers[i] = names[i];
102 }
103 }
104
105 public ManyCore(S... solverObjects) {
106 availableSolvers = new String[solverObjects.length];
107 for (int i = 0; i < solverObjects.length; i++) {
108 availableSolvers[i] = "solver" + i;
109 }
110 numberOfSolvers = computeNumberOfSolversInParallel(solverObjects.length);
111 solvers = new ArrayList<S>(numberOfSolvers);
112 for (int i = 0; i < numberOfSolvers; i++) {
113 solvers.add(solverObjects[i]);
114 }
115 }
116
117 public void addAllClauses(IVec<IVecInt> clauses)
118 throws ContradictionException {
119 for (int i = 0; i < numberOfSolvers; i++) {
120 solvers.get(i).addAllClauses(clauses);
121 }
122 }
123
124 public IConstr addAtLeast(IVecInt literals, int degree)
125 throws ContradictionException {
126 ConstrGroup group = new ConstrGroup(false);
127 for (int i = 0; i < numberOfSolvers; i++) {
128 group.add(solvers.get(i).addAtLeast(literals, degree));
129 }
130 return group;
131 }
132
133 public IConstr addAtMost(IVecInt literals, int degree)
134 throws ContradictionException {
135 ConstrGroup group = new ConstrGroup(false);
136 for (int i = 0; i < numberOfSolvers; i++) {
137 group.add(solvers.get(i).addAtMost(literals, degree));
138 }
139 return group;
140 }
141
142 public IConstr addExactly(IVecInt literals, int n)
143 throws ContradictionException {
144 ConstrGroup group = new ConstrGroup(false);
145 for (int i = 0; i < numberOfSolvers; i++) {
146 group.add(solvers.get(i).addExactly(literals, n));
147 }
148 return group;
149 }
150
151 public IConstr addClause(IVecInt literals) throws ContradictionException {
152 ConstrGroup group = new ConstrGroup(false);
153 for (int i = 0; i < numberOfSolvers; i++) {
154 group.add(solvers.get(i).addClause(literals));
155 }
156 return group;
157 }
158
159 public void clearLearntClauses() {
160 for (int i = 0; i < numberOfSolvers; i++) {
161 solvers.get(i).clearLearntClauses();
162 }
163 }
164
165 public void expireTimeout() {
166 for (int i = 0; i < numberOfSolvers; i++) {
167 solvers.get(i).expireTimeout();
168 }
169 sleepTime = FAST_SLEEP;
170 }
171
172 public Map<String, Number> getStat() {
173 return solvers.get(winnerId).getStat();
174 }
175
176 public int getTimeout() {
177 return solvers.get(0).getTimeout();
178 }
179
180 public long getTimeoutMs() {
181 return solvers.get(0).getTimeoutMs();
182 }
183
184 public int newVar() {
185 throw new UnsupportedOperationException();
186 }
187
188 public int newVar(int howmany) {
189 int result = 0;
190 for (int i = 0; i < numberOfSolvers; i++) {
191 result = solvers.get(i).newVar(howmany);
192 }
193 return result;
194 }
195
196 @Deprecated
197 public void printStat(PrintStream out, String prefix) {
198 solvers.get(winnerId).printStat(out, prefix);
199 }
200
201 public void printStat(PrintWriter out, String prefix) {
202 solvers.get(winnerId).printStat(out, prefix);
203 }
204
205 public boolean removeConstr(IConstr c) {
206 if (c instanceof ConstrGroup) {
207 ConstrGroup group = (ConstrGroup) c;
208 boolean removed = true;
209 IConstr toRemove;
210 for (int i = 0; i < numberOfSolvers; i++) {
211 toRemove = group.getConstr(i);
212 if (toRemove != null) {
213 removed = removed & solvers.get(i).removeConstr(toRemove);
214 }
215 }
216 return removed;
217 }
218 throw new IllegalArgumentException(
219 "Can only remove a group of constraints!");
220 }
221
222 public void reset() {
223 for (int i = 0; i < numberOfSolvers; i++) {
224 solvers.get(i).reset();
225 }
226 }
227
228 public void setExpectedNumberOfClauses(int nb) {
229 for (int i = 0; i < numberOfSolvers; i++) {
230 solvers.get(i).setExpectedNumberOfClauses(nb);
231 }
232 }
233
234 public void setTimeout(int t) {
235 for (int i = 0; i < numberOfSolvers; i++) {
236 solvers.get(i).setTimeout(t);
237 }
238 }
239
240 public void setTimeoutMs(long t) {
241 for (int i = 0; i < numberOfSolvers; i++) {
242 solvers.get(i).setTimeoutMs(t);
243 }
244 }
245
246 public void setTimeoutOnConflicts(int count) {
247 for (int i = 0; i < numberOfSolvers; i++) {
248 solvers.get(i).setTimeoutOnConflicts(count);
249 }
250 }
251
252 public String toString(String prefix) {
253 StringBuffer res = new StringBuffer();
254 res.append(prefix);
255 res.append("ManyCore solver with ");
256 res.append(numberOfSolvers);
257 res.append(" solvers running in parallel");
258 res.append("\n");
259 for (int i = 0; i < numberOfSolvers; i++) {
260 res.append(solvers.get(i).toString(prefix));
261 if (i < numberOfSolvers - 1) {
262 res.append("\n");
263 }
264 }
265 return res.toString();
266 }
267
268 public int[] findModel() throws TimeoutException {
269 if (isSatisfiable()) {
270 return model();
271 }
272
273 return null;
274 }
275
276 public int[] findModel(IVecInt assumps) throws TimeoutException {
277 if (isSatisfiable(assumps)) {
278 return model();
279 }
280
281 return null;
282 }
283
284 public boolean isSatisfiable() throws TimeoutException {
285 return isSatisfiable(VecInt.EMPTY, false);
286 }
287
288 public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
289 throws TimeoutException {
290 remainingSolvers = numberOfSolvers;
291 solved = false;
292 for (int i = 0; i < numberOfSolvers; i++) {
293 new Thread(new RunnableSolver(i, solvers.get(i), assumps,
294 globalTimeout, this)).start();
295 }
296 try {
297 sleepTime = NORMAL_SLEEP;
298 do {
299 Thread.sleep(sleepTime);
300 } while (remainingSolvers > 0);
301 } catch (InterruptedException e) {
302
303 }
304 if (!solved) {
305 assert remainingSolvers == 0;
306 throw new TimeoutException();
307 }
308 return resultFound;
309 }
310
311 public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
312 throw new UnsupportedOperationException();
313 }
314
315 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
316 throw new UnsupportedOperationException();
317 }
318
319 public int[] model() {
320 return solvers.get(winnerId).model();
321 }
322
323 public boolean model(int var) {
324 return solvers.get(winnerId).model(var);
325 }
326
327 public int nConstraints() {
328 return solvers.get(0).nConstraints();
329 }
330
331 public int nVars() {
332 return solvers.get(0).nVars();
333 }
334
335 public void printInfos(PrintWriter out, String prefix) {
336 for (int i = 0; i < numberOfSolvers; i++) {
337 solvers.get(i).printInfos(out, prefix);
338 }
339 }
340
341 public synchronized void onFinishWithAnswer(boolean finished,
342 boolean result, int index) {
343 if (finished && !solved) {
344 winnerId = index;
345 solved = true;
346 resultFound = result;
347 for (int i = 0; i < numberOfSolvers; i++) {
348 if (i != winnerId)
349 solvers.get(i).expireTimeout();
350 }
351 sleepTime = FAST_SLEEP;
352 System.out.println(getLogPrefix() + " And the winner is "
353 + availableSolvers[winnerId]);
354 }
355 remainingSolvers--;
356 }
357
358 public boolean isDBSimplificationAllowed() {
359 return solvers.get(0).isDBSimplificationAllowed();
360 }
361
362 public void setDBSimplificationAllowed(boolean status) {
363 for (int i = 0; i < numberOfSolvers; i++) {
364 solvers.get(0).setDBSimplificationAllowed(status);
365 }
366 }
367
368 public void setSearchListener(SearchListener sl) {
369 for (int i = 0; i < numberOfSolvers; i++) {
370 solvers.get(i).setSearchListener(sl);
371 }
372 }
373
374
375
376
377 public SearchListener getSearchListener() {
378 return solvers.get(0).getSearchListener();
379 }
380
381 public int nextFreeVarId(boolean reserve) {
382 return solvers.get(0).nextFreeVarId(reserve);
383 }
384
385 public IConstr addBlockingClause(IVecInt literals)
386 throws ContradictionException {
387 ConstrGroup group = new ConstrGroup(false);
388 for (int i = 0; i < numberOfSolvers; i++) {
389 group.add(solvers.get(i).addBlockingClause(literals));
390 }
391 return group;
392 }
393
394 public boolean removeSubsumedConstr(IConstr c) {
395 if (c instanceof ConstrGroup) {
396 ConstrGroup group = (ConstrGroup) c;
397 boolean removed = true;
398 IConstr toRemove;
399 for (int i = 0; i < numberOfSolvers; i++) {
400 toRemove = group.getConstr(i);
401 if (toRemove != null) {
402 removed = removed
403 & solvers.get(i).removeSubsumedConstr(toRemove);
404 }
405 }
406 return removed;
407 }
408 throw new IllegalArgumentException(
409 "Can only remove a group of constraints!");
410 }
411
412 public boolean isVerbose() {
413 return solvers.get(0).isVerbose();
414 }
415
416 public void setVerbose(boolean value) {
417 for (int i = 0; i < numberOfSolvers; i++) {
418 solvers.get(i).setVerbose(value);
419 }
420 }
421
422 public void setLogPrefix(String prefix) {
423 for (int i = 0; i < numberOfSolvers; i++) {
424 solvers.get(i).setLogPrefix(prefix);
425 }
426
427 }
428
429 public String getLogPrefix() {
430 return solvers.get(0).getLogPrefix();
431 }
432
433 public IVecInt unsatExplanation() {
434 return solvers.get(winnerId).unsatExplanation();
435 }
436
437 public int[] primeImplicant() {
438 return solvers.get(winnerId).primeImplicant();
439 }
440
441 public List<S> getSolvers() {
442 return new ArrayList<S>(this.solvers);
443 }
444
445 public int[] modelWithInternalVariables() {
446 return solvers.get(winnerId).modelWithInternalVariables();
447 }
448
449 public int realNumberOfVariables() {
450 return solvers.get(0).realNumberOfVariables();
451 }
452
453 public void registerLiteral(int p) {
454 for (int i = 0; i < numberOfSolvers; i++) {
455 solvers.get(i).registerLiteral(p);
456 }
457
458 }
459 }
460
461 interface OutcomeListener {
462 void onFinishWithAnswer(boolean finished, boolean result, int index);
463 }
464
465 class RunnableSolver implements Runnable {
466
467 private final int index;
468 private final ISolver solver;
469 private final OutcomeListener ol;
470 private final IVecInt assumps;
471 private final boolean globalTimeout;
472
473 public RunnableSolver(int i, ISolver solver, IVecInt assumps,
474 boolean globalTimeout, OutcomeListener ol) {
475 index = i;
476 this.solver = solver;
477 this.ol = ol;
478 this.assumps = assumps;
479 this.globalTimeout = globalTimeout;
480 }
481
482 public void run() {
483 try {
484 boolean result = solver.isSatisfiable(assumps, globalTimeout);
485 ol.onFinishWithAnswer(true, result, index);
486 } catch (Exception e) {
487 ol.onFinishWithAnswer(false, false, index);
488 }
489 }
490
491 }