View Javadoc

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.pb.constraints.MaxLongWatchPBConstructor;
39  import org.sat4j.specs.ContradictionException;
40  import org.sat4j.specs.IVecInt;
41  
42  public abstract class WatchPbLongCP implements IWatchPb, Undoable, Serializable {
43  
44  	/**
45  	 * 
46  	 */
47  	private static final long serialVersionUID = 1L;
48  
49  	/**
50  	 * constraint activity
51  	 */
52  	protected double activity;
53  
54  	/**
55  	 * coefficients of the literals of the constraint
56  	 */
57  	protected BigInteger[] bigCoefs;
58  
59  	/**
60  	 * degree of the pseudo-boolean constraint
61  	 */
62  	protected BigInteger bigDegree;
63  
64  	/**
65  	 * coefficients of the literals of the constraint
66  	 */
67  	protected long[] coefs;
68  
69  	/**
70  	 * degree of the pseudo-boolean constraint
71  	 */
72  	protected long degree;
73  
74  	/**
75  	 * literals of the constraint
76  	 */
77  	protected int[] lits;
78  
79  	/**
80  	 * true if the constraint is a learned constraint
81  	 */
82  	protected boolean learnt = false;
83  
84  	/**
85  	 * constraint's vocabulary
86  	 */
87  	protected ILits voc;
88  
89  	/**
90  	 * This constructor is only available for the serialization.
91  	 */
92  	WatchPbLongCP() {
93  	}
94  
95  	WatchPbLongCP(IDataStructurePB mpb) {
96  		int size = mpb.size();
97  		lits = new int[size];
98  		bigCoefs = new BigInteger[size];
99  		mpb.buildConstraintFromMapPb(lits, bigCoefs);
100 		assert mpb.isLongSufficient();
101 		assert MaxLongWatchPBConstructor.isLongSufficient(bigCoefs,
102 				mpb.getDegree());
103 		coefs = toLong(bigCoefs);
104 
105 		this.bigDegree = mpb.getDegree();
106 		this.degree = bigDegree.longValue();
107 
108 		// arrays are sorted by decreasing coefficients
109 		sort();
110 	}
111 
112 	WatchPbLongCP(int[] lits, BigInteger[] coefs, BigInteger degree) { // NOPMD
113 		this.lits = lits;
114 		this.coefs = toLong(coefs);
115 		this.degree = degree.longValue();
116 		bigCoefs = coefs;
117 		bigDegree = degree;
118 		// arrays are sorted by decreasing coefficients
119 		sort();
120 	}
121 
122 	public static long[] toLong(BigInteger[] bigValues) {
123 		long[] res = new long[bigValues.length];
124 		for (int i = 0; i < res.length; i++) {
125 			assert bigValues[i].bitLength() < Long.SIZE;
126 			res[i] = bigValues[i].longValue();
127 			assert res[i] >= 0;
128 		}
129 		return res;
130 	}
131 
132 	/**
133 	 * This predicate tests wether the constraint is assertive at decision level
134 	 * dl
135 	 * 
136 	 * @param dl
137 	 * @return true iff the constraint is assertive at decision level dl.
138 	 */
139 	public boolean isAssertive(int dl) {
140 		long slack = 0;
141 		for (int i = 0; i < lits.length; i++) {
142 			if ((coefs[i] > 0)
143 					&& ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
144 				slack = slack + coefs[i];
145 		}
146 		slack = slack - degree;
147 		if (slack < 0)
148 			return false;
149 		for (int i = 0; i < lits.length; i++) {
150 			if ((coefs[i] > 0)
151 					&& (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
152 					&& (slack < coefs[i])) {
153 				return true;
154 			}
155 		}
156 		return false;
157 	}
158 
159 	/**
160 	 * compute the reason for the assignment of a literal
161 	 * 
162 	 * @param p
163 	 *            a falsified literal (or Lit.UNDEFINED)
164 	 * @param outReason
165 	 *            list of falsified literals for which the negation is the
166 	 *            reason of the assignment
167 	 * @see org.sat4j.minisat.core.Constr#calcReason(int, IVecInt)
168 	 */
169 	public void calcReason(int p, IVecInt outReason) {
170 		final int[] mlits = lits;
171 		for (int q : mlits) {
172 			if (voc.isFalsified(q)) {
173 				outReason.push(q ^ 1);
174 			}
175 		}
176 	}
177 
178 	abstract protected void computeWatches() throws ContradictionException;
179 
180 	abstract protected void computePropagation(UnitPropagationListener s)
181 			throws ContradictionException;
182 
183 	/**
184 	 * to obtain the i-th literal of the constraint
185 	 * 
186 	 * @param i
187 	 *            index of the literal
188 	 * @return the literal
189 	 */
190 	public int get(int i) {
191 		return lits[i];
192 	}
193 
194 	/**
195 	 * to obtain the activity value of the constraint
196 	 * 
197 	 * @return activity value of the constraint
198 	 * @see org.sat4j.minisat.core.Constr#getActivity()
199 	 */
200 	public double getActivity() {
201 		return activity;
202 	}
203 
204 	/**
205 	 * increase activity value of the constraint
206 	 * 
207 	 * @see org.sat4j.minisat.core.Constr#incActivity(double)
208 	 */
209 	public void incActivity(double claInc) {
210 		if (learnt) {
211 			activity += claInc;
212 		}
213 	}
214 
215 	/**
216 	 * compute the slack of the current constraint slack = poss - degree of the
217 	 * constraint
218 	 * 
219 	 * @return la marge
220 	 */
221 	public long slackConstraint() {
222 		return computeLeftSide() - this.degree;
223 	}
224 
225 	/**
226 	 * compute the slack of a described constraint slack = poss - degree of the
227 	 * constraint
228 	 * 
229 	 * @param theCoefs
230 	 *            coefficients of the constraint
231 	 * @param theDegree
232 	 *            degree of the constraint
233 	 * @return slack of the constraint
234 	 */
235 	public long slackConstraint(long[] theCoefs, long theDegree) {
236 		return computeLeftSide(theCoefs) - theDegree;
237 	}
238 
239 	/**
240 	 * compute the sum of the coefficients of the satisfied or non-assigned
241 	 * literals of a described constraint (usually called poss)
242 	 * 
243 	 * @param coefs
244 	 *            coefficients of the constraint
245 	 * @return poss
246 	 */
247 	public long computeLeftSide(long[] theCoefs) {
248 		long poss = 0;
249 		// for each literal
250 		for (int i = 0; i < lits.length; i++)
251 			if (!voc.isFalsified(lits[i])) {
252 				assert theCoefs[i] >= 0;
253 				poss = poss + theCoefs[i];
254 			}
255 		return poss;
256 	}
257 
258 	/**
259 	 * compute the sum of the coefficients of the satisfied or non-assigned
260 	 * literals of a described constraint (usually called poss)
261 	 * 
262 	 * @param coefs
263 	 *            coefficients of the constraint
264 	 * @return poss
265 	 */
266 	public BigInteger computeLeftSide(BigInteger[] theCoefs) {
267 		BigInteger poss = BigInteger.ZERO;
268 		// for each literal
269 		for (int i = 0; i < lits.length; i++)
270 			if (!voc.isFalsified(lits[i])) {
271 				assert theCoefs[i].signum() >= 0;
272 				poss = poss.add(theCoefs[i]);
273 			}
274 		return poss;
275 	}
276 
277 	/**
278 	 * compute the sum of the coefficients of the satisfied or non-assigned
279 	 * literals of the current constraint (usually called poss)
280 	 * 
281 	 * @return poss
282 	 */
283 	public long computeLeftSide() {
284 		return computeLeftSide(this.coefs);
285 	}
286 
287 	/**
288 	 * tests if the constraint is still satisfiable.
289 	 * 
290 	 * this method is only called in assertions.
291 	 * 
292 	 * @return the constraint is satisfiable
293 	 */
294 	protected boolean isSatisfiable() {
295 		return computeLeftSide() >= degree;
296 	}
297 
298 	/**
299 	 * is the constraint a learnt constraint ?
300 	 * 
301 	 * @return true if the constraint is learnt, else false
302 	 * @see org.sat4j.specs.IConstr#learnt()
303 	 */
304 	public boolean learnt() {
305 		return learnt;
306 	}
307 
308 	/**
309 	 * The constraint is the reason of a unit propagation.
310 	 * 
311 	 * @return true
312 	 */
313 	public boolean locked() {
314 		for (int p : lits) {
315 			if (voc.getReason(p) == this) {
316 				return true;
317 			}
318 		}
319 		return false;
320 	}
321 
322 	/**
323 	 * ppcm : least common multiple for two integers (plus petit commun
324 	 * multiple)
325 	 * 
326 	 * @param a
327 	 *            one integer
328 	 * @param b
329 	 *            the other integer
330 	 * @return the least common multiple of a and b
331 	 */
332 	protected static BigInteger ppcm(BigInteger a, BigInteger b) {
333 		return a.divide(a.gcd(b)).multiply(b);
334 	}
335 
336 	/**
337 	 * to re-scale the activity of the constraint
338 	 * 
339 	 * @param d
340 	 *            adjusting factor
341 	 */
342 	public void rescaleBy(double d) {
343 		activity *= d;
344 	}
345 
346 	void selectionSort(int from, int to) {
347 		int i, j, best_i;
348 		long tmp;
349 		BigInteger bigTmp;
350 		int tmp2;
351 
352 		for (i = from; i < to - 1; i++) {
353 			best_i = i;
354 			for (j = i + 1; j < to; j++) {
355 				if ((coefs[j] > coefs[best_i])
356 						|| ((coefs[j] == coefs[best_i]) && (lits[j] > lits[best_i])))
357 					best_i = j;
358 			}
359 			tmp = coefs[i];
360 			coefs[i] = coefs[best_i];
361 			coefs[best_i] = tmp;
362 			bigTmp = bigCoefs[i];
363 			bigCoefs[i] = bigCoefs[best_i];
364 			bigCoefs[best_i] = bigTmp;
365 			tmp2 = lits[i];
366 			lits[i] = lits[best_i];
367 			lits[best_i] = tmp2;
368 			assert coefs[i] >= 0;
369 			assert coefs[best_i] >= 0;
370 		}
371 	}
372 
373 	/**
374 	 * the constraint is learnt
375 	 */
376 	public void setLearnt() {
377 		learnt = true;
378 	}
379 
380 	/**
381 	 * simplify the constraint (if it is satisfied)
382 	 * 
383 	 * @return true if the constraint is satisfied, else false
384 	 */
385 	public boolean simplify() {
386 		long cumul = 0;
387 
388 		int i = 0;
389 		while (i < lits.length && cumul < degree) {
390 			if (voc.isSatisfied(lits[i])) {
391 				// strong measure
392 				cumul = cumul + coefs[i];
393 			}
394 			i++;
395 		}
396 
397 		return (cumul >= degree);
398 	}
399 
400 	public final int size() {
401 		return lits.length;
402 	}
403 
404 	/**
405 	 * sort coefficient and literal arrays
406 	 */
407 	final protected void sort() {
408 		assert this.lits != null;
409 		if (coefs.length > 0) {
410 			this.sort(0, size());
411 			// long buffInt = coefs[0];
412 			// for (int i = 1; i < coefs.length; i++) {
413 			// assert buffInt >= coefs[i];
414 			// buffInt = coefs[i];
415 			// }
416 
417 		}
418 	}
419 
420 	/**
421 	 * sort partially coefficient and literal arrays
422 	 * 
423 	 * @param from
424 	 *            index for the beginning of the sort
425 	 * @param to
426 	 *            index for the end of the sort
427 	 */
428 	final protected void sort(int from, int to) {
429 		int width = to - from;
430 		if (width <= 15)
431 			selectionSort(from, to);
432 
433 		else {
434 			assert coefs.length == bigCoefs.length;
435 			int indPivot = width / 2 + from;
436 			long pivot = coefs[indPivot];
437 			int litPivot = lits[indPivot];
438 			long tmp;
439 			BigInteger bigTmp;
440 			int i = from - 1;
441 			int j = to;
442 			int tmp2;
443 
444 			for (;;) {
445 				do
446 					i++;
447 				while ((coefs[i] > pivot)
448 						|| ((coefs[i] == pivot) && (lits[i] > litPivot)));
449 				do
450 					j--;
451 				while ((pivot > coefs[j])
452 						|| ((coefs[j] == pivot) && (lits[j] < litPivot)));
453 
454 				if (i >= j)
455 					break;
456 
457 				tmp = coefs[i];
458 				coefs[i] = coefs[j];
459 				coefs[j] = tmp;
460 				bigTmp = bigCoefs[i];
461 				bigCoefs[i] = bigCoefs[j];
462 				bigCoefs[j] = bigTmp;
463 				tmp2 = lits[i];
464 				lits[i] = lits[j];
465 				lits[j] = tmp2;
466 				assert coefs[i] >= 0;
467 				assert coefs[j] >= 0;
468 			}
469 
470 			sort(from, i);
471 			sort(i, to);
472 		}
473 
474 	}
475 
476 	@Override
477 	public String toString() {
478 		StringBuffer stb = new StringBuffer();
479 
480 		if (lits.length > 0) {
481 			for (int i = 0; i < lits.length; i++) {
482 				// if (voc.isUnassigned(lits[i])) {
483 				stb.append(" + ");
484 				stb.append(this.coefs[i]);
485 				stb.append(".");
486 				stb.append(Lits.toString(this.lits[i]));
487 				stb.append("[");
488 				stb.append(voc.valueToString(lits[i]));
489 				stb.append("@");
490 				stb.append(voc.getLevel(lits[i]));
491 				stb.append("]");
492 				stb.append(" ");
493 				// }
494 			}
495 			stb.append(">= ");
496 			stb.append(this.degree);
497 		}
498 		return stb.toString();
499 	}
500 
501 	public void assertConstraint(UnitPropagationListener s) {
502 		long tmp = slackConstraint();
503 		for (int i = 0; i < lits.length; i++) {
504 			if (voc.isUnassigned(lits[i]) && tmp < coefs[i]) {
505 				boolean ret = s.enqueue(lits[i], this);
506 				assert ret;
507 			}
508 		}
509 	}
510 
511 	public void register() {
512 		assert learnt;
513 		try {
514 			computeWatches();
515 		} catch (ContradictionException e) {
516 			System.out.println(this);
517 			assert false;
518 		}
519 	}
520 
521 	/**
522 	 * to obtain the literals of the constraint.
523 	 * 
524 	 * @return a copy of the array of the literals
525 	 */
526 	public int[] getLits() {
527 		int[] litsBis = new int[lits.length];
528 		System.arraycopy(lits, 0, litsBis, 0, lits.length);
529 		return litsBis;
530 	}
531 
532 	public ILits getVocabulary() {
533 		return voc;
534 	}
535 
536 	/**
537 	 * compute an implied clause on the literals with the greater coefficients.
538 	 * 
539 	 * @return a vector containing the literals for this clause.
540 	 */
541 	public IVecInt computeAnImpliedClause() {
542 		long cptCoefs = 0;
543 		int index = coefs.length;
544 		while ((cptCoefs > degree) && (index > 0)) {
545 			cptCoefs = cptCoefs + coefs[--index];
546 		}
547 		if (index > 0 && index < size() / 2) {
548 			IVecInt literals = new VecInt(index);
549 			for (int j = 0; j <= index; j++)
550 				literals.push(lits[j]);
551 			return literals;
552 		}
553 		return null;
554 	}
555 
556 	public boolean coefficientsEqualToOne() {
557 		return false;
558 	}
559 
560 	@Override
561 	public boolean equals(Object pb) {
562 		if (pb == null) {
563 			return false;
564 		}
565 		// this method should be simplified since now two constraints should
566 		// have
567 		// always
568 		// their literals in the same order
569 		try {
570 
571 			WatchPbLongCP wpb = (WatchPbLongCP) pb;
572 			if (degree != wpb.degree || coefs.length != wpb.coefs.length
573 					|| lits.length != wpb.lits.length) {
574 				return false;
575 			}
576 			int lit;
577 			boolean ok;
578 			for (int ilit = 0; ilit < coefs.length; ilit++) {
579 				lit = lits[ilit];
580 				ok = false;
581 				for (int ilit2 = 0; ilit2 < coefs.length; ilit2++)
582 					if (wpb.lits[ilit2] == lit) {
583 						if (wpb.coefs[ilit2] != coefs[ilit]) {
584 							return false;
585 						}
586 
587 						ok = true;
588 						break;
589 
590 					}
591 				if (!ok) {
592 					return false;
593 				}
594 			}
595 			return true;
596 		} catch (ClassCastException e) {
597 			return false;
598 		}
599 	}
600 
601 	@Override
602 	public int hashCode() {
603 		long sum = 0;
604 		for (int p : lits) {
605 			sum += p;
606 		}
607 		return (int) sum / lits.length;
608 	}
609 
610 	public void forwardActivity(double claInc) {
611 		if (!learnt) {
612 			activity += claInc;
613 		}
614 	}
615 
616 	public long[] getLongCoefs() {
617 		long[] coefsBis = new long[coefs.length];
618 		System.arraycopy(coefs, 0, coefsBis, 0, coefs.length);
619 		return coefsBis;
620 	}
621 
622 	public BigInteger slackConstraint(BigInteger[] theCoefs,
623 			BigInteger theDegree) {
624 		return computeLeftSide(theCoefs).subtract(theDegree);
625 	}
626 
627 	/**
628 	 * to obtain the coefficient of the i-th literal of the constraint
629 	 * 
630 	 * @param i
631 	 *            index of the literal
632 	 * @return coefficient of the literal
633 	 */
634 	public BigInteger getCoef(int i) {
635 		return bigCoefs[i];
636 	}
637 
638 	/**
639 	 * to obtain the coefficients of the constraint.
640 	 * 
641 	 * @return a copy of the array of the coefficients
642 	 */
643 	public BigInteger[] getCoefs() {
644 		BigInteger[] coefsBis = new BigInteger[coefs.length];
645 		System.arraycopy(bigCoefs, 0, coefsBis, 0, coefs.length);
646 		return coefsBis;
647 	}
648 
649 	/**
650 	 * @return Returns the degree.
651 	 */
652 	public BigInteger getDegree() {
653 		return bigDegree;
654 	}
655 
656 	public boolean canBePropagatedMultipleTimes() {
657 		return true;
658 	}
659 }