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
54
55
56 protected double activity;
57
58
59
60
61
62 protected BigInteger[] bigCoefs;
63
64
65
66
67 protected BigInteger bigDegree;
68
69
70
71
72 protected long[] coefs;
73
74 protected long sumcoefs;
75
76
77
78
79 protected long degree;
80
81
82
83
84 protected int[] lits;
85
86
87
88
89 protected boolean learnt = false;
90
91
92
93
94 protected ILits voc;
95
96
97
98
99 WatchPbLongCP() {
100 }
101
102
103 WatchPbLongCP(IDataStructurePB mpb) {
104 int size = mpb.size();
105 this.lits = new int[size];
106 this.bigCoefs = new BigInteger[size];
107 mpb.buildConstraintFromMapPb(this.lits, this.bigCoefs);
108 assert mpb.isLongSufficient();
109
110
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 abstract protected void computeWatches() throws ContradictionException;
203
204 abstract protected 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, best_i;
380 long tmp;
381 BigInteger bigTmp;
382 int tmp2;
383
384 for (i = from; i < to - 1; i++) {
385 best_i = i;
386 for (j = i + 1; j < to; j++) {
387 if (this.coefs[j] > this.coefs[best_i]
388 || this.coefs[j] == this.coefs[best_i]
389 && this.lits[j] > this.lits[best_i]) {
390 best_i = j;
391 }
392 }
393 tmp = this.coefs[i];
394 this.coefs[i] = this.coefs[best_i];
395 this.coefs[best_i] = tmp;
396 bigTmp = this.bigCoefs[i];
397 this.bigCoefs[i] = this.bigCoefs[best_i];
398 this.bigCoefs[best_i] = bigTmp;
399 tmp2 = this.lits[i];
400 this.lits[i] = this.lits[best_i];
401 this.lits[best_i] = tmp2;
402 assert this.coefs[i] >= 0;
403 assert this.coefs[best_i] >= 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 final protected 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
457
458
459
460
461
462 final protected void sort(int from, int to) {
463 int width = to - from;
464 if (width <= 15) {
465 selectionSort(from, to);
466 } else {
467 assert this.coefs.length == this.bigCoefs.length;
468 int indPivot = width / 2 + from;
469 long pivot = this.coefs[indPivot];
470 int litPivot = this.lits[indPivot];
471 long tmp;
472 BigInteger bigTmp;
473 int i = from - 1;
474 int j = to;
475 int tmp2;
476
477 for (;;) {
478 do {
479 i++;
480 } while (this.coefs[i] > pivot || this.coefs[i] == pivot
481 && this.lits[i] > litPivot);
482 do {
483 j--;
484 } while (pivot > this.coefs[j] || this.coefs[j] == pivot
485 && this.lits[j] < litPivot);
486
487 if (i >= j) {
488 break;
489 }
490
491 tmp = this.coefs[i];
492 this.coefs[i] = this.coefs[j];
493 this.coefs[j] = tmp;
494 bigTmp = this.bigCoefs[i];
495 this.bigCoefs[i] = this.bigCoefs[j];
496 this.bigCoefs[j] = bigTmp;
497 tmp2 = this.lits[i];
498 this.lits[i] = this.lits[j];
499 this.lits[j] = tmp2;
500 assert this.coefs[i] >= 0;
501 assert this.coefs[j] >= 0;
502 }
503
504 sort(from, i);
505 sort(i, to);
506 }
507
508 }
509
510 @Override
511 public String toString() {
512 StringBuffer stb = new StringBuffer();
513
514 if (this.lits.length > 0) {
515 for (int i = 0; i < this.lits.length; i++) {
516
517 stb.append(" + ");
518 stb.append(this.coefs[i]);
519 stb.append(".");
520 stb.append(Lits.toString(this.lits[i]));
521 stb.append("[");
522 stb.append(this.voc.valueToString(this.lits[i]));
523 stb.append("@");
524 stb.append(this.voc.getLevel(this.lits[i]));
525 stb.append("]");
526 stb.append(" ");
527
528 }
529 stb.append(">= ");
530 stb.append(this.degree);
531 }
532 return stb.toString();
533 }
534
535 public void assertConstraint(UnitPropagationListener s) {
536 long tmp = slackConstraint();
537 for (int i = 0; i < this.lits.length; i++) {
538 if (this.voc.isUnassigned(this.lits[i]) && tmp < this.coefs[i]) {
539 boolean ret = s.enqueue(this.lits[i], this);
540 assert ret;
541 }
542 }
543 }
544
545 public void register() {
546 assert this.learnt;
547 try {
548 computeWatches();
549 } catch (ContradictionException e) {
550 System.out.println(this);
551 assert false;
552 }
553 }
554
555
556
557
558
559
560 public int[] getLits() {
561 int[] litsBis = new int[this.lits.length];
562 System.arraycopy(this.lits, 0, litsBis, 0, this.lits.length);
563 return litsBis;
564 }
565
566 public ILits getVocabulary() {
567 return this.voc;
568 }
569
570
571
572
573
574
575 public IVecInt computeAnImpliedClause() {
576 long cptCoefs = 0;
577 int index = this.coefs.length;
578 while (cptCoefs > this.degree && index > 0) {
579 cptCoefs = cptCoefs + this.coefs[--index];
580 }
581 if (index > 0 && index < size() / 2) {
582 IVecInt literals = new VecInt(index);
583 for (int j = 0; j <= index; j++) {
584 literals.push(this.lits[j]);
585 }
586 return literals;
587 }
588 return null;
589 }
590
591 public boolean coefficientsEqualToOne() {
592 return false;
593 }
594
595 @Override
596 public boolean equals(Object pb) {
597 if (pb == null) {
598 return false;
599 }
600
601
602
603
604 try {
605
606 WatchPbLongCP wpb = (WatchPbLongCP) pb;
607 if (this.degree != wpb.degree
608 || this.coefs.length != wpb.coefs.length
609 || this.lits.length != wpb.lits.length) {
610 return false;
611 }
612 int lit;
613 boolean ok;
614 for (int ilit = 0; ilit < this.coefs.length; ilit++) {
615 lit = this.lits[ilit];
616 ok = false;
617 for (int ilit2 = 0; ilit2 < this.coefs.length; ilit2++) {
618 if (wpb.lits[ilit2] == lit) {
619 if (wpb.coefs[ilit2] != this.coefs[ilit]) {
620 return false;
621 }
622
623 ok = true;
624 break;
625
626 }
627 }
628 if (!ok) {
629 return false;
630 }
631 }
632 return true;
633 } catch (ClassCastException e) {
634 return false;
635 }
636 }
637
638 @Override
639 public int hashCode() {
640 long sum = 0;
641 for (int p : this.lits) {
642 sum += p;
643 }
644 return (int) sum / this.lits.length;
645 }
646
647 public void forwardActivity(double claInc) {
648 if (!this.learnt) {
649 this.activity += claInc;
650 }
651 }
652
653 public long[] getLongCoefs() {
654 long[] coefsBis = new long[this.coefs.length];
655 System.arraycopy(this.coefs, 0, coefsBis, 0, this.coefs.length);
656 return coefsBis;
657 }
658
659 public BigInteger slackConstraint(BigInteger[] theCoefs,
660 BigInteger theDegree) {
661 return computeLeftSide(theCoefs).subtract(theDegree);
662 }
663
664
665
666
667
668
669
670
671 public BigInteger getCoef(int i) {
672 return this.bigCoefs[i];
673 }
674
675
676
677
678
679
680 public BigInteger[] getCoefs() {
681 BigInteger[] coefsBis = new BigInteger[this.coefs.length];
682 System.arraycopy(this.bigCoefs, 0, coefsBis, 0, this.coefs.length);
683 return coefsBis;
684 }
685
686
687
688
689 public BigInteger getDegree() {
690 return this.bigDegree;
691 }
692
693 public boolean canBePropagatedMultipleTimes() {
694 return true;
695 }
696
697 public Constr toConstraint() {
698 return this;
699 }
700 }