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.minisat.core.UnitPropagationListener;
42 import org.sat4j.specs.ContradictionException;
43 import org.sat4j.specs.IVecInt;
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 register() {
538 assert this.learnt;
539 try {
540 computeWatches();
541 } catch (ContradictionException e) {
542 System.out.println(this);
543 assert false;
544 }
545 }
546
547
548
549
550
551
552 public int[] getLits() {
553 int[] litsBis = new int[this.lits.length];
554 System.arraycopy(this.lits, 0, litsBis, 0, this.lits.length);
555 return litsBis;
556 }
557
558 public ILits getVocabulary() {
559 return this.voc;
560 }
561
562
563
564
565
566
567 public IVecInt computeAnImpliedClause() {
568 long cptCoefs = 0;
569 int index = this.coefs.length;
570 while (cptCoefs > this.degree && index > 0) {
571 cptCoefs = cptCoefs + this.coefs[--index];
572 }
573 if (index > 0 && index < size() / 2) {
574 IVecInt literals = new VecInt(index);
575 for (int j = 0; j <= index; j++) {
576 literals.push(this.lits[j]);
577 }
578 return literals;
579 }
580 return null;
581 }
582
583 public boolean coefficientsEqualToOne() {
584 return false;
585 }
586
587 @Override
588 public boolean equals(Object pb) {
589 if (pb == null) {
590 return false;
591 }
592
593
594
595
596 try {
597
598 WatchPbLongCP wpb = (WatchPbLongCP) pb;
599 if (this.degree != wpb.degree
600 || this.coefs.length != wpb.coefs.length
601 || this.lits.length != wpb.lits.length) {
602 return false;
603 }
604 int lit;
605 boolean ok;
606 for (int ilit = 0; ilit < this.coefs.length; ilit++) {
607 lit = this.lits[ilit];
608 ok = false;
609 for (int ilit2 = 0; ilit2 < this.coefs.length; ilit2++) {
610 if (wpb.lits[ilit2] == lit) {
611 if (wpb.coefs[ilit2] != this.coefs[ilit]) {
612 return false;
613 }
614
615 ok = true;
616 break;
617
618 }
619 }
620 if (!ok) {
621 return false;
622 }
623 }
624 return true;
625 } catch (ClassCastException e) {
626 return false;
627 }
628 }
629
630 @Override
631 public int hashCode() {
632 long sum = 0;
633 for (int p : this.lits) {
634 sum += p;
635 }
636 return (int) sum / this.lits.length;
637 }
638
639 public void forwardActivity(double claInc) {
640 if (!this.learnt) {
641 this.activity += claInc;
642 }
643 }
644
645 public long[] getLongCoefs() {
646 long[] coefsBis = new long[this.coefs.length];
647 System.arraycopy(this.coefs, 0, coefsBis, 0, this.coefs.length);
648 return coefsBis;
649 }
650
651 public BigInteger slackConstraint(BigInteger[] theCoefs,
652 BigInteger theDegree) {
653 return computeLeftSide(theCoefs).subtract(theDegree);
654 }
655
656
657
658
659
660
661
662
663 public BigInteger getCoef(int i) {
664 return this.bigCoefs[i];
665 }
666
667
668
669
670
671
672 public BigInteger[] getCoefs() {
673 BigInteger[] coefsBis = new BigInteger[this.coefs.length];
674 System.arraycopy(this.bigCoefs, 0, coefsBis, 0, this.coefs.length);
675 return coefsBis;
676 }
677
678
679
680
681 public BigInteger getDegree() {
682 return this.bigDegree;
683 }
684
685 public boolean canBePropagatedMultipleTimes() {
686 return true;
687 }
688
689 public Constr toConstraint() {
690 return this;
691 }
692
693 public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) {
694 throw new UnsupportedOperationException("Not implemented yet!");
695 }
696 }