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