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