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