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