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
45 public abstract class WatchPbLong implements Propagatable, Constr, Undoable,
46 Serializable {
47
48
49
50
51 private static final long serialVersionUID = 1L;
52
53
54
55
56 protected double activity;
57
58
59
60
61 protected long[] coefs;
62
63 protected long sumcoefs;
64
65
66
67
68 protected long degree;
69
70
71
72
73 protected int[] lits;
74
75
76
77
78 protected boolean learnt = false;
79
80
81
82
83 protected ILits voc;
84
85
86
87
88 WatchPbLong() {
89 }
90
91
92 WatchPbLong(IDataStructurePB mpb) {
93 int size = mpb.size();
94 this.lits = new int[size];
95 BigInteger[] bigCoefs = new BigInteger[size];
96 mpb.buildConstraintFromMapPb(this.lits, bigCoefs);
97 this.coefs = toLong(bigCoefs);
98
99 this.degree = mpb.getDegree().longValue();
100 this.sumcoefs = 0;
101 for (long c : this.coefs) {
102 this.sumcoefs += c;
103 }
104 this.learnt = true;
105
106 sort();
107 }
108
109
110 WatchPbLong(int[] lits, BigInteger[] coefs, BigInteger degree,
111 BigInteger sumCoefs) {
112 this.lits = lits;
113 this.coefs = toLong(coefs);
114 this.degree = degree.longValue();
115 this.sumcoefs = sumCoefs.longValue();
116
117 sort();
118 }
119
120 public static long[] toLong(BigInteger[] bigValues) {
121 long[] res = new long[bigValues.length];
122 for (int i = 0; i < res.length; i++) {
123 res[i] = bigValues[i].longValue();
124 }
125 return res;
126 }
127
128
129
130
131
132
133
134
135 public boolean isAssertive(int dl) {
136 long slack = 0;
137 for (int i = 0; i < this.lits.length; i++) {
138 if (this.coefs[i] > 0
139 && (!this.voc.isFalsified(this.lits[i]) || this.voc
140 .getLevel(this.lits[i]) >= dl)) {
141 slack = slack + this.coefs[i];
142 }
143 }
144 slack = slack - this.degree;
145 if (slack < 0) {
146 return false;
147 }
148 for (int i = 0; i < this.lits.length; i++) {
149 if (this.coefs[i] > 0
150 && (this.voc.isUnassigned(this.lits[i]) || this.voc
151 .getLevel(this.lits[i]) >= dl)
152 && slack < this.coefs[i]) {
153 return true;
154 }
155 }
156 return false;
157 }
158
159
160
161
162
163
164
165
166
167
168
169 public void calcReason(int p, IVecInt outReason) {
170 long sumfalsified = 0;
171 long tous = 0;
172 final int[] mlits = this.lits;
173 boolean ok = true;
174 for (int i = 0; i < mlits.length; i++) {
175 int q = mlits[i];
176 if (this.voc.isFalsified(q)) {
177 if (ok) {
178 outReason.push(q ^ 1);
179 sumfalsified += this.coefs[i];
180 if (this.sumcoefs - sumfalsified < this.degree) {
181 ok = false;
182 tous = sumfalsified;
183
184 }
185 } else {
186 tous += this.coefs[i];
187 }
188 }
189 }
190 }
191
192 abstract protected void computeWatches() throws ContradictionException;
193
194 abstract protected void computePropagation(UnitPropagationListener s)
195 throws ContradictionException;
196
197
198
199
200
201
202
203
204 public int get(int i) {
205 return this.lits[i];
206 }
207
208
209
210
211
212
213
214 public double getActivity() {
215 return this.activity;
216 }
217
218
219
220
221
222
223 public void incActivity(double claInc) {
224 if (this.learnt) {
225 this.activity += claInc;
226 }
227 }
228
229 public void setActivity(double d) {
230 if (this.learnt) {
231 this.activity = d;
232 }
233 }
234
235
236
237
238
239
240
241 public long slackConstraint() {
242 return computeLeftSide() - this.degree;
243 }
244
245
246
247
248
249
250
251
252
253
254
255 public long slackConstraint(long[] theCoefs, long theDegree) {
256 return computeLeftSide(theCoefs) - theDegree;
257 }
258
259
260
261
262
263
264
265
266
267 public long computeLeftSide(long[] theCoefs) {
268 long poss = 0;
269
270 for (int i = 0; i < this.lits.length; i++) {
271 if (!this.voc.isFalsified(this.lits[i])) {
272 assert theCoefs[i] >= 0;
273 poss = poss + theCoefs[i];
274 }
275 }
276 return poss;
277 }
278
279
280
281
282
283
284
285 public long computeLeftSide() {
286 return computeLeftSide(this.coefs);
287 }
288
289
290
291
292
293
294
295
296 protected boolean isSatisfiable() {
297 return computeLeftSide() >= this.degree;
298 }
299
300
301
302
303
304
305
306 public boolean learnt() {
307 return this.learnt;
308 }
309
310
311
312
313
314
315 public boolean locked() {
316 for (int p : this.lits) {
317 if (this.voc.getReason(p) == this) {
318 return true;
319 }
320 }
321 return false;
322 }
323
324
325
326
327
328
329
330
331
332
333
334 protected static BigInteger ppcm(BigInteger a, BigInteger b) {
335 return a.divide(a.gcd(b)).multiply(b);
336 }
337
338
339
340
341
342
343
344 public void rescaleBy(double d) {
345 this.activity *= d;
346 }
347
348 void selectionSort(int from, int to) {
349 int i, j, best_i;
350 long tmp;
351 int tmp2;
352
353 for (i = from; i < to - 1; i++) {
354 best_i = i;
355 for (j = i + 1; j < to; j++) {
356 if (this.coefs[j] > this.coefs[best_i]
357 || this.coefs[j] == this.coefs[best_i]
358 && this.lits[j] > this.lits[best_i]) {
359 best_i = j;
360 }
361 }
362 tmp = this.coefs[i];
363 this.coefs[i] = this.coefs[best_i];
364 this.coefs[best_i] = tmp;
365 tmp2 = this.lits[i];
366 this.lits[i] = this.lits[best_i];
367 this.lits[best_i] = tmp2;
368 }
369 }
370
371
372
373
374 public void setLearnt() {
375 this.learnt = true;
376 }
377
378
379
380
381
382
383 public boolean simplify() {
384 long cumul = 0;
385
386 int i = 0;
387 while (i < this.lits.length && cumul < this.degree) {
388 if (this.voc.isSatisfied(this.lits[i])) {
389
390 cumul = cumul + this.coefs[i];
391 }
392 i++;
393 }
394
395 return cumul >= this.degree;
396 }
397
398 public final int size() {
399 return this.lits.length;
400 }
401
402
403
404
405 final protected void sort() {
406 assert this.lits != null;
407 if (this.coefs.length > 0) {
408 this.sort(0, size());
409 long buffInt = this.coefs[0];
410 for (int i = 1; i < this.coefs.length; i++) {
411 assert buffInt >= this.coefs[i];
412 buffInt = this.coefs[i];
413 }
414 }
415 }
416
417
418
419
420
421
422
423
424
425 final protected void sort(int from, int to) {
426 int width = to - from;
427 if (width <= 15) {
428 selectionSort(from, to);
429 } else {
430 int indPivot = width / 2 + from;
431 long pivot = this.coefs[indPivot];
432 int litPivot = this.lits[indPivot];
433 long tmp;
434 int i = from - 1;
435 int j = to;
436 int tmp2;
437
438 for (;;) {
439 do {
440 i++;
441 } while (this.coefs[i] > pivot || this.coefs[i] == pivot
442 && this.lits[i] > litPivot);
443 do {
444 j--;
445 } while (pivot > this.coefs[j] || this.coefs[j] == pivot
446 && this.lits[j] < litPivot);
447
448 if (i >= j) {
449 break;
450 }
451
452 tmp = this.coefs[i];
453 this.coefs[i] = this.coefs[j];
454 this.coefs[j] = tmp;
455 tmp2 = this.lits[i];
456 this.lits[i] = this.lits[j];
457 this.lits[j] = tmp2;
458 }
459
460 sort(from, i);
461 sort(i, to);
462 }
463
464 }
465
466 @Override
467 public String toString() {
468 StringBuffer stb = new StringBuffer();
469
470 if (this.lits.length > 0) {
471 for (int i = 0; i < this.lits.length; i++) {
472
473 stb.append(" + ");
474 stb.append(this.coefs[i]);
475 stb.append(".");
476 stb.append(Lits.toString(this.lits[i]));
477 stb.append("[");
478 stb.append(this.voc.valueToString(this.lits[i]));
479 stb.append("@");
480 stb.append(this.voc.getLevel(this.lits[i]));
481 stb.append("]");
482 stb.append(" ");
483
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 }