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