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.math.BigInteger;
33
34 import org.sat4j.minisat.core.ILits;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.UnitPropagationListener;
37
38
39
40
41
42
43
44
45
46 public class MinWatchPbLong extends WatchPbLong {
47
48 private static final long serialVersionUID = 1L;
49
50
51
52
53 protected long watchCumul = 0;
54
55
56
57
58 protected boolean[] watched;
59
60
61
62
63 protected int[] watching;
64
65
66
67
68
69
70 protected int watchingCount = 0;
71
72
73
74
75
76
77
78
79
80
81
82 protected MinWatchPbLong(ILits voc, IDataStructurePB mpb) {
83
84 super(mpb);
85 this.voc = voc;
86
87 this.watching = new int[this.coefs.length];
88 this.watched = new boolean[this.coefs.length];
89 this.activity = 0;
90 this.watchCumul = 0;
91 this.watchingCount = 0;
92
93 }
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108 protected MinWatchPbLong(ILits voc, int[] lits, BigInteger[] coefs,
109 BigInteger degree, BigInteger sumCoefs) {
110
111 super(lits, coefs, degree, sumCoefs);
112 this.voc = voc;
113
114 this.watching = new int[this.coefs.length];
115 this.watched = new boolean[this.coefs.length];
116 this.activity = 0;
117 this.watchCumul = 0;
118 this.watchingCount = 0;
119
120 }
121
122
123
124
125
126
127
128
129 @Override
130 protected void computeWatches() throws ContradictionException {
131 assert this.watchCumul == 0;
132 assert this.watchingCount == 0;
133 for (int i = 0; i < this.lits.length
134 && this.watchCumul - this.coefs[0] < this.degree; i++) {
135 if (!this.voc.isFalsified(this.lits[i])) {
136 this.voc.watch(this.lits[i] ^ 1, this);
137 this.watching[this.watchingCount++] = i;
138 this.watched[i] = true;
139
140 this.watchCumul = this.watchCumul + this.coefs[i];
141 }
142 }
143
144 if (this.learnt) {
145 watchMoreForLearntConstraint();
146 }
147
148 if (this.watchCumul < this.degree) {
149 throw new ContradictionException("non satisfiable constraint");
150 }
151 assert nbOfWatched() == this.watchingCount;
152 }
153
154 private void watchMoreForLearntConstraint() {
155
156
157 int free = 1;
158 int maxlevel, maxi, level;
159
160 while (this.watchCumul - this.coefs[0] < this.degree && free > 0) {
161 free = 0;
162
163
164 maxlevel = -1;
165 maxi = -1;
166 for (int i = 0; i < this.lits.length; i++) {
167 if (this.voc.isFalsified(this.lits[i]) && !this.watched[i]) {
168 free++;
169 level = this.voc.getLevel(this.lits[i]);
170 if (level > maxlevel) {
171 maxi = i;
172 maxlevel = level;
173 }
174 }
175 }
176
177 if (free > 0) {
178 assert maxi >= 0;
179 this.voc.watch(this.lits[maxi] ^ 1, this);
180 this.watching[this.watchingCount++] = maxi;
181 this.watched[maxi] = true;
182
183 this.watchCumul = this.watchCumul + this.coefs[maxi];
184 free--;
185 assert free >= 0;
186 }
187 }
188 assert this.lits.length == 1 || this.watchingCount > 1;
189 }
190
191
192
193
194
195
196
197
198
199
200 @Override
201 protected void computePropagation(UnitPropagationListener s)
202 throws ContradictionException {
203
204 int ind = 0;
205 while (ind < this.lits.length
206 && this.watchCumul - this.coefs[this.watching[ind]] < this.degree) {
207 if (this.voc.isUnassigned(this.lits[ind])
208 && !s.enqueue(this.lits[ind], this)) {
209 throw new ContradictionException("non satisfiable constraint");
210 }
211 ind++;
212 }
213 }
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233 public static MinWatchPbLong normalizedMinWatchPbNew(
234 UnitPropagationListener s, ILits voc, int[] lits,
235 BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
236 throws ContradictionException {
237
238 MinWatchPbLong outclause = new MinWatchPbLong(voc, lits, coefs, degree,
239 sumCoefs);
240
241 if (outclause.degree <= 0) {
242 return null;
243 }
244
245 outclause.computeWatches();
246
247 outclause.computePropagation(s);
248
249 return outclause;
250
251 }
252
253
254
255
256
257
258
259
260
261 protected int nbOfWatched() {
262 int retour = 0;
263 for (int ind = 0; ind < this.watched.length; ind++) {
264 for (int i = 0; i < this.watchingCount; i++) {
265 if (this.watching[i] == ind) {
266 assert this.watched[ind];
267 }
268 }
269 retour += this.watched[ind] ? 1 : 0;
270 }
271 return retour;
272 }
273
274
275
276
277
278
279
280
281
282
283 @Override
284 public boolean propagate(UnitPropagationListener s, int p) {
285 assert nbOfWatched() == this.watchingCount;
286 assert this.watchingCount > 1;
287
288
289
290 int pIndiceWatching = 0;
291 while (pIndiceWatching < this.watchingCount
292 && (this.lits[this.watching[pIndiceWatching]] ^ 1) != p) {
293 pIndiceWatching++;
294 }
295 int pIndice = this.watching[pIndiceWatching];
296
297 assert p == (this.lits[pIndice] ^ 1);
298 assert this.watched[pIndice];
299
300
301
302 long maxCoef = maximalCoefficient(pIndice);
303
304
305
306 maxCoef = updateWatched(maxCoef, pIndice);
307
308 long upWatchCumul = this.watchCumul - this.coefs[pIndice];
309 assert nbOfWatched() == this.watchingCount;
310
311
312 if (upWatchCumul < this.degree) {
313
314 this.voc.watch(p, this);
315 assert this.watched[pIndice];
316 assert !isSatisfiable();
317 return false;
318 } else if (upWatchCumul < this.degree + maxCoef) {
319
320 assert this.watchingCount != 0;
321 long limit = upWatchCumul - this.degree;
322 for (int i = 0; i < this.watchingCount; i++) {
323 if (limit < this.coefs[this.watching[i]]
324 && i != pIndiceWatching
325 && !this.voc.isSatisfied(this.lits[this.watching[i]])
326 && !s.enqueue(this.lits[this.watching[i]], this)) {
327 this.voc.watch(p, this);
328 assert !isSatisfiable();
329 return false;
330 }
331 }
332
333
334 this.voc.undos(p).push(this);
335 }
336
337
338 this.watched[pIndice] = false;
339 this.watchCumul = upWatchCumul;
340 this.watching[pIndiceWatching] = this.watching[--this.watchingCount];
341
342 assert this.watchingCount != 0;
343 assert nbOfWatched() == this.watchingCount;
344
345 return true;
346 }
347
348
349
350
351 @Override
352 public void remove(UnitPropagationListener upl) {
353 for (int i = 0; i < this.watchingCount; i++) {
354 this.voc.watches(this.lits[this.watching[i]] ^ 1).remove(this);
355 this.watched[this.watching[i]] = false;
356 }
357 this.watchingCount = 0;
358 assert nbOfWatched() == this.watchingCount;
359 }
360
361
362
363
364
365
366
367 @Override
368 public void undo(int p) {
369 this.voc.watch(p, this);
370 int pIndice = 0;
371 while ((this.lits[pIndice] ^ 1) != p) {
372 pIndice++;
373 }
374
375 assert pIndice < this.lits.length;
376
377 this.watchCumul = this.watchCumul + this.coefs[pIndice];
378
379 assert this.watchingCount == nbOfWatched();
380
381 this.watched[pIndice] = true;
382 this.watching[this.watchingCount++] = pIndice;
383
384 assert this.watchingCount == nbOfWatched();
385 }
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400 public static WatchPbLong normalizedWatchPbNew(ILits voc,
401 IDataStructurePB mpb) {
402 return new MinWatchPbLong(voc, mpb);
403 }
404
405
406
407
408
409
410
411
412
413 protected long maximalCoefficient(int pIndice) {
414 long maxCoef = 0;
415 for (int i = 0; i < this.watchingCount; i++) {
416 if (this.coefs[this.watching[i]] > maxCoef
417 && this.watching[i] != pIndice) {
418 maxCoef = this.coefs[this.watching[i]];
419 }
420 }
421
422 assert this.learnt || maxCoef != 0;
423 return maxCoef;
424 }
425
426
427
428
429
430
431
432
433
434
435
436
437
438 protected long updateWatched(long mc, int pIndice) {
439 long maxCoef = mc;
440
441 if (this.watchingCount < size()) {
442
443 long upWatchCumul = this.watchCumul - this.coefs[pIndice];
444
445
446
447 long degreePlusMaxCoef = this.degree + maxCoef;
448 for (int ind = 0; ind < this.lits.length; ind++) {
449 if (upWatchCumul >= degreePlusMaxCoef) {
450
451
452 break;
453 }
454
455 if (!this.voc.isFalsified(this.lits[ind]) && !this.watched[ind]) {
456
457 upWatchCumul = upWatchCumul + this.coefs[ind];
458
459 this.watched[ind] = true;
460 assert this.watchingCount < size();
461 this.watching[this.watchingCount++] = ind;
462 this.voc.watch(this.lits[ind] ^ 1, this);
463
464
465 if (this.coefs[ind] > maxCoef) {
466 maxCoef = this.coefs[ind];
467 degreePlusMaxCoef = this.degree + maxCoef;
468 }
469 }
470 }
471
472 this.watchCumul = upWatchCumul + this.coefs[pIndice];
473 }
474 return maxCoef;
475 }
476
477 }