View Javadoc

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