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 WatchPb wpb = (WatchPb) 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, WatchPb 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 poss = poss.add(tmp);
306 }
307 return poss.subtract(degree);
308 }
309
310 public boolean oldIsAssertive(int dl) {
311 BigInteger tmp;
312 int lit;
313 BigInteger slack = computeSlack(dl).subtract(degree);
314 if (slack.signum() < 0)
315 return false;
316 for (int i = 0; i < size(); i++) {
317 tmp = weightedLits.getCoef(i);
318 lit = weightedLits.getLit(i);
319 if ((tmp.signum() > 0)
320 && (voc.isUnassigned(lit) || voc.getLevel(lit) >= dl)
321 && (slack.compareTo(tmp) < 0))
322 return true;
323 }
324 return false;
325 }
326
327
328 private BigInteger computeSlack(int dl) {
329 BigInteger slack = BigInteger.ZERO;
330 int lit;
331 BigInteger tmp;
332 for (int i = 0; i < size(); i++) {
333 tmp = weightedLits.getCoef(i);
334 lit = weightedLits.getLit(i);
335 if ((tmp.signum() > 0)
336 && (((!voc.isFalsified(lit)) || voc.getLevel(lit) >= dl)))
337 slack = slack.add(tmp);
338 }
339 return slack;
340 }
341
342
343
344
345
346
347
348
349
350 public boolean isAssertive(int dl) {
351 assert dl <= currentLevel;
352 assert dl <= currentLevel;
353
354 currentLevel = dl;
355
356 BigInteger slack = currentSlack.subtract(degree);
357 if (slack.signum() < 0)
358 return false;
359 return isImplyingLiteral(slack);
360 }
361
362
363
364
365 private boolean isImplyingLiteral(BigInteger slack) {
366
367 int unassigned = levelToIndex(-1);
368 int lit;
369 if (byLevel[unassigned] != null) {
370 for (IteratorInt iterator = byLevel[unassigned].iterator(); iterator
371 .hasNext();) {
372 lit = iterator.next();
373 if (slack.compareTo(weightedLits.get(lit)) < 0) {
374 assertiveLiteral = weightedLits.allLits.get(lit);
375 return true;
376 }
377 }
378 }
379
380 BigInteger tmp;
381 int level = levelToIndex(currentLevel);
382 if (byLevel[level] != null)
383 for (IteratorInt iterator = byLevel[level].iterator(); iterator
384 .hasNext();) {
385 lit = iterator.next();
386 tmp = weightedLits.get(lit);
387 if (tmp != null && slack.compareTo(tmp) < 0) {
388 assertiveLiteral = weightedLits.allLits.get(lit);
389 return true;
390 }
391 }
392 return false;
393 }
394
395
396
397
398
399 private boolean isImplyingLiteralOrdered(int dl, BigInteger slack) {
400 int ilit, litLevel;
401 for (int i = 0; i < size(); i++) {
402 ilit = weightedLits.getLit(i);
403 litLevel = voc.getLevel(ilit);
404 if ((litLevel >= dl || voc.isUnassigned(ilit))
405 && (slack.compareTo(weightedLits.getCoef(i)) < 0))
406 return true;
407 }
408 return false;
409 }
410
411
412
413
414
415
416
417
418
419
420
421 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
422 return a.divide(a.gcd(b)).multiply(b);
423 }
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442 public BigInteger reduceInConstraint(WatchPb wpb,
443 final BigInteger[] coefsBis, final int indLitImplied,
444 final BigInteger degreeBis) {
445
446 assert degreeBis.compareTo(BigInteger.ONE) > 0;
447
448 int lit = -1;
449 for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
450 if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.lits[ind])) {
451 assert coefsBis[ind].compareTo(degreeBis) < 0;
452 lit = ind;
453 }
454
455
456 if (lit == -1)
457 for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
458 if ((coefsBis[ind].signum() != 0)
459 && (voc.isSatisfied(wpb.lits[ind]))
460 && (ind != indLitImplied))
461 lit = ind;
462
463
464 assert lit != -1;
465
466 assert lit != indLitImplied;
467
468
469 BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
470 coefsBis[lit] = BigInteger.ZERO;
471
472
473 degUpdate = saturation(coefsBis, degUpdate);
474
475 assert coefsBis[indLitImplied].signum() > 0;
476 assert degreeBis.compareTo(degUpdate) > 0;
477 return degUpdate;
478 }
479
480 static BigInteger saturation(BigInteger[] coefs, BigInteger degree) {
481 assert degree.signum() > 0;
482 BigInteger minimum = degree;
483 for (int i = 0; i < coefs.length; i++) {
484 if (coefs[i].signum() > 0)
485 minimum = minimum.min(coefs[i]);
486 coefs[i] = degree.min(coefs[i]);
487 }
488 if (minimum.equals(degree) && !degree.equals(BigInteger.ONE)) {
489
490
491 degree = BigInteger.ONE;
492 for (int i = 0; i < coefs.length; i++)
493 if (coefs[i].signum() > 0)
494 coefs[i] = degree;
495 }
496 return degree;
497 }
498
499 private static boolean positiveCoefs(final BigInteger[] coefsCons) {
500 for (int i = 0; i < coefsCons.length; i++) {
501 if (coefsCons[i].signum() <= 0)
502 return false;
503 }
504 return true;
505 }
506
507
508
509
510
511
512
513
514
515
516 public int getBacktrackLevel(int maxLevel) {
517
518
519 VecInt lits;
520 int level;
521 int indStop = levelToIndex(maxLevel) - 1;
522 int indStart = levelToIndex(0);
523 BigInteger slack = computeSlack(0).subtract(degree);
524 int previous = 0;
525 for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
526 if (byLevel[indLevel] != null) {
527 level = indexToLevel(indLevel);
528 assert computeSlack(level).subtract(degree).equals(slack);
529 if (isImplyingLiteralOrdered(level, slack)) {
530 break;
531 }
532
533 lits = byLevel[indLevel];
534 int lit;
535 for (IteratorInt iterator = lits.iterator(); iterator.hasNext();) {
536 lit = iterator.next();
537 if (voc.isFalsified(lit)
538 && voc.getLevel(lit) == indexToLevel(indLevel))
539 slack = slack.subtract(weightedLits.get(lit));
540 }
541 if (!lits.isEmpty())
542 previous = level;
543 }
544 }
545 assert previous == oldGetBacktrackLevel(maxLevel);
546 return previous;
547 }
548
549 public int oldGetBacktrackLevel(int maxLevel) {
550 int litLevel;
551 int borneMax = maxLevel;
552 assert oldIsAssertive(borneMax);
553 int borneMin = -1;
554
555
556 for (int i = 0; i < size(); i++) {
557 litLevel = voc.getLevel(weightedLits.getLit(i));
558 if (litLevel < borneMax && litLevel > borneMin
559 && oldIsAssertive(litLevel))
560 borneMax = litLevel;
561 }
562
563
564 int retour = 0;
565 for (int i = 0; i < size(); i++) {
566 litLevel = voc.getLevel(weightedLits.getLit(i));
567 if (litLevel > retour && litLevel < borneMax) {
568 retour = litLevel;
569 }
570 }
571 return retour;
572 }
573
574 public void updateSlack(int level) {
575 int dl = levelToIndex(level);
576 if (byLevel[dl] != null) {
577 int lit;
578 for (IteratorInt iterator = byLevel[dl].iterator(); iterator
579 .hasNext();) {
580 lit = iterator.next();
581 if (voc.isFalsified(lit))
582 currentSlack = currentSlack.add(weightedLits.get(lit));
583 }
584 }
585 }
586
587 @Override
588 void increaseCoef(int lit, BigInteger incCoef) {
589 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
590 currentSlack = currentSlack.add(incCoef);
591 }
592 assert byLevel[levelToIndex(voc.getLevel(lit))].contains(lit);
593 super.increaseCoef(lit, incCoef);
594 }
595
596 @Override
597 void decreaseCoef(int lit, BigInteger decCoef) {
598 if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
599 currentSlack = currentSlack.subtract(decCoef);
600 }
601 assert byLevel[levelToIndex(voc.getLevel(lit))].contains(lit);
602 super.decreaseCoef(lit, decCoef);
603 }
604
605 @Override
606 void setCoef(int lit, BigInteger newValue) {
607 int litLevel = voc.getLevel(lit);
608 if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
609 if (weightedLits.containsKey(lit))
610 currentSlack = currentSlack.subtract(weightedLits.get(lit));
611 currentSlack = currentSlack.add(newValue);
612 }
613 int indLitLevel = levelToIndex(litLevel);
614 if (!weightedLits.containsKey(lit)) {
615 if (byLevel[indLitLevel] == null) {
616 byLevel[indLitLevel] = new VecInt();
617 }
618 byLevel[indLitLevel].push(lit);
619
620 }
621 assert byLevel[indLitLevel] != null;
622 assert byLevel[indLitLevel].contains(lit);
623 super.setCoef(lit, newValue);
624 }
625
626 @Override
627 void changeCoef(int indLit, BigInteger newValue) {
628 int lit = weightedLits.getLit(indLit);
629 int litLevel = voc.getLevel(lit);
630 if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
631 if (weightedLits.containsKey(lit))
632 currentSlack = currentSlack.subtract(weightedLits.get(lit));
633 currentSlack = currentSlack.add(newValue);
634 }
635 int indLitLevel = levelToIndex(litLevel);
636 assert weightedLits.containsKey(lit);
637 assert byLevel[indLitLevel] != null;
638 assert byLevel[indLitLevel].contains(lit);
639 super.changeCoef(indLit, newValue);
640 }
641
642 @Override
643 void removeCoef(int lit) {
644 int litLevel = voc.getLevel(lit);
645 if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
646 currentSlack = currentSlack.subtract(weightedLits.get(lit));
647 }
648 int indLitLevel = levelToIndex(litLevel);
649 assert indLitLevel < byLevel.length;
650 assert byLevel[indLitLevel] != null;
651 assert byLevel[indLitLevel].contains(lit);
652 byLevel[indLitLevel].remove(lit);
653 super.removeCoef(lit);
654 }
655
656 private int getLevelByLevel(int lit) {
657 for (int i = 0; i < byLevel.length; i++)
658 if (byLevel[i] != null && byLevel[i].contains(lit))
659 return i;
660 return -1;
661 }
662
663 public boolean slackIsCorrect(int dl) {
664 return currentSlack.equals(computeSlack(dl));
665 }
666
667 @Override
668 public String toString() {
669 int lit;
670 StringBuffer stb = new StringBuffer();
671 for (int i = 0; i < size(); i++) {
672 lit = weightedLits.getLit(i);
673 stb.append(weightedLits.getCoef(i));
674 stb.append(".");
675 stb.append(Lits.toString(lit));
676 stb.append(" ");
677 stb.append("[");
678 stb.append(voc.valueToString(lit));
679 stb.append("@");
680 stb.append(voc.getLevel(lit));
681 stb.append("]");
682 }
683 return stb.toString() + " >= " + degree;
684 }
685
686 public boolean hasBeenReduced() {
687 return hasBeenReduced;
688 }
689
690 public long getNumberOfReductions() {
691 return numberOfReductions;
692 }
693 }