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