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