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.pb.constraints.pb;
29
30 import java.io.Serializable;
31 import java.math.BigInteger;
32
33 import org.sat4j.core.VecInt;
34 import org.sat4j.minisat.constraints.cnf.Lits;
35 import org.sat4j.minisat.core.ILits;
36 import org.sat4j.minisat.core.Undoable;
37 import org.sat4j.minisat.core.UnitPropagationListener;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.IVecInt;
40
41 public abstract class WatchPb implements PBConstr, Undoable, Serializable {
42
43
44
45
46 private static final long serialVersionUID = 1L;
47
48
49
50
51 public static final boolean ATMOST = false;
52
53
54
55
56 public static final boolean ATLEAST = true;
57
58
59
60
61 protected double activity;
62
63
64
65
66 protected BigInteger[] coefs;
67
68
69
70
71 protected BigInteger degree;
72
73
74
75
76 protected int[] lits;
77
78
79
80
81 protected boolean learnt = false;
82
83
84
85
86 protected BigInteger watchCumul = BigInteger.ZERO;
87
88
89
90
91 protected ILits voc;
92
93
94
95
96 WatchPb() {
97 }
98
99 WatchPb(IDataStructurePB mpb) {
100 int size = mpb.size();
101 lits = new int[size];
102 this.coefs = new BigInteger[size];
103 mpb.buildConstraintFromMapPb(lits, coefs);
104
105 this.degree = mpb.getDegree();
106
107
108 sort();
109 }
110
111 WatchPb(int[] lits, BigInteger[] coefs, BigInteger degree) {
112 this.lits = lits;
113 this.coefs = coefs;
114 this.degree = degree;
115
116 sort();
117 }
118
119
120
121
122
123
124
125
126 public boolean isAssertive(int dl) {
127 BigInteger slack = BigInteger.ZERO;
128 for (int i = 0; i < lits.length; i++) {
129 if ((coefs[i].signum() > 0)
130 && ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
131 slack = slack.add(coefs[i]);
132 }
133 slack = slack.subtract(degree);
134 if (slack.signum() < 0)
135 return false;
136 for (int i = 0; i < lits.length; i++) {
137 if ((coefs[i].signum() > 0)
138 && (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
139 && (slack.compareTo(coefs[i]) < 0)) {
140 return true;
141 }
142 }
143 return false;
144 }
145
146
147
148
149
150
151
152
153
154
155
156 public void calcReason(int p, IVecInt outReason) {
157 for (int q : lits) {
158 if (voc.isFalsified(q)) {
159 outReason.push(q ^ 1);
160 }
161 }
162 }
163
164 abstract protected void computeWatches() throws ContradictionException;
165
166 abstract protected void computePropagation(UnitPropagationListener s)
167 throws ContradictionException;
168
169
170
171
172
173
174
175
176 public int get(int i) {
177 return lits[i];
178 }
179
180
181
182
183
184
185
186
187 public BigInteger getCoef(int i) {
188 return coefs[i];
189 }
190
191
192
193
194
195
196
197 public double getActivity() {
198 return activity;
199 }
200
201
202
203
204
205
206 public void incActivity(double claInc) {
207 if (learnt) {
208 activity += claInc;
209 }
210 }
211
212
213
214
215
216
217
218 public BigInteger slackConstraint() {
219 return recalcLeftSide().subtract(this.degree);
220 }
221
222
223
224
225
226
227
228
229
230
231
232 public BigInteger slackConstraint(BigInteger[] theCoefs,
233 BigInteger theDegree) {
234 return recalcLeftSide(theCoefs).subtract(theDegree);
235 }
236
237
238
239
240
241
242
243
244
245 public BigInteger recalcLeftSide(BigInteger[] theCoefs) {
246 BigInteger poss = BigInteger.ZERO;
247
248 for (int i = 0; i < lits.length; i++)
249 if (!voc.isFalsified(lits[i])) {
250 assert theCoefs[i].signum() >= 0;
251 poss = poss.add(theCoefs[i]);
252 }
253 return poss;
254 }
255
256
257
258
259
260
261
262 public BigInteger recalcLeftSide() {
263 return recalcLeftSide(this.coefs);
264 }
265
266
267
268
269
270
271 protected boolean isSatisfiable() {
272 return recalcLeftSide().compareTo(degree) >= 0;
273 }
274
275
276
277
278
279
280
281 public boolean learnt() {
282 return learnt;
283 }
284
285
286
287
288
289
290 public boolean locked() {
291 for (int p : lits) {
292 if (voc.getReason(p) == this) {
293 return true;
294 }
295 }
296 return false;
297 }
298
299
300
301
302
303
304
305
306
307
308 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
309 return a.divide(a.gcd(b)).multiply(b);
310 }
311
312
313
314
315
316
317
318 public void rescaleBy(double d) {
319 activity *= d;
320 }
321
322 void selectionSort(int from, int to) {
323 int i, j, best_i;
324 BigInteger tmp;
325 int tmp2;
326
327 for (i = from; i < to - 1; i++) {
328 best_i = i;
329 for (j = i + 1; j < to; j++) {
330 if ((coefs[j].compareTo(coefs[best_i]) > 0)
331 || ((coefs[j].equals(coefs[best_i])) && (lits[j] > lits[best_i])))
332 best_i = j;
333 }
334 tmp = coefs[i];
335 coefs[i] = coefs[best_i];
336 coefs[best_i] = tmp;
337 tmp2 = lits[i];
338 lits[i] = lits[best_i];
339 lits[best_i] = tmp2;
340 }
341 }
342
343
344
345
346 public void setLearnt() {
347 learnt = true;
348 }
349
350
351
352
353
354
355 public boolean simplify() {
356 BigInteger cumul = BigInteger.ZERO;
357
358 int i = 0;
359 while (i < lits.length && cumul.compareTo(degree) < 0) {
360 if (voc.isSatisfied(lits[i])) {
361
362 cumul = cumul.add(coefs[i]);
363 }
364 i++;
365 }
366
367 return (cumul.compareTo(degree) >= 0);
368 }
369
370 public int size() {
371 return lits.length;
372 }
373
374
375
376
377 final protected void sort() {
378 assert this.lits != null;
379 if (coefs.length > 0) {
380 this.sort(0, size());
381 BigInteger buffInt = coefs[0];
382 for (int i = 1; i < coefs.length; i++) {
383 assert buffInt.compareTo(coefs[i]) >= 0;
384 buffInt = coefs[i];
385 }
386
387 }
388 }
389
390
391
392
393
394
395
396
397
398 final protected void sort(int from, int to) {
399 int width = to - from;
400 if (width <= 15)
401 selectionSort(from, to);
402
403 else {
404 int indPivot = width / 2 + from;
405 BigInteger pivot = coefs[indPivot];
406 int litPivot = lits[indPivot];
407 BigInteger tmp;
408 int i = from - 1;
409 int j = to;
410 int tmp2;
411
412 for (;;) {
413 do
414 i++;
415 while ((coefs[i].compareTo(pivot) > 0)
416 || ((coefs[i].equals(pivot)) && (lits[i] > litPivot)));
417 do
418 j--;
419 while ((pivot.compareTo(coefs[j]) > 0)
420 || ((coefs[j].equals(pivot)) && (lits[j] < litPivot)));
421
422 if (i >= j)
423 break;
424
425 tmp = coefs[i];
426 coefs[i] = coefs[j];
427 coefs[j] = tmp;
428 tmp2 = lits[i];
429 lits[i] = lits[j];
430 lits[j] = tmp2;
431 }
432
433 sort(from, i);
434 sort(i, to);
435 }
436
437 }
438
439 @Override
440 public String toString() {
441 StringBuffer stb = new StringBuffer();
442
443 if (lits.length > 0) {
444 for (int i = 0; i < lits.length; i++) {
445
446 stb.append(" + ");
447 stb.append(this.coefs[i]);
448 stb.append(".");
449 stb.append(Lits.toString(this.lits[i]));
450 stb.append("[");
451 stb.append(voc.valueToString(lits[i]));
452 stb.append("@");
453 stb.append(voc.getLevel(lits[i]));
454 stb.append("]");
455 stb.append(" ");
456
457 }
458 stb.append(">= ");
459 stb.append(this.degree);
460 }
461 return stb.toString();
462 }
463
464 public void assertConstraint(UnitPropagationListener s) {
465 BigInteger tmp = slackConstraint();
466 for (int i = 0; i < lits.length; i++) {
467 if (voc.isUnassigned(lits[i]) && tmp.compareTo(coefs[i]) < 0) {
468 boolean ret = s.enqueue(lits[i], this);
469 assert ret;
470 }
471 }
472 }
473
474
475
476
477
478
479 public BigInteger getDegree() {
480 return degree;
481 }
482
483 public void register() {
484 assert learnt;
485 try {
486 computeWatches();
487 } catch (ContradictionException e) {
488 System.out.println(this);
489 assert false;
490 }
491 }
492
493 public BigInteger[] getCoefs() {
494 BigInteger[] coefsBis = new BigInteger[coefs.length];
495 System.arraycopy(coefs, 0, coefsBis, 0, coefs.length);
496 return coefsBis;
497 }
498
499 public int[] getLits() {
500 int[] litsBis = new int[lits.length];
501 System.arraycopy(lits, 0, litsBis, 0, lits.length);
502 return litsBis;
503 }
504
505 public ILits getVocabulary() {
506 return voc;
507 }
508
509
510
511
512 public IVecInt computeAnImpliedClause() {
513 BigInteger cptCoefs = BigInteger.ZERO;
514 int index = coefs.length;
515 while ((cptCoefs.compareTo(degree) > 0) && (index > 0)) {
516 cptCoefs = cptCoefs.add(coefs[--index]);
517 }
518 if (index > 0 && index < size() / 2) {
519
520
521 IVecInt literals = new VecInt(index);
522 for (int j = 0; j <= index; j++)
523 literals.push(lits[j]);
524 return literals;
525 }
526 return null;
527 }
528
529 public boolean coefficientsEqualToOne() {
530 return false;
531 }
532
533 @Override
534 public boolean equals(Object pb) {
535 if (pb == null) {
536 return false;
537 }
538
539
540
541
542 try {
543
544 WatchPb wpb = (WatchPb) pb;
545 if (!degree.equals(wpb.degree) || coefs.length != wpb.coefs.length
546 || lits.length != wpb.lits.length) {
547 return false;
548 }
549 int lit;
550 boolean ok;
551 for (int ilit = 0; ilit < coefs.length; ilit++) {
552 lit = lits[ilit];
553 ok = false;
554 for (int ilit2 = 0; ilit2 < coefs.length; ilit2++)
555 if (wpb.lits[ilit2] == lit) {
556 if (!wpb.coefs[ilit2].equals(coefs[ilit])) {
557 return false;
558 }
559
560 ok = true;
561 break;
562
563 }
564 if (!ok) {
565 return false;
566 }
567 }
568 return true;
569 } catch (ClassCastException e) {
570 return false;
571 }
572 }
573
574 @Override
575 public int hashCode() {
576 long sum = 0;
577 for (int p : lits) {
578 sum += p;
579 }
580 return (int) sum / lits.length;
581 }
582
583 public void forwardActivity(double claInc) {
584 if (!learnt) {
585 activity += claInc;
586 }
587 }
588
589 }