1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 * Contributors:
28 * CRIL - initial API and implementation
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.minisat.core.UnitPropagationListener;
36 import org.sat4j.specs.ContradictionException;
37
38 /**
39 * Data structure for pseudo-boolean constraint with watched literals.
40 *
41 * All literals are watched. The sum of the literals satisfied or unvalued is
42 * always memorized, to detect conflict.
43 *
44 *
45 */
46
47 public class MinWatchPbLongLimit extends WatchPbLong {
48 private static final long serialVersionUID = 1L;
49
50 /**
51 * sum of the coefficients of the literals satisfied or unvalued
52 */
53 protected long watchCumul = 0;
54
55 /**
56 * if watchCumul is at Long.MAX_VALUE, contains the complement to the sum of
57 * the coefficients of the literals satisfied or unvalued
58 */
59 protected long compWatchCumul = 0;
60
61 /**
62 * is the literal of index i watching the constraint ?
63 */
64 protected boolean[] watched;
65
66 /**
67 * indexes of literals watching the constraint
68 */
69 protected int[] watching;
70
71 /**
72 * number of literals watching the constraint.
73 *
74 * This is the real size of the array watching
75 */
76 protected int watchingCount = 0;
77
78 /**
79 * Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k
80 *
81 * This constructor is called for learnt pseudo boolean constraints.
82 *
83 * @param voc
84 * all the possible variables (vocabulary)
85 * @param mpb
86 * a mutable PB constraint
87 */
88 protected MinWatchPbLongLimit(ILits voc, IDataStructurePB mpb) {
89
90 super(mpb);
91 this.voc = voc;
92
93 this.watching = new int[this.coefs.length];
94 this.watched = new boolean[this.coefs.length];
95 this.activity = 0;
96 this.watchCumul = 0;
97 this.watchingCount = 0;
98
99 }
100
101 /**
102 * Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
103 *
104 * @param voc
105 * all the possible variables (vocabulary)
106 * @param lits
107 * literals of the constraint (x0,x1, ... xn)
108 * @param coefs
109 * coefficients of the left side of the constraint (a0, a1, ...
110 * an)
111 * @param degree
112 * degree of the constraint (k)
113 */
114 protected MinWatchPbLongLimit(ILits voc, int[] lits, BigInteger[] coefs, // NOPMD
115 BigInteger degree, BigInteger sumCoefs) {
116
117 super(lits, coefs, degree, sumCoefs);
118 this.voc = voc;
119
120 this.watching = new int[this.coefs.length];
121 this.watched = new boolean[this.coefs.length];
122 this.activity = 0;
123 this.watchCumul = 0;
124 this.watchingCount = 0;
125
126 }
127
128 /*
129 * This method initialize the watched literals.
130 *
131 * This method is only called in the factory methods.
132 *
133 * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
134 */
135 @Override
136 protected void computeWatches() throws ContradictionException {
137 assert this.watchCumul == 0;
138 assert this.watchingCount == 0;
139 for (int i = 0; i < this.lits.length
140 && watchCumulMinusValueIsLessThanDegree(this.coefs[0]); i++) {
141 if (!this.voc.isFalsified(this.lits[i])) {
142 this.voc.watch(this.lits[i] ^ 1, this);
143 this.watching[this.watchingCount++] = i;
144 this.watched[i] = true;
145 // update the initial value for watchCumul (poss)
146 addToWC(this.coefs[i]);
147 }
148 }
149
150 if (this.learnt) {
151 watchMoreForLearntConstraint();
152 }
153
154 if (this.watchCumul < this.degree) {
155 throw new ContradictionException("non satisfiable constraint");
156 }
157 assert nbOfWatched() == this.watchingCount;
158 }
159
160 private void watchMoreForLearntConstraint() {
161 // looking for literals to be watched,
162 // ordered by decreasing level
163 int free = 1;
164 int maxlevel, maxi, level;
165
166 while (watchCumulMinusValueIsLessThanDegree(this.coefs[0]) && free > 0) {
167 free = 0;
168 // looking for the literal falsified
169 // at the least (lowest ?) level
170 maxlevel = -1;
171 maxi = -1;
172 for (int i = 0; i < this.lits.length; i++) {
173 if (this.voc.isFalsified(this.lits[i]) && !this.watched[i]) {
174 free++;
175 level = this.voc.getLevel(this.lits[i]);
176 if (level > maxlevel) {
177 maxi = i;
178 maxlevel = level;
179 }
180 }
181 }
182
183 if (free > 0) {
184 assert maxi >= 0;
185 this.voc.watch(this.lits[maxi] ^ 1, this);
186 this.watching[this.watchingCount++] = maxi;
187 this.watched[maxi] = true;
188 // update of the watchCumul value
189 addToWC(this.coefs[maxi]);
190 free--;
191 assert free >= 0;
192 }
193 }
194 assert this.lits.length == 1 || this.watchingCount > 1;
195 }
196
197 /*
198 * This method propagates any possible value.
199 *
200 * This method is only called in the factory methods.
201 *
202 * @see
203 * org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat
204 * .UnitPropagationListener)
205 */
206 @Override
207 protected void computePropagation(UnitPropagationListener s)
208 throws ContradictionException {
209 // propagate any possible value
210 int ind = 0;
211 while (ind < this.lits.length
212 && watchCumulMinusValueIsLessThanDegree(this.coefs[this.watching[ind]])) {
213 // (watchCumul - coefs[watching[ind]]) < degree) {
214 if (this.voc.isUnassigned(this.lits[ind])
215 && !s.enqueue(this.lits[ind], this)) {
216 throw new ContradictionException("non satisfiable constraint");
217 }
218 ind++;
219 }
220 }
221
222 /**
223 * build a pseudo boolean constraint. Coefficients are positive integers
224 * less than or equal to the degree (this is called a normalized
225 * constraint).
226 *
227 * @param s
228 * a unit propagation listener
229 * @param voc
230 * the vocabulary
231 * @param lits
232 * the literals
233 * @param coefs
234 * the coefficients
235 * @param degree
236 * the degree of the constraint to normalize.
237 * @return a new PB constraint or null if a trivial inconsistency is
238 * detected.
239 */
240 public static MinWatchPbLongLimit normalizedMinWatchPbNew(
241 UnitPropagationListener s, ILits voc, int[] lits,
242 BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
243 throws ContradictionException {
244 // Parameters must not be modified
245 MinWatchPbLongLimit outclause = new MinWatchPbLongLimit(voc, lits,
246 coefs, degree, sumCoefs);
247
248 if (outclause.degree <= 0) {
249 return null;
250 }
251
252 outclause.computeWatches();
253
254 outclause.computePropagation(s);
255
256 return outclause;
257
258 }
259
260 /**
261 * Number of really watched literals. It should return the same value as
262 * watchingCount.
263 *
264 * This method must only be called for assertions.
265 *
266 * @return number of watched literals.
267 */
268 protected int nbOfWatched() {
269 int retour = 0;
270 for (int ind = 0; ind < this.watched.length; ind++) {
271 for (int i = 0; i < this.watchingCount; i++) {
272 if (this.watching[i] == ind) {
273 assert this.watched[ind];
274 }
275 }
276 retour += this.watched[ind] ? 1 : 0;
277 }
278 return retour;
279 }
280
281 /**
282 * Propagation of a falsified literal
283 *
284 * @param s
285 * the solver
286 * @param p
287 * the propagated literal (it must be falsified)
288 * @return false iff there is a conflict
289 */
290 @Override
291 public boolean propagate(UnitPropagationListener s, int p) {
292 assert nbOfWatched() == this.watchingCount;
293 assert this.watchingCount > 1;
294
295 // finding the index for p in the array of literals (pIndice)
296 // and in the array of watching (pIndiceWatching)
297 int pIndiceWatching = 0;
298 while (pIndiceWatching < this.watchingCount
299 && (this.lits[this.watching[pIndiceWatching]] ^ 1) != p) {
300 pIndiceWatching++;
301 }
302 int pIndice = this.watching[pIndiceWatching];
303
304 assert p == (this.lits[pIndice] ^ 1);
305 assert this.watched[pIndice];
306
307 // the greatest coefficient of the watched literals is necessary
308 // (pIndice excluded)
309 long maxCoef = maximalCoefficient(pIndice);
310
311 // update watching and watched w.r.t. to the propagation of p
312 // new literals will be watched, maxCoef could be changed
313 maxCoef = updateWatched(maxCoef, pIndice);
314
315 // long upWatchCumul = watchCumul - coefs[pIndice];
316 assert nbOfWatched() == this.watchingCount;
317
318 // if a conflict has been detected, return false
319 if (watchCumulMinusValueIsLessThanDegree(this.coefs[pIndice])) {
320 // if (watchCumul - coefs[pIndice] < degree) {
321 // conflit
322 this.voc.watch(p, this);
323 assert this.watched[pIndice];
324 assert !isSatisfiable();
325 return false;
326 } else {
327 assert Long.MAX_VALUE - this.coefs[pIndice] > maxCoef;
328 if (watchCumulMinusValueIsLessThanDegree(this.coefs[pIndice]
329 + maxCoef)) {
330 // some literals must be assigned to true and then propagated
331 assert this.watchingCount != 0;
332 // long limit = upWatchCumul - degree;
333 // A REVOIR A PARTIR D'ICI
334 for (int i = 0; i < this.watchingCount; i++) {
335 assert Long.MAX_VALUE - this.coefs[pIndice] > this.coefs[this.watching[i]];
336 // if (watchCumul - coefs[pIndice] - degree <
337 // coefs[watching[i]]
338 if (watchCumulMinusValueIsLessThanDegree(this.coefs[pIndice]
339 + this.coefs[this.watching[i]])
340 && i != pIndiceWatching
341 && !this.voc
342 .isSatisfied(this.lits[this.watching[i]])
343 && !s.enqueue(this.lits[this.watching[i]], this)) {
344 this.voc.watch(p, this);
345 assert !isSatisfiable();
346 return false;
347 }
348 }
349 }
350 // if the constraint is added to the undos of p (by propagation),
351 // then p should be preserved.
352 this.voc.undos(p).push(this);
353 }
354
355 // else p is no more watched
356 this.watched[pIndice] = false;
357 substractToWC(this.coefs[pIndice]);
358 this.watching[pIndiceWatching] = this.watching[--this.watchingCount];
359
360 assert this.watchingCount != 0;
361 assert nbOfWatched() == this.watchingCount;
362
363 return true;
364 }
365
366 /**
367 * Remove the constraint from the solver
368 */
369 @Override
370 public void remove(UnitPropagationListener upl) {
371 for (int i = 0; i < this.watchingCount; i++) {
372 this.voc.watches(this.lits[this.watching[i]] ^ 1).remove(this);
373 this.watched[this.watching[i]] = false;
374 }
375 this.watchingCount = 0;
376 assert nbOfWatched() == this.watchingCount;
377 int ind = 0;
378 while (ind < this.coefs.length
379 && watchCumulMinusValueIsLessThanDegree(this.coefs[ind])) {
380 // (watchCumul - coefs[ind]) < degree) {
381 upl.unset(this.lits[ind]);
382 ind++;
383 }
384 }
385
386 /**
387 * this method is called during backtrack
388 *
389 * @param p
390 * un unassigned literal
391 */
392 @Override
393 public void undo(int p) {
394 this.voc.watch(p, this);
395 int pIndice = 0;
396 while ((this.lits[pIndice] ^ 1) != p) {
397 pIndice++;
398 }
399
400 assert pIndice < this.lits.length;
401
402 // watchCumul = watchCumul + coefs[pIndice];
403 addToWC(this.coefs[pIndice]);
404
405 assert this.watchingCount == nbOfWatched();
406
407 this.watched[pIndice] = true;
408 this.watching[this.watchingCount++] = pIndice;
409
410 assert this.watchingCount == nbOfWatched();
411 }
412
413 /**
414 * build a pseudo boolean constraint from a specific data structure. For
415 * learnt constraints.
416 *
417 * @param s
418 * a unit propagation listener (usually the solver)
419 * @param mpb
420 * data structure which contains literals of the constraint,
421 * coefficients (a0, a1, ... an), and the degree of the
422 * constraint (k). The constraint is a "more than" constraint.
423 * @return a new PB constraint or null if a trivial inconsistency is
424 * detected.
425 */
426 public static WatchPbLong normalizedWatchPbNew(ILits voc,
427 IDataStructurePB mpb) {
428 return new MinWatchPbLong(voc, mpb);
429 }
430
431 /**
432 * the maximal coefficient for the watched literals
433 *
434 * @param pIndice
435 * propagated literal : its coefficient is excluded from the
436 * search of the maximal coefficient
437 * @return the maximal coefficient for the watched literals
438 */
439 protected long maximalCoefficient(int pIndice) {
440 long maxCoef = 0;
441 for (int i = 0; i < this.watchingCount; i++) {
442 if (this.coefs[this.watching[i]] > maxCoef
443 && this.watching[i] != pIndice) {
444 maxCoef = this.coefs[this.watching[i]];
445 }
446 }
447
448 assert this.learnt || maxCoef != 0;
449 // DLB assert maxCoef!=0;
450 return maxCoef;
451 }
452
453 /**
454 * update arrays watched and watching w.r.t. the propagation of a literal.
455 *
456 * return the maximal coefficient of the watched literals (could have been
457 * changed).
458 *
459 * @param mc
460 * the current maximal coefficient of the watched literals
461 * @param pIndice
462 * the literal propagated (falsified)
463 * @return the new maximal coefficient of the watched literals
464 */
465 protected long updateWatched(long mc, int pIndice) {
466 long maxCoef = mc;
467 // if not all the literals are watched
468 if (this.watchingCount < size()) {
469 // the watchCumul sum will have to be updated
470 // long upWatchCumul = watchCumul - coefs[pIndice];
471 long upWatchCumul = 0;
472 long compUpWatchCumul = 0;
473 if (this.compWatchCumul > 0) {
474 assert this.watchCumul == Long.MAX_VALUE;
475 compUpWatchCumul = this.compWatchCumul - this.coefs[pIndice];
476 if (compUpWatchCumul < 0) {
477 upWatchCumul = Long.MAX_VALUE - compUpWatchCumul;
478 compUpWatchCumul = 0;
479 }
480 } else {
481 upWatchCumul = this.watchCumul - this.coefs[pIndice];
482 }
483 // we must obtain upWatchCumul such that
484 // upWatchCumul = degree + maxCoef
485 // long degreePlusMaxCoef = degree + maxCoef; // dvh
486 long degreePlusMaxCoef = 0;
487 long compDegreePlusMaxCoef = 0;
488 if (Long.MAX_VALUE - this.degree < maxCoef) {
489 degreePlusMaxCoef = Long.MAX_VALUE;
490 compDegreePlusMaxCoef = maxCoef
491 - (Long.MAX_VALUE - this.degree);
492 } else {
493 degreePlusMaxCoef = this.degree + maxCoef;
494 }
495 for (int ind = 0; ind < this.lits.length; ind++) {
496 // if (upWatchCumul >= degreePlusMaxCoef) {
497 if (compUpWatchCumul == 0 && compDegreePlusMaxCoef == 0
498 && upWatchCumul >= degreePlusMaxCoef
499 || compUpWatchCumul > compDegreePlusMaxCoef
500 || compUpWatchCumul == compDegreePlusMaxCoef
501 && upWatchCumul == degreePlusMaxCoef) {
502 // nothing more to watch
503 // note: logic negated to old version // dvh
504 break;
505 }
506 // while upWatchCumul does not contain enough
507 if (!this.voc.isFalsified(this.lits[ind]) && !this.watched[ind]) {
508 // watch one more
509 // upWatchCumul = upWatchCumul + coefs[ind];
510 if (Long.MAX_VALUE - this.coefs[ind] >= upWatchCumul) {
511 upWatchCumul = upWatchCumul + this.coefs[ind];
512 } else {
513 compUpWatchCumul = this.coefs[ind]
514 - (Long.MAX_VALUE - upWatchCumul);
515 upWatchCumul = Long.MAX_VALUE;
516 }
517
518 // update arrays watched and watching
519 this.watched[ind] = true;
520 assert this.watchingCount < size();
521 this.watching[this.watchingCount++] = ind;
522 this.voc.watch(this.lits[ind] ^ 1, this);
523 // this new watched literal could change the maximal
524 // coefficient
525 if (this.coefs[ind] > maxCoef) {
526 maxCoef = this.coefs[ind];
527 // degreePlusMaxCoef = degree + maxCoef; // update
528 compDegreePlusMaxCoef = 0;
529 if (Long.MAX_VALUE - this.degree < maxCoef) {
530 degreePlusMaxCoef = Long.MAX_VALUE;
531 compDegreePlusMaxCoef = maxCoef
532 - (Long.MAX_VALUE - this.degree);
533 } else {
534 degreePlusMaxCoef = this.degree + maxCoef;
535 // that one
536 // too
537 }
538 }
539 }
540 }
541 // update watchCumul
542 // watchCumul = upWatchCumul + coefs[pIndice];
543 this.watchCumul = upWatchCumul;
544 this.compWatchCumul = compUpWatchCumul;
545 addToWC(this.coefs[pIndice]);
546 }
547 return maxCoef;
548 }
549
550 private boolean watchCumulMinusValueIsLessThanDegree(long coef) {
551 return this.watchCumul - coef < this.degree
552 && this.watchCumul != Long.MAX_VALUE
553 || this.compWatchCumul - coef > 0
554 || this.watchCumul - coef + this.compWatchCumul < this.degree;
555 }
556
557 private void addToWC(long coef) {
558 if (Long.MAX_VALUE - coef >= this.watchCumul) {
559 this.watchCumul = this.watchCumul + coef;
560 } else {
561 this.compWatchCumul = coef - (Long.MAX_VALUE - this.watchCumul);
562 this.watchCumul = Long.MAX_VALUE;
563 }
564 }
565
566 private void substractToWC(long coef) {
567 if (this.compWatchCumul == 0) {
568 this.watchCumul = this.watchCumul - coef;
569 } else {
570 this.compWatchCumul = this.compWatchCumul - coef;
571 if (this.compWatchCumul < 0) {
572 this.watchCumul = this.watchCumul - this.compWatchCumul;
573 this.compWatchCumul = 0;
574 }
575 }
576 }
577
578 }