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