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