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