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