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.math.BigInteger;
33
34 import org.sat4j.core.VecInt;
35 import org.sat4j.minisat.constraints.cnf.Lits;
36 import org.sat4j.minisat.core.ILits;
37 import org.sat4j.minisat.core.VarActivityListener;
38 import org.sat4j.specs.IteratorInt;
39
40
41
42
43
44 public class ConflictMap extends MapPb implements IConflict {
45
46 private final ILits voc;
47
48 protected boolean hasBeenReduced = false;
49 protected long numberOfReductions = 0;
50
51
52
53
54 protected BigInteger currentSlack;
55
56 protected int currentLevel;
57
58
59
60
61
62
63 protected VecInt[] byLevel;
64
65
66
67
68
69
70
71
72
73
74 public static IConflict createConflict(PBConstr cpb, int level) {
75 return new ConflictMap(cpb, level);
76 }
77
78 ConflictMap(PBConstr cpb, int level) {
79 super(cpb);
80 this.voc = cpb.getVocabulary();
81 this.currentLevel = level;
82 initStructures();
83 }
84
85 private void initStructures() {
86 this.currentSlack = BigInteger.ZERO;
87 this.byLevel = new VecInt[levelToIndex(this.currentLevel) + 1];
88 int ilit, litLevel, index;
89 BigInteger tmp;
90 for (int i = 0; i < size(); i++) {
91 ilit = this.weightedLits.getLit(i);
92 litLevel = this.voc.getLevel(ilit);
93
94 tmp = this.weightedLits.getCoef(i);
95 if (tmp.signum() > 0
96 && (!this.voc.isFalsified(ilit) || litLevel == this.currentLevel)) {
97 this.currentSlack = this.currentSlack.add(tmp);
98 }
99
100 index = levelToIndex(litLevel);
101 if (this.byLevel[index] == null) {
102 this.byLevel[index] = new VecInt();
103 }
104 this.byLevel[index].push(ilit);
105 }
106 }
107
108
109
110
111
112
113
114 private static int levelToIndex(int level) {
115 return level + 1;
116 }
117
118
119
120
121
122
123
124 private static int indexToLevel(int indLevel) {
125 return indLevel - 1;
126 }
127
128
129
130
131 protected BigInteger coefMult = BigInteger.ZERO;
132
133 protected BigInteger coefMultCons = BigInteger.ZERO;
134
135
136
137
138
139
140
141
142
143
144
145 public BigInteger resolve(PBConstr cpb, int litImplied,
146 VarActivityListener val) {
147 assert litImplied > 1;
148 int nLitImplied = litImplied ^ 1;
149 if (cpb == null || !this.weightedLits.containsKey(nLitImplied)) {
150
151
152 int litLevel = levelToIndex(this.voc.getLevel(litImplied));
153 int lit = 0;
154 if (this.byLevel[litLevel] != null) {
155 if (this.byLevel[litLevel].contains(litImplied)) {
156 lit = litImplied;
157 assert this.weightedLits.containsKey(litImplied);
158 } else if (this.byLevel[litLevel].contains(nLitImplied)) {
159 lit = nLitImplied;
160 assert this.weightedLits.containsKey(nLitImplied);
161 }
162 }
163
164 if (lit > 0) {
165 this.byLevel[litLevel].remove(lit);
166 if (this.byLevel[0] == null) {
167 this.byLevel[0] = new VecInt();
168 }
169 this.byLevel[0].push(lit);
170 }
171 return this.degree;
172 }
173
174 assert slackConflict().signum() <= 0;
175 assert this.degree.signum() >= 0;
176
177
178
179 BigInteger[] coefsCons = null;
180 BigInteger degreeCons = cpb.getDegree();
181
182
183 int ind = 0;
184 while (cpb.get(ind) != litImplied) {
185 ind++;
186 }
187
188 assert cpb.get(ind) == litImplied;
189 assert cpb.getCoef(ind) != BigInteger.ZERO;
190
191 if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
192
193
194 this.coefMultCons = this.weightedLits.get(nLitImplied);
195 this.coefMult = BigInteger.ONE;
196
197 degreeCons = degreeCons.multiply(this.coefMultCons);
198 } else {
199 if (this.weightedLits.get(nLitImplied).equals(BigInteger.ONE)) {
200
201
202 this.coefMult = cpb.getCoef(ind);
203 this.coefMultCons = BigInteger.ONE;
204
205 this.degree = this.degree.multiply(this.coefMult);
206 } else {
207
208
209
210 IWatchPb wpb = (IWatchPb) cpb;
211 coefsCons = wpb.getCoefs();
212 assert positiveCoefs(coefsCons);
213 degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
214 wpb);
215
216 degreeCons = degreeCons.multiply(this.coefMultCons);
217 this.degree = this.degree.multiply(this.coefMult);
218 }
219
220
221 if (!this.coefMult.equals(BigInteger.ONE)) {
222 for (int i = 0; i < size(); i++) {
223 changeCoef(i,
224 this.weightedLits.getCoef(i)
225 .multiply(this.coefMult));
226 }
227 }
228 }
229
230 assert slackConflict().signum() <= 0;
231
232
233 this.degree = cuttingPlane(cpb, degreeCons, coefsCons,
234 this.coefMultCons, val);
235
236
237 assert !this.weightedLits.containsKey(litImplied);
238 assert !this.weightedLits.containsKey(nLitImplied);
239
240 assert getLevelByLevel(litImplied) == -1;
241 assert getLevelByLevel(nLitImplied) == -1;
242 assert this.degree.signum() > 0;
243 assert slackConflict().signum() <= 0;
244
245
246 this.degree = saturation();
247 assert slackConflict().signum() <= 0;
248
249 return this.degree;
250 }
251
252
253
254
255
256
257
258
259 private BigInteger possReducedCoefs = BigInteger.ZERO;
260
261 protected BigInteger reduceUntilConflict(int litImplied, int ind,
262 BigInteger[] reducedCoefs, IWatchPb wpb) {
263 BigInteger slackResolve = BigInteger.ONE.negate();
264 BigInteger slackThis = BigInteger.ZERO;
265 BigInteger slackIndex;
266 BigInteger slackConflict = slackConflict();
267 BigInteger ppcm;
268 BigInteger reducedDegree = wpb.getDegree();
269 BigInteger previousCoefLitImplied = BigInteger.ZERO;
270 BigInteger tmp;
271 BigInteger coefLitImplied = this.weightedLits.get(litImplied ^ 1);
272 this.possReducedCoefs = possConstraint(wpb, reducedCoefs);
273
274 do {
275 if (slackResolve.signum() >= 0) {
276 assert slackThis.signum() > 0;
277 tmp = reduceInConstraint(wpb, reducedCoefs, ind, reducedDegree);
278 assert tmp.compareTo(reducedDegree) < 0
279 && tmp.compareTo(BigInteger.ONE) >= 0;
280 reducedDegree = tmp;
281 }
282
283 assert this.weightedLits.get(litImplied ^ 1).signum() > 0;
284 assert reducedCoefs[ind].signum() > 0;
285
286 if (!reducedCoefs[ind].equals(previousCoefLitImplied)) {
287 assert coefLitImplied.equals(this.weightedLits
288 .get(litImplied ^ 1));
289 ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
290 assert ppcm.signum() > 0;
291 this.coefMult = ppcm.divide(coefLitImplied);
292 this.coefMultCons = ppcm.divide(reducedCoefs[ind]);
293
294 assert this.coefMultCons.signum() > 0;
295 assert this.coefMult.signum() > 0;
296 assert this.coefMult.multiply(coefLitImplied).equals(
297 this.coefMultCons.multiply(reducedCoefs[ind]));
298 previousCoefLitImplied = reducedCoefs[ind];
299 }
300
301
302 slackThis = this.possReducedCoefs.subtract(reducedDegree).multiply(
303 this.coefMultCons);
304 assert slackThis.equals(wpb.slackConstraint(reducedCoefs,
305 reducedDegree).multiply(this.coefMultCons));
306 assert slackConflict.equals(slackConflict());
307 slackIndex = slackConflict.multiply(this.coefMult);
308 assert slackIndex.signum() <= 0;
309
310 slackResolve = slackThis.add(slackIndex);
311 } while (slackResolve.signum() >= 0);
312 assert this.coefMult.multiply(this.weightedLits.get(litImplied ^ 1))
313 .equals(this.coefMultCons.multiply(reducedCoefs[ind]));
314 return reducedDegree;
315
316 }
317
318 private BigInteger possConstraint(IWatchPb wpb, BigInteger[] theCoefs) {
319 BigInteger poss = BigInteger.ZERO;
320
321 for (int i = 0; i < wpb.size(); i++) {
322 if (!this.voc.isFalsified(wpb.get(i))) {
323 assert theCoefs[i].signum() >= 0;
324 poss = poss.add(theCoefs[i]);
325 }
326 }
327 return poss;
328 }
329
330
331
332
333 public BigInteger slackConflict() {
334 BigInteger poss = BigInteger.ZERO;
335 BigInteger tmp;
336
337 for (int i = 0; i < size(); i++) {
338 tmp = this.weightedLits.getCoef(i);
339 if (tmp.signum() != 0
340 && !this.voc.isFalsified(this.weightedLits.getLit(i))) {
341 assert tmp.signum() > 0;
342 poss = poss.add(tmp);
343 }
344 }
345 return poss.subtract(this.degree);
346 }
347
348 public boolean oldIsAssertive(int dl) {
349 BigInteger tmp;
350 int lit;
351 BigInteger slack = computeSlack(dl).subtract(this.degree);
352 if (slack.signum() < 0) {
353 return false;
354 }
355 for (int i = 0; i < size(); i++) {
356 tmp = this.weightedLits.getCoef(i);
357 lit = this.weightedLits.getLit(i);
358 if (tmp.signum() > 0
359 && (this.voc.isUnassigned(lit) || this.voc.getLevel(lit) >= dl)
360 && slack.compareTo(tmp) < 0) {
361 return true;
362 }
363 }
364 return false;
365 }
366
367
368 private BigInteger computeSlack(int dl) {
369 BigInteger slack = BigInteger.ZERO;
370 int lit;
371 BigInteger tmp;
372 for (int i = 0; i < size(); i++) {
373 tmp = this.weightedLits.getCoef(i);
374 lit = this.weightedLits.getLit(i);
375 if (tmp.signum() > 0
376 && (!this.voc.isFalsified(lit) || this.voc.getLevel(lit) >= dl)) {
377 slack = slack.add(tmp);
378 }
379 }
380 return slack;
381 }
382
383
384
385
386
387
388
389
390
391 public boolean isAssertive(int dl) {
392 assert dl <= this.currentLevel;
393 assert dl <= this.currentLevel;
394
395 this.currentLevel = dl;
396 BigInteger slack = this.currentSlack.subtract(this.degree);
397 if (slack.signum() < 0) {
398 return false;
399 }
400 return isImplyingLiteral(slack);
401 }
402
403
404
405
406 private boolean isImplyingLiteral(BigInteger slack) {
407
408 int unassigned = levelToIndex(-1);
409 int lit;
410 if (this.byLevel[unassigned] != null) {
411 for (IteratorInt iterator = this.byLevel[unassigned].iterator(); iterator
412 .hasNext();) {
413 lit = iterator.next();
414 if (slack.compareTo(this.weightedLits.get(lit)) < 0) {
415 this.assertiveLiteral = this.weightedLits
416 .getFromAllLits(lit);
417 return true;
418 }
419 }
420 }
421
422 BigInteger tmp;
423 int level = levelToIndex(this.currentLevel);
424 if (this.byLevel[level] != null) {
425 for (IteratorInt iterator = this.byLevel[level].iterator(); iterator
426 .hasNext();) {
427 lit = iterator.next();
428 tmp = this.weightedLits.get(lit);
429 if (tmp != null && slack.compareTo(tmp) < 0) {
430 this.assertiveLiteral = this.weightedLits
431 .getFromAllLits(lit);
432 return true;
433 }
434 }
435 }
436 return false;
437 }
438
439
440
441
442
443 private boolean isImplyingLiteralOrdered(int dl, BigInteger slack) {
444 int ilit, litLevel;
445 for (int i = 0; i < size(); i++) {
446 ilit = this.weightedLits.getLit(i);
447 litLevel = this.voc.getLevel(ilit);
448 if ((litLevel >= dl || this.voc.isUnassigned(ilit))
449 && slack.compareTo(this.weightedLits.getCoef(i)) < 0) {
450 return true;
451 }
452 }
453 return false;
454 }
455
456
457
458
459
460
461
462
463
464
465
466 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
467 return a.divide(a.gcd(b)).multiply(b);
468 }
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487 public BigInteger reduceInConstraint(IWatchPb wpb,
488 final BigInteger[] coefsBis, final int indLitImplied,
489 final BigInteger degreeBis) {
490 assert degreeBis.compareTo(BigInteger.ONE) > 0;
491
492 int lit = -1;
493 int size = wpb.size();
494 for (int ind = 0; ind < size && lit == -1; ind++) {
495 if (coefsBis[ind].signum() != 0
496 && this.voc.isUnassigned(wpb.get(ind))) {
497 assert coefsBis[ind].compareTo(degreeBis) < 0;
498 lit = ind;
499 }
500 }
501
502
503 if (lit == -1) {
504 for (int ind = 0; ind < size && lit == -1; ind++) {
505 if (coefsBis[ind].signum() != 0
506 && this.voc.isSatisfied(wpb.get(ind))
507 && ind != indLitImplied) {
508 lit = ind;
509 }
510 }
511 }
512
513
514 assert lit != -1;
515
516 assert lit != indLitImplied;
517
518 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
519 this.possReducedCoefs = this.possReducedCoefs.subtract(coefsBis[lit]);
520 coefsBis[lit] = BigInteger.ZERO;
521 assert this.possReducedCoefs.equals(possConstraint(wpb, coefsBis));
522
523
524 degUpdate = saturation(coefsBis, degUpdate, wpb);
525
526 assert coefsBis[indLitImplied].signum() > 0;
527 assert degreeBis.compareTo(degUpdate) > 0;
528 assert this.possReducedCoefs.equals(possConstraint(wpb, coefsBis));
529 return degUpdate;
530 }
531
532 private BigInteger saturation(BigInteger[] coefs, BigInteger degree,
533 IWatchPb wpb) {
534 assert degree.signum() > 0;
535 BigInteger degreeResult = degree;
536 boolean isMinimumEqualsToDegree = true;
537 int comparison;
538 for (int i = 0; i < coefs.length; i++) {
539 comparison = coefs[i].compareTo(degree);
540 if (comparison > 0) {
541 if (!this.voc.isFalsified(wpb.get(i))) {
542 this.possReducedCoefs = this.possReducedCoefs
543 .subtract(coefs[i]);
544 this.possReducedCoefs = this.possReducedCoefs.add(degree);
545 }
546 coefs[i] = degree;
547 } else if (comparison < 0 && coefs[i].signum() > 0) {
548 isMinimumEqualsToDegree = false;
549 }
550
551 }
552 if (isMinimumEqualsToDegree && !degree.equals(BigInteger.ONE)) {
553
554
555 this.possReducedCoefs = BigInteger.ZERO;
556 degreeResult = BigInteger.ONE;
557 for (int i = 0; i < coefs.length; i++) {
558 if (coefs[i].signum() > 0) {
559 coefs[i] = BigInteger.ONE;
560 if (!this.voc.isFalsified(wpb.get(i))) {
561 this.possReducedCoefs = this.possReducedCoefs
562 .add(BigInteger.ONE);
563 }
564 }
565 }
566 }
567 return degreeResult;
568 }
569
570 private static boolean positiveCoefs(final BigInteger[] coefsCons) {
571 for (BigInteger coefsCon : coefsCons) {
572 if (coefsCon.signum() <= 0) {
573 return false;
574 }
575 }
576 return true;
577 }
578
579
580
581
582
583
584
585
586
587
588 public int getBacktrackLevel(int maxLevel) {
589
590
591 VecInt lits;
592 int level;
593 int indStop = levelToIndex(maxLevel) - 1;
594 int indStart = levelToIndex(0);
595 BigInteger slack = computeSlack(0).subtract(this.degree);
596 int previous = 0;
597 for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
598 if (this.byLevel[indLevel] != null) {
599 level = indexToLevel(indLevel);
600 assert computeSlack(level).subtract(this.degree).equals(slack);
601 if (isImplyingLiteralOrdered(level, slack)) {
602 break;
603 }
604
605 lits = this.byLevel[indLevel];
606 int lit;
607 for (IteratorInt iterator = lits.iterator(); iterator.hasNext();) {
608 lit = iterator.next();
609 if (this.voc.isFalsified(lit)
610 && this.voc.getLevel(lit) == indexToLevel(indLevel)) {
611 slack = slack.subtract(this.weightedLits.get(lit));
612 }
613 }
614 if (!lits.isEmpty()) {
615 previous = level;
616 }
617 }
618 }
619 assert previous == oldGetBacktrackLevel(maxLevel);
620 return previous;
621 }
622
623 public int oldGetBacktrackLevel(int maxLevel) {
624 int litLevel;
625 int borneMax = maxLevel;
626 assert oldIsAssertive(borneMax);
627 int borneMin = -1;
628
629
630 for (int i = 0; i < size(); i++) {
631 litLevel = this.voc.getLevel(this.weightedLits.getLit(i));
632 if (litLevel < borneMax && litLevel > borneMin
633 && oldIsAssertive(litLevel)) {
634 borneMax = litLevel;
635 }
636 }
637
638
639 int retour = 0;
640 for (int i = 0; i < size(); i++) {
641 litLevel = this.voc.getLevel(this.weightedLits.getLit(i));
642 if (litLevel > retour && litLevel < borneMax) {
643 retour = litLevel;
644 }
645 }
646 return retour;
647 }
648
649 public void updateSlack(int level) {
650 int dl = levelToIndex(level);
651 if (this.byLevel[dl] != null) {
652 int lit;
653 for (IteratorInt iterator = this.byLevel[dl].iterator(); iterator
654 .hasNext();) {
655 lit = iterator.next();
656 if (this.voc.isFalsified(lit)) {
657 this.currentSlack = this.currentSlack.add(this.weightedLits
658 .get(lit));
659 }
660 }
661 }
662 }
663
664 @Override
665 void increaseCoef(int lit, BigInteger incCoef) {
666 if (!this.voc.isFalsified(lit)
667 || this.voc.getLevel(lit) == this.currentLevel) {
668 this.currentSlack = this.currentSlack.add(incCoef);
669 }
670 assert this.byLevel[levelToIndex(this.voc.getLevel(lit))].contains(lit);
671 super.increaseCoef(lit, incCoef);
672 }
673
674 @Override
675 void decreaseCoef(int lit, BigInteger decCoef) {
676 if (!this.voc.isFalsified(lit)
677 || this.voc.getLevel(lit) == this.currentLevel) {
678 this.currentSlack = this.currentSlack.subtract(decCoef);
679 }
680 assert this.byLevel[levelToIndex(this.voc.getLevel(lit))].contains(lit);
681 super.decreaseCoef(lit, decCoef);
682 }
683
684 @Override
685 void setCoef(int lit, BigInteger newValue) {
686 int litLevel = this.voc.getLevel(lit);
687 if (!this.voc.isFalsified(lit) || litLevel == this.currentLevel) {
688 if (this.weightedLits.containsKey(lit)) {
689 this.currentSlack = this.currentSlack
690 .subtract(this.weightedLits.get(lit));
691 }
692 this.currentSlack = this.currentSlack.add(newValue);
693 }
694 int indLitLevel = levelToIndex(litLevel);
695 if (!this.weightedLits.containsKey(lit)) {
696 if (this.byLevel[indLitLevel] == null) {
697 this.byLevel[indLitLevel] = new VecInt();
698 }
699 this.byLevel[indLitLevel].push(lit);
700
701 }
702 assert this.byLevel[indLitLevel] != null;
703 assert this.byLevel[indLitLevel].contains(lit);
704 super.setCoef(lit, newValue);
705 }
706
707 @Override
708 void changeCoef(int indLit, BigInteger newValue) {
709 int lit = this.weightedLits.getLit(indLit);
710 int litLevel = this.voc.getLevel(lit);
711 if (!this.voc.isFalsified(lit) || litLevel == this.currentLevel) {
712 if (this.weightedLits.containsKey(lit)) {
713 this.currentSlack = this.currentSlack
714 .subtract(this.weightedLits.get(lit));
715 }
716 this.currentSlack = this.currentSlack.add(newValue);
717 }
718 int indLitLevel = levelToIndex(litLevel);
719 assert this.weightedLits.containsKey(lit);
720 assert this.byLevel[indLitLevel] != null;
721 assert this.byLevel[indLitLevel].contains(lit);
722 super.changeCoef(indLit, newValue);
723 }
724
725 @Override
726 void removeCoef(int lit) {
727 int litLevel = this.voc.getLevel(lit);
728 if (!this.voc.isFalsified(lit) || litLevel == this.currentLevel) {
729 this.currentSlack = this.currentSlack.subtract(this.weightedLits
730 .get(lit));
731 }
732 int indLitLevel = levelToIndex(litLevel);
733 assert indLitLevel < this.byLevel.length;
734 assert this.byLevel[indLitLevel] != null;
735 assert this.byLevel[indLitLevel].contains(lit);
736 this.byLevel[indLitLevel].remove(lit);
737 super.removeCoef(lit);
738 }
739
740 private int getLevelByLevel(int lit) {
741 for (int i = 0; i < this.byLevel.length; i++) {
742 if (this.byLevel[i] != null && this.byLevel[i].contains(lit)) {
743 return i;
744 }
745 }
746 return -1;
747 }
748
749 public boolean slackIsCorrect(int dl) {
750 return this.currentSlack.equals(computeSlack(dl));
751 }
752
753 @Override
754 public String toString() {
755 int lit;
756 StringBuffer stb = new StringBuffer();
757 for (int i = 0; i < size(); i++) {
758 lit = this.weightedLits.getLit(i);
759 stb.append(this.weightedLits.getCoef(i));
760 stb.append(".");
761 stb.append(Lits.toString(lit));
762 stb.append(" ");
763 stb.append("[");
764 stb.append(this.voc.valueToString(lit));
765 stb.append("@");
766 stb.append(this.voc.getLevel(lit));
767 stb.append("]");
768 }
769 return stb.toString() + " >= " + this.degree;
770 }
771
772 public boolean hasBeenReduced() {
773 return this.hasBeenReduced;
774 }
775
776 public long getNumberOfReductions() {
777 return this.numberOfReductions;
778 }
779
780 }