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