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.math.BigInteger;
31  
32  import org.sat4j.minisat.core.ILits;
33  import org.sat4j.minisat.core.UnitPropagationListener;
34  import org.sat4j.specs.ContradictionException;
35  
36  /**
37   * Data structure for pseudo-boolean constraint with watched literals.
38   * 
39   * All literals are watched. The sum of the literals satisfied or unvalued is
40   * always memorized, to detect conflict.
41   * 
42   * 
43   */
44  public class MinWatchPbLongCP extends WatchPbLongCP {
45  
46  	/**
47  	 * 
48  	 */
49  	private static final long serialVersionUID = 1L;
50  
51  	/**
52  	 * sum of the coefficients of the literals satisfied or unvalued
53  	 */
54  	protected long watchCumul = 0;
55  
56  	/**
57  	 * is the literal of index i watching the constraint ?
58  	 */
59  	protected boolean[] watched;
60  
61  	/**
62  	 * indexes of literals watching the constraint
63  	 */
64  	protected int[] watching;
65  
66  	/**
67  	 * number of literals watching the constraint.
68  	 * 
69  	 * This is the real size of the array watching
70  	 */
71  	protected int watchingCount = 0;
72  
73  	/**
74  	 * Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k
75  	 * 
76  	 * This constructor is called for learnt pseudo boolean constraints.
77  	 * 
78  	 * @param voc
79  	 *            all the possible variables (vocabulary)
80  	 * @param mpb
81  	 *            a mutable PB constraint
82  	 */
83  	protected MinWatchPbLongCP(ILits voc, IDataStructurePB mpb) {
84  
85  		super(mpb);
86  		this.voc = voc;
87  
88  		watching = new int[this.coefs.length];
89  		watched = new boolean[this.coefs.length];
90  		activity = 0;
91  		watchCumul = 0;
92  		watchingCount = 0;
93  
94  	}
95  
96  	/**
97  	 * Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
98  	 * 
99  	 * @param voc
100 	 *            all the possible variables (vocabulary)
101 	 * @param lits
102 	 *            literals of the constraint (x0,x1, ... xn)
103 	 * @param coefs
104 	 *            coefficients of the left side of the constraint (a0, a1, ...
105 	 *            an)
106 	 * @param degree
107 	 *            degree of the constraint (k)
108 	 */
109 	protected MinWatchPbLongCP(ILits voc, int[] lits, BigInteger[] coefs, // NOPMD
110 			BigInteger degree) {
111 
112 		super(lits, coefs, degree);
113 		this.voc = voc;
114 
115 		watching = new int[this.coefs.length];
116 		watched = new boolean[this.coefs.length];
117 		activity = 0;
118 		watchCumul = 0;
119 		watchingCount = 0;
120 
121 	}
122 
123 	/*
124 	 * This method initialize the watched literals.
125 	 * 
126 	 * This method is only called in the factory methods.
127 	 * 
128 	 * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
129 	 */
130 	@Override
131 	protected void computeWatches() throws ContradictionException {
132 		assert watchCumul == 0;
133 		assert watchingCount == 0;
134 		for (int i = 0; i < lits.length && (watchCumul - coefs[0]) < degree; i++) {
135 			if (!voc.isFalsified(lits[i])) {
136 				voc.watch(lits[i] ^ 1, this);
137 				watching[watchingCount++] = i;
138 				watched[i] = true;
139 				// update the initial value for watchCumul (poss)
140 				watchCumul = watchCumul + coefs[i];
141 			}
142 		}
143 
144 		if (learnt)
145 			watchMoreForLearntConstraint();
146 
147 		if (watchCumul < degree) {
148 			throw new ContradictionException("non satisfiable constraint");
149 		}
150 		assert nbOfWatched() == watchingCount;
151 	}
152 
153 	private void watchMoreForLearntConstraint() {
154 		// looking for literals to be watched,
155 		// ordered by decreasing level
156 		int free = 1;
157 		int maxlevel, maxi, level;
158 
159 		while ((watchCumul - coefs[0]) < degree && (free > 0)) {
160 			free = 0;
161 			// looking for the literal falsified
162 			// at the least (lowest ?) level
163 			maxlevel = -1;
164 			maxi = -1;
165 			for (int i = 0; i < lits.length; i++) {
166 				if (voc.isFalsified(lits[i]) && !watched[i]) {
167 					free++;
168 					level = voc.getLevel(lits[i]);
169 					if (level > maxlevel) {
170 						maxi = i;
171 						maxlevel = level;
172 					}
173 				}
174 			}
175 
176 			if (free > 0) {
177 				assert maxi >= 0;
178 				voc.watch(lits[maxi] ^ 1, this);
179 				watching[watchingCount++] = maxi;
180 				watched[maxi] = true;
181 				// update of the watchCumul value
182 				watchCumul = watchCumul + coefs[maxi];
183 				free--;
184 				assert free >= 0;
185 			}
186 		}
187 		assert lits.length == 1 || watchingCount > 1;
188 	}
189 
190 	/*
191 	 * This method propagates any possible value.
192 	 * 
193 	 * This method is only called in the factory methods.
194 	 * 
195 	 * @see
196 	 * org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat
197 	 * .UnitPropagationListener)
198 	 */
199 	@Override
200 	protected void computePropagation(UnitPropagationListener s)
201 			throws ContradictionException {
202 		// propagate any possible value
203 		int ind = 0;
204 		while (ind < lits.length
205 				&& (watchCumul - coefs[watching[ind]]) < degree) {
206 			if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) {
207 				throw new ContradictionException("non satisfiable constraint");
208 			}
209 			ind++;
210 		}
211 	}
212 
213 	/**
214 	 * build a pseudo boolean constraint. Coefficients are positive integers
215 	 * less than or equal to the degree (this is called a normalized
216 	 * constraint).
217 	 * 
218 	 * @param s
219 	 *            a unit propagation listener
220 	 * @param voc
221 	 *            the vocabulary
222 	 * @param lits
223 	 *            the literals
224 	 * @param coefs
225 	 *            the coefficients
226 	 * @param degree
227 	 *            the degree of the constraint to normalize.
228 	 * @return a new PB constraint or null if a trivial inconsistency is
229 	 *         detected.
230 	 */
231 	public static MinWatchPbLongCP normalizedMinWatchPbNew(
232 			UnitPropagationListener s, ILits voc, int[] lits,
233 			BigInteger[] coefs, BigInteger degree)
234 			throws ContradictionException {
235 		// Parameters must not be modified
236 		MinWatchPbLongCP outclause = new MinWatchPbLongCP(voc, lits, coefs,
237 				degree);
238 
239 		if (outclause.degree <= 0) {
240 			return null;
241 		}
242 
243 		outclause.computeWatches();
244 
245 		outclause.computePropagation(s);
246 
247 		return outclause;
248 
249 	}
250 
251 	/**
252 	 * Number of really watched literals. It should return the same value as
253 	 * watchingCount.
254 	 * 
255 	 * This method must only be called for assertions.
256 	 * 
257 	 * @return number of watched literals.
258 	 */
259 	protected int nbOfWatched() {
260 		int retour = 0;
261 		for (int ind = 0; ind < this.watched.length; ind++) {
262 			for (int i = 0; i < watchingCount; i++)
263 				if (watching[i] == ind)
264 					assert watched[ind];
265 			retour += (this.watched[ind]) ? 1 : 0;
266 		}
267 		return retour;
268 	}
269 
270 	/**
271 	 * Propagation of a falsified literal
272 	 * 
273 	 * @param s
274 	 *            the solver
275 	 * @param p
276 	 *            the propagated literal (it must be falsified)
277 	 * @return false iff there is a conflict
278 	 */
279 	public boolean propagate(UnitPropagationListener s, int p) {
280 		assert nbOfWatched() == watchingCount;
281 		assert watchingCount > 1;
282 
283 		// finding the index for p in the array of literals (pIndice)
284 		// and in the array of watching (pIndiceWatching)
285 		int pIndiceWatching = 0;
286 		while (pIndiceWatching < watchingCount
287 				&& (lits[watching[pIndiceWatching]] ^ 1) != p)
288 			pIndiceWatching++;
289 		int pIndice = watching[pIndiceWatching];
290 
291 		assert p == (lits[pIndice] ^ 1);
292 		assert watched[pIndice];
293 
294 		// the greatest coefficient of the watched literals is necessary
295 		// (pIndice excluded)
296 		long maxCoef = maximalCoefficient(pIndice);
297 
298 		// update watching and watched w.r.t. to the propagation of p
299 		// new literals will be watched, maxCoef could be changed
300 		maxCoef = updateWatched(maxCoef, pIndice);
301 
302 		long upWatchCumul = watchCumul - coefs[pIndice];
303 		assert nbOfWatched() == watchingCount;
304 
305 		// if a conflict has been detected, return false
306 		if (upWatchCumul < degree) {
307 			// conflit
308 			voc.watch(p, this);
309 			assert watched[pIndice];
310 			assert !isSatisfiable();
311 			return false;
312 		} else if (upWatchCumul < (degree + maxCoef)) {
313 			// some literals must be assigned to true and then propagated
314 			assert watchingCount != 0;
315 			long limit = upWatchCumul - degree;
316 			for (int i = 0; i < watchingCount; i++) {
317 				if (limit < coefs[watching[i]] && i != pIndiceWatching
318 						&& !voc.isSatisfied(lits[watching[i]])
319 						&& !s.enqueue(lits[watching[i]], this)) {
320 					voc.watch(p, this);
321 					assert !isSatisfiable();
322 					return false;
323 				}
324 			}
325 			// if the constraint is added to the undos of p (by propagation),
326 			// then p should be preserved.
327 			voc.undos(p).push(this);
328 		}
329 
330 		// else p is no more watched
331 		watched[pIndice] = false;
332 		watchCumul = upWatchCumul;
333 		watching[pIndiceWatching] = watching[--watchingCount];
334 
335 		assert watchingCount != 0;
336 		assert nbOfWatched() == watchingCount;
337 
338 		return true;
339 	}
340 
341 	/**
342 	 * Remove the constraint from the solver
343 	 */
344 	public void remove(UnitPropagationListener upl) {
345 		for (int i = 0; i < watchingCount; i++) {
346 			voc.watches(lits[watching[i]] ^ 1).remove(this);
347 			this.watched[this.watching[i]] = false;
348 		}
349 		watchingCount = 0;
350 		assert nbOfWatched() == watchingCount;
351 	}
352 
353 	/**
354 	 * this method is called during backtrack
355 	 * 
356 	 * @param p
357 	 *            un unassigned literal
358 	 */
359 	public void undo(int p) {
360 		voc.watch(p, this);
361 		int pIndice = 0;
362 		while ((lits[pIndice] ^ 1) != p)
363 			pIndice++;
364 
365 		assert pIndice < lits.length;
366 
367 		watchCumul = watchCumul + coefs[pIndice];
368 
369 		assert watchingCount == nbOfWatched();
370 
371 		watched[pIndice] = true;
372 		watching[watchingCount++] = pIndice;
373 
374 		assert watchingCount == nbOfWatched();
375 	}
376 
377 	/**
378 	 * build a pseudo boolean constraint from a specific data structure. For
379 	 * learnt constraints.
380 	 * 
381 	 * @param s
382 	 *            a unit propagation listener (usually the solver)
383 	 * @param mpb
384 	 *            data structure which contains literals of the constraint,
385 	 *            coefficients (a0, a1, ... an), and the degree of the
386 	 *            constraint (k). The constraint is a "more than" constraint.
387 	 * @return a new PB constraint or null if a trivial inconsistency is
388 	 *         detected.
389 	 */
390 	public static WatchPbLongCP normalizedWatchPbNew(ILits voc,
391 			IDataStructurePB mpb) {
392 		return new MinWatchPbLongCP(voc, mpb);
393 	}
394 
395 	/**
396 	 * the maximal coefficient for the watched literals
397 	 * 
398 	 * @param pIndice
399 	 *            propagated literal : its coefficient is excluded from the
400 	 *            search of the maximal coefficient
401 	 * @return the maximal coefficient for the watched literals
402 	 */
403 	protected long maximalCoefficient(int pIndice) {
404 		long maxCoef = 0;
405 		for (int i = 0; i < watchingCount; i++)
406 			if (coefs[watching[i]] > maxCoef && watching[i] != pIndice) {
407 				maxCoef = coefs[watching[i]];
408 			}
409 
410 		assert learnt || maxCoef != 0;
411 		// DLB assert maxCoef!=0;
412 		return maxCoef;
413 	}
414 
415 	/**
416 	 * update arrays watched and watching w.r.t. the propagation of a literal.
417 	 * 
418 	 * return the maximal coefficient of the watched literals (could have been
419 	 * changed).
420 	 * 
421 	 * @param mc
422 	 *            the current maximal coefficient of the watched literals
423 	 * @param pIndice
424 	 *            the literal propagated (falsified)
425 	 * @return the new maximal coefficient of the watched literals
426 	 */
427 	protected long updateWatched(long mc, int pIndice) {
428 		long maxCoef = mc;
429 		// if not all the literals are watched
430 		if (watchingCount < size()) {
431 			// the watchCumul sum will have to be updated
432 			long upWatchCumul = watchCumul - coefs[pIndice];
433 
434 			// we must obtain upWatchCumul such that
435 			// upWatchCumul = degree + maxCoef
436 			long degreePlusMaxCoef = degree + maxCoef; // dvh
437 			for (int ind = 0; ind < lits.length; ind++) {
438 				if (upWatchCumul >= degreePlusMaxCoef) {
439 					// nothing more to watch
440 					// note: logic negated to old version // dvh
441 					break;
442 				}
443 				// while upWatchCumul does not contain enough
444 				if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
445 					// watch one more
446 					upWatchCumul = upWatchCumul + coefs[ind];
447 					// update arrays watched and watching
448 					watched[ind] = true;
449 					assert watchingCount < size();
450 					watching[watchingCount++] = ind;
451 					voc.watch(lits[ind] ^ 1, this);
452 					// this new watched literal could change the maximal
453 					// coefficient
454 					if (coefs[ind] > maxCoef) {
455 						maxCoef = coefs[ind];
456 						degreePlusMaxCoef = degree + maxCoef; // update
457 						// that one
458 						// too
459 					}
460 				}
461 			}
462 			// update watchCumul
463 			watchCumul = upWatchCumul + coefs[pIndice];
464 		}
465 		return maxCoef;
466 	}
467 
468 }