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