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