1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
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 pseudo boolean algorithms described in:
20 * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21 * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22 * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23 *
24 * and
25 * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
26 * Framework. Ph.D. Dissertation, University of Oregon.
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.ILits;
36 import org.sat4j.minisat.core.Undoable;
37 import org.sat4j.minisat.core.UnitPropagationListener;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.IVecInt;
40
41 public abstract class WatchPb implements PBConstr, Undoable, Serializable {
42
43 /**
44 *
45 */
46 private static final long serialVersionUID = 1L;
47
48 /**
49 * constant for the initial type of inequality less than or equal
50 */
51 public static final boolean ATMOST = false;
52
53 /**
54 * constant for the initial type of inequality more than or equal
55 */
56 public static final boolean ATLEAST = true;
57
58 /**
59 * constraint activity
60 */
61 protected double activity;
62
63 /**
64 * coefficients of the literals of the constraint
65 */
66 protected BigInteger[] coefs;
67
68 /**
69 * degree of the pseudo-boolean constraint
70 */
71 protected BigInteger degree;
72
73 /**
74 * literals of the constraint
75 */
76 protected int[] lits;
77
78 /**
79 * true if the constraint is a learned constraint
80 */
81 protected boolean learnt = false;
82
83 /**
84 * sum of the coefficients of the literals satisfied or unvalued
85 */
86 protected BigInteger watchCumul = BigInteger.ZERO;
87
88 /**
89 * constraint's vocabulary
90 */
91 protected ILits voc;
92
93 /**
94 * This constructor is only available for the serialization.
95 */
96 WatchPb() {
97 }
98
99 WatchPb(IDataStructurePB mpb) {
100 int size = mpb.size();
101 lits = new int[size];
102 this.coefs = new BigInteger[size];
103 mpb.buildConstraintFromMapPb(lits, coefs);
104
105 this.degree = mpb.getDegree();
106
107 // On peut trier suivant les coefficients
108 sort();
109 }
110
111 WatchPb(int[] lits, BigInteger[] coefs, BigInteger degree) {
112 this.lits = lits;
113 this.coefs = coefs;
114 this.degree = degree;
115 // On peut trier suivant les coefficients
116 sort();
117 }
118
119 /**
120 * This predicate tests wether the constraint is assertive at decision level
121 * dl
122 *
123 * @param dl
124 * @return true iff the constraint is assertive at decision level dl.
125 */
126 public boolean isAssertive(int dl) {
127 BigInteger slack = BigInteger.ZERO;
128 for (int i = 0; i < lits.length; i++) {
129 if ((coefs[i].signum() > 0)
130 && ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
131 slack = slack.add(coefs[i]);
132 }
133 slack = slack.subtract(degree);
134 if (slack.signum() < 0)
135 return false;
136 for (int i = 0; i < lits.length; i++) {
137 if ((coefs[i].signum() > 0)
138 && (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
139 && (slack.compareTo(coefs[i]) < 0)) {
140 return true;
141 }
142 }
143 return false;
144 }
145
146 /**
147 * compute the reason for the assignment of a literal
148 *
149 * @param p
150 * a falsified literal (or Lit.UNDEFINED)
151 * @param outReason
152 * list of falsified literals for which the negation is the
153 * reason of the assignment
154 * @see org.sat4j.minisat.core.Constr#calcReason(int, IVecInt)
155 */
156 public void calcReason(int p, IVecInt outReason) {
157 for (int q : lits) {
158 if (voc.isFalsified(q)) {
159 outReason.push(q ^ 1);
160 }
161 }
162 }
163
164 abstract protected void computeWatches() throws ContradictionException;
165
166 abstract protected void computePropagation(UnitPropagationListener s)
167 throws ContradictionException;
168
169 /**
170 * to obtain the i-th literal of the constraint
171 *
172 * @param i
173 * index of the literal
174 * @return the literal
175 */
176 public int get(int i) {
177 return lits[i];
178 }
179
180 /**
181 * to obtain the coefficient of the i-th literal of the constraint
182 *
183 * @param i
184 * index of the literal
185 * @return coefficient of the literal
186 */
187 public BigInteger getCoef(int i) {
188 return coefs[i];
189 }
190
191 /**
192 * to obtain the activity value of the constraint
193 *
194 * @return activity value of the constraint
195 * @see org.sat4j.minisat.core.Constr#getActivity()
196 */
197 public double getActivity() {
198 return activity;
199 }
200
201 /**
202 * increase activity value of the constraint
203 *
204 * @see org.sat4j.minisat.core.Constr#incActivity(double)
205 */
206 public void incActivity(double claInc) {
207 activity += claInc;
208 }
209
210 /**
211 * compute the slack of the current constraint slack = poss - degree of the
212 * constraint
213 *
214 * @return la marge
215 */
216 public BigInteger slackConstraint() {
217 return recalcLeftSide().subtract(this.degree);
218 }
219
220 /**
221 * compute the slack of a described constraint slack = poss - degree of the
222 * constraint
223 *
224 * @param theCoefs
225 * coefficients of the constraint
226 * @param theDegree
227 * degree of the constraint
228 * @return slack of the constraint
229 */
230 public BigInteger slackConstraint(BigInteger[] theCoefs, BigInteger theDegree) {
231 return recalcLeftSide(theCoefs).subtract(theDegree);
232 }
233
234 /**
235 * compute the sum of the coefficients of the satisfied or non-assigned
236 * literals of a described constraint (usually called poss)
237 *
238 * @param theCoefs
239 * coefficients of the constraint
240 * @return poss
241 */
242 public BigInteger recalcLeftSide(BigInteger[] theCoefs) {
243 BigInteger poss = BigInteger.ZERO;
244 // Pour chaque litteral
245 for (int i = 0; i < lits.length; i++)
246 if (!voc.isFalsified(lits[i])) {
247 assert theCoefs[i].signum() >= 0;
248 poss = poss.add(theCoefs[i]);
249 }
250 return poss;
251 }
252
253 /**
254 * compute the sum of the coefficients of the satisfied or non-assigned
255 * literals of the current constraint (usually called poss)
256 *
257 * @return poss
258 */
259 public BigInteger recalcLeftSide() {
260 return recalcLeftSide(this.coefs);
261 }
262
263 /**
264 * D?termine si la contrainte est toujours satisfiable
265 *
266 * @return la contrainte est encore satisfiable
267 */
268 protected boolean isSatisfiable() {
269 return recalcLeftSide().compareTo(degree) >= 0;
270 }
271
272 /**
273 * is the constraint a learnt constrainte ?
274 *
275 * @return true si la contrainte est apprise, false sinon
276 * @see org.sat4j.specs.IConstr#learnt()
277 */
278 public boolean learnt() {
279 return learnt;
280 }
281
282 /**
283 * The constraint is the reason of a unit propagation.
284 *
285 * @return true
286 */
287 public boolean locked() {
288 for (int p : lits) {
289 if (voc.getReason(p)==this) {
290 return true;
291 }
292 }
293 return false;
294 }
295
296 /**
297 * Permet le r??????chantillonage de l'activit??? de la contrainte
298 *
299 * @param d
300 * facteur d'ajustement
301 */
302 public void rescaleBy(double d) {
303 activity *= d;
304 }
305
306 void selectionSort(int from, int to) {
307 int i, j, best_i;
308 BigInteger tmp;
309 int tmp2;
310
311 for (i = from; i < to - 1; i++) {
312 best_i = i;
313 for (j = i + 1; j < to; j++) {
314 if ((coefs[j].compareTo(coefs[best_i]) > 0)
315 || ((coefs[j].equals(coefs[best_i])) && (lits[j] > lits[best_i])))
316 best_i = j;
317 }
318 tmp = coefs[i];
319 coefs[i] = coefs[best_i];
320 coefs[best_i] = tmp;
321 tmp2 = lits[i];
322 lits[i] = lits[best_i];
323 lits[best_i] = tmp2;
324 }
325 }
326
327 /**
328 * La contrainte est apprise
329 */
330 public void setLearnt() {
331 learnt = true;
332 }
333
334 /**
335 * Simplifie la contrainte(l'all???ge)
336 *
337 * @return true si la contrainte est satisfaite, false sinon
338 */
339 public boolean simplify() {
340 BigInteger cumul = BigInteger.ZERO;
341
342 int i = 0;
343 while (i < lits.length && cumul.compareTo(degree) < 0) {
344 if (voc.isSatisfied(lits[i])) {
345 // Mesure pessimiste
346 cumul = cumul.add(coefs[i]);
347 }
348 i++;
349 }
350
351 return (cumul.compareTo(degree) >= 0);
352 }
353
354 public int size() {
355 return lits.length;
356 }
357
358 /**
359 * sort coefficient and literal arrays
360 */
361 final protected void sort() {
362 assert this.lits != null;
363 if (coefs.length > 0) {
364 this.sort(0, size());
365 BigInteger buffInt = coefs[0];
366 for (int i = 1; i < coefs.length; i++) {
367 assert buffInt.compareTo(coefs[i]) >= 0;
368 buffInt = coefs[i];
369 }
370
371 }
372 }
373
374 /**
375 * sort partially coefficient and literal arrays
376 *
377 * @param from
378 * index for the beginning of the sort
379 * @param to
380 * index for the end of the sort
381 */
382 final protected void sort(int from, int to) {
383 int width = to - from;
384 if (width <= 15)
385 selectionSort(from, to);
386
387 else {
388 int indPivot = width/2 + from;
389 BigInteger pivot = coefs[indPivot];
390 int litPivot = lits[indPivot];
391 BigInteger tmp;
392 int i = from - 1;
393 int j = to;
394 int tmp2;
395
396 for (;;) {
397 do
398 i++;
399 while ((coefs[i].compareTo(pivot) > 0)
400 || ((coefs[i].equals(pivot)) && (lits[i] > litPivot)));
401 do
402 j--;
403 while ((pivot.compareTo(coefs[j]) > 0)
404 || ((coefs[j].equals(pivot)) && (lits[j] < litPivot)));
405
406 if (i >= j)
407 break;
408
409 tmp = coefs[i];
410 coefs[i] = coefs[j];
411 coefs[j] = tmp;
412 tmp2 = lits[i];
413 lits[i] = lits[j];
414 lits[j] = tmp2;
415 }
416
417 sort(from, i);
418 sort(i, to);
419 }
420
421 }
422
423 @Override
424 public String toString() {
425 StringBuffer stb = new StringBuffer();
426
427 if (lits.length > 0) {
428 for (int i = 0; i < lits.length; i++) {
429 // if (voc.isUnassigned(lits[i])) {
430 stb.append(" + ");
431 stb.append(this.coefs[i]);
432 stb.append(".");
433 stb.append(Lits.toString(this.lits[i]));
434 stb.append("[");
435 stb.append(voc.valueToString(lits[i]));
436 stb.append("@");
437 stb.append(voc.getLevel(lits[i]));
438 stb.append("]");
439 stb.append(" ");
440 // }
441 }
442 stb.append(">= ");
443 stb.append(this.degree);
444 }
445 return stb.toString();
446 }
447
448 public void assertConstraint(UnitPropagationListener s) {
449 BigInteger tmp = slackConstraint();
450 for (int i = 0; i < lits.length; i++) {
451 if (voc.isUnassigned(lits[i]) && tmp.compareTo(coefs[i]) < 0) {
452 boolean ret = s.enqueue(lits[i], this);
453 assert ret;
454 }
455 }
456 }
457
458 // protected abstract WatchPb watchPbNew(Lits voc, VecInt lits, VecInt
459 // coefs, boolean moreThan, int degree, int[] indexer);
460 /**
461 * @return Returns the degree.
462 */
463 public BigInteger getDegree() {
464 return degree;
465 }
466
467 public void register() {
468 assert learnt;
469 try {
470 computeWatches();
471 } catch (ContradictionException e) {
472 System.out.println(this);
473 assert false;
474 }
475 }
476
477 public BigInteger[] getCoefs() {
478 BigInteger[] coefsBis = new BigInteger[coefs.length];
479 System.arraycopy(coefs, 0, coefsBis, 0, coefs.length);
480 return coefsBis;
481 }
482
483 public int[] getLits() {
484 int[] litsBis = new int[lits.length];
485 System.arraycopy(lits, 0, litsBis, 0, lits.length);
486 return litsBis;
487 }
488
489 public ILits getVocabulary() {
490 return voc;
491 }
492
493 /**
494 * compute an implied clause on the literals with the greater coefficients
495 */
496 public IVecInt computeAnImpliedClause() {
497 BigInteger cptCoefs = BigInteger.ZERO;
498 int index = coefs.length;
499 while ((cptCoefs.compareTo(degree) > 0) && (index > 0)) {
500 cptCoefs = cptCoefs.add(coefs[--index]);
501 }
502 if (index > 0 && index < size() / 2) {
503 // System.out.println(this);
504 // System.out.println("index : "+index);
505 IVecInt literals = new VecInt(index);
506 for (int j = 0; j <= index; j++)
507 literals.push(lits[j]);
508 return literals;
509 }
510 return null;
511 }
512
513 public boolean coefficientsEqualToOne() {
514 return false;
515 }
516
517 @Override
518 public boolean equals(Object pb) {
519 if (pb==null) {
520 return false;
521 }
522 // this method should be simplified since now to constraints should have
523 // always
524 // their literals in the same order
525 try {
526
527 WatchPb wpb = (WatchPb) pb;
528 if (!degree.equals(wpb.degree) || coefs.length != wpb.coefs.length
529 || lits.length != wpb.lits.length) {
530 return false;
531 }
532 int lit;
533 boolean ok;
534 for (int ilit = 0; ilit < coefs.length; ilit++) {
535 lit = lits[ilit];
536 ok = false;
537 for (int ilit2 = 0; ilit2 < coefs.length; ilit2++)
538 if (wpb.lits[ilit2] == lit) {
539 if (!wpb.coefs[ilit2].equals(coefs[ilit])) {
540 return false;
541 }
542
543 ok = true;
544 break;
545
546 }
547 if (!ok) {
548 return false;
549 }
550 }
551 return true;
552 } catch (ClassCastException e) {
553 return false;
554 }
555 }
556
557 @Override
558 public int hashCode() {
559 long sum = 0;
560 for (int p : lits) {
561 sum += p;
562 }
563 return (int) sum / lits.length;
564 }
565 }