1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25
26 package org.sat4j.minisat.constraints.card;
27
28 import java.io.Serializable;
29
30 import org.sat4j.minisat.constraints.cnf.Lits;
31 import org.sat4j.minisat.core.Constr;
32 import org.sat4j.minisat.core.ILits;
33 import org.sat4j.minisat.core.Undoable;
34 import org.sat4j.minisat.core.UnitPropagationListener;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IVecInt;
37
38 public class MinWatchCard implements Constr, Undoable, Serializable {
39
40 private static final long serialVersionUID = 1L;
41
42 public static final boolean ATLEAST = true;
43
44 public static final boolean ATMOST = false;
45
46 /**
47 * degree of the cardinality constraint
48 */
49 protected int degree;
50
51 /**
52 * literals involved in the constraint
53 */
54 private int[] lits;
55
56 /**
57 * contains the sign of the constraint : ATLEAT or ATMOST
58 */
59 private boolean moreThan;
60
61 /**
62 * contains the sum of the coefficients of the watched literals
63 */
64 protected int watchCumul;
65
66 /**
67 * Vocabulary of the constraint
68 */
69 private final ILits voc;
70
71 /**
72 * Constructs and normalizes a cardinality constraint. used by
73 * minWatchCardNew in the non-normalized case.
74 *
75 * @param voc
76 * vocabulary used by the constraint
77 * @param ps
78 * literals involved in the constraint
79 * @param moreThan
80 * should be ATLEAST or ATMOST;
81 * @param degree
82 * degree of the constraint
83 */
84 public MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
85 // On met en place les valeurs
86 this.voc = voc;
87 this.degree = degree;
88 this.moreThan = moreThan;
89
90 // On simplifie ps
91 int[] index = new int[voc.nVars() * 2 + 2];
92 for (int i = 0; i < index.length; i++)
93 index[i] = 0;
94 // On repertorie les litt?raux utiles
95 for (int i = 0; i < ps.size(); i++) {
96 if (index[ps.get(i) ^ 1] == 0) {
97 index[ps.get(i)]++;
98 } else {
99 index[ps.get(i) ^ 1]--;
100 }
101 }
102 // On supprime les litt?raux inutiles
103 int ind = 0;
104 while (ind < ps.size()) {
105 if (index[ps.get(ind)] > 0) {
106 index[ps.get(ind)]--;
107 ind++;
108 } else {
109 // ??
110 if ((ps.get(ind) & 1) != 0)
111 this.degree--;
112 ps.set(ind, ps.last());
113 ps.pop();
114 }
115 }
116
117 // On copie les litt?raux de la contrainte
118 lits = new int[ps.size()];
119 ps.moveTo(lits);
120
121 // On normalise la contrainte au sens de Barth
122 normalize();
123
124 }
125
126 /**
127 * Constructs and normalizes a cardinality constraint. used by
128 * MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case. <br />
129 * <strong>Should not be used if parameters are not already normalized</strong><br />
130 * This constraint is always an ATLEAST constraint.
131 *
132 * @param voc
133 * vocabulary used by the constraint
134 * @param ps
135 * literals involved in the constraint
136 * @param degree
137 * degree of the constraint
138 */
139 protected MinWatchCard(ILits voc, IVecInt ps, int degree) {
140 // On met en place les valeurs
141 this.voc = voc;
142 this.degree = degree;
143 this.moreThan = ATLEAST;
144
145 // On copie les litt?raux de la contrainte
146 lits = new int[ps.size()];
147 ps.moveTo(lits);
148
149 }
150
151 /**
152 * computes the reason for a literal
153 *
154 * @param p
155 * falsified literal (or Lit.UNDEFINED)
156 * @param outReason
157 * the reason to be computed. Vector of literals.
158 * @see Constr#calcReason(int p, IVecInt outReason)
159 */
160 public void calcReason(int p, IVecInt outReason) {
161 // TODO calcReason: v?rifier par rapport ? l'article
162 // Pour chaque litt?ral
163 for (int i = 0; i < lits.length; i++) {
164 // Si il est falsifi?
165 if (voc.isFalsified(lits[i])) {
166 // On ajoute sa n?gation au vecteur
167 outReason.push(lits[i] ^ 1);
168 }
169 }
170 }
171
172 /**
173 * Returns the activity of the constraint
174 *
175 * @return activity value of the constraint
176 * @see Constr#getActivity()
177 */
178 public double getActivity() {
179 // TODO getActivity
180 return 0;
181 }
182
183 /**
184 * Increments activity of the constraint
185 *
186 * @param claInc
187 * value to be added to the activity of the constraint
188 * @see Constr#incActivity(double claInc)
189 */
190 public void incActivity(double claInc) {
191 // TODO incActivity
192 }
193
194 /**
195 * Returns wether the constraint is learnt or not.
196 *
197 * @return false : a MinWatchCard cannot be learnt.
198 * @see Constr#learnt()
199 */
200 public boolean learnt() {
201 return false;
202 }
203
204 /**
205 * Simplifies the constraint w.r.t. the assignments of the literals
206 *
207 * @param voc
208 * vocabulary used
209 * @param ps
210 * literals involved
211 * @return value to be added to the degree. This value is less than or equal
212 * to 0.
213 */
214 protected static int linearisation(ILits voc, IVecInt ps) {
215 // Stockage de l'influence des modifications
216 int modif = 0;
217
218 for (int i = 0; i < ps.size();) {
219 // on verifie si le litteral est affecte
220 if (voc.isUnassigned(ps.get(i))) {
221 i++;
222 } else {
223 // Si le litteral est satisfait,
224 // ?a revient ? baisser le degr?
225 if (voc.isSatisfied(ps.get(i))) {
226 modif--;
227 }
228 // dans tous les cas, s'il est assign?,
229 // on enleve le ieme litteral
230 ps.set(i, ps.last());
231 ps.pop();
232 }
233 }
234
235 // DLB: inutile?
236 // ps.shrinkTo(nbElement);
237 assert modif <= 0;
238
239 return modif;
240 }
241
242 /**
243 * Returns if the constraint is the reason for a unit propagation.
244 *
245 * @return true
246 * @see Constr#locked()
247 */
248 public boolean locked() {
249 // TODO locked
250 return true;
251 }
252
253 /**
254 * Constructs a cardinality constraint with a minimal set of watched
255 * literals Permet la cr?ation de contrainte de cardinalit? ? observation
256 * minimale
257 *
258 * @param s
259 * tool for propagation
260 * @param voc
261 * vocalulary used by the constraint
262 * @param ps
263 * literals involved in the constraint
264 * @param moreThan
265 * sign of the constraint. Should be ATLEAST or ATMOST.
266 * @param degree
267 * degree of the constraint
268 * @return a new cardinality constraint, null if it is a tautology
269 * @throws ContradictionException
270 */
271 public static MinWatchCard minWatchCardNew(UnitPropagationListener s,
272 ILits voc, IVecInt ps, boolean moreThan, int degree)
273 throws ContradictionException {
274
275 int mydegree = degree + linearisation(voc, ps);
276
277 if (ps.size() == 0 && mydegree > 0) {
278 throw new ContradictionException();
279 } else if (ps.size() == mydegree || ps.size() <= 0) {
280 for (int i = 0; i < ps.size(); i++)
281 if (!s.enqueue(ps.get(i))) {
282 throw new ContradictionException();
283 }
284 return null;
285 }
286
287 // La contrainte est maintenant cr??e
288 MinWatchCard retour = new MinWatchCard(voc, ps, moreThan, mydegree);
289
290 if (retour.degree <= 0)
291 return null;
292
293 retour.computeWatches();
294
295 retour.computePropagation(s);
296
297 return retour;
298 }
299
300 /**
301 * normalize the constraint (cf. P.Barth normalization)
302 */
303 public final void normalize() {
304 // Gestion du signe
305 if (!moreThan) {
306 // On multiplie le degr? par -1
307 this.degree = 0 - this.degree;
308 // On r?vise chaque litt?ral
309 for (int indLit = 0; indLit < lits.length; indLit++) {
310 lits[indLit] = lits[indLit] ^ 1;
311 this.degree++;
312 }
313 this.moreThan = true;
314 }
315 }
316
317 /**
318 * propagates the value of a falsified literal
319 *
320 * @param s
321 * tool for literal propagation
322 * @param p
323 * falsified literal
324 * @return false if an inconistency is detected, else true
325 */
326 public boolean propagate(UnitPropagationListener s, int p) {
327
328 // Si la contrainte est responsable de propagation unitaire
329 if (watchCumul == degree) {
330 voc.watch(p, this);
331 return false;
332 }
333
334 // Recherche du litt?ral falsifi?
335 int indFalsified = 0;
336 while ((lits[indFalsified] ^ 1) != p)
337 indFalsified++;
338 assert watchCumul > degree;
339
340 // Recherche du litt?ral swap
341 int indSwap = degree + 1;
342 while (indSwap < lits.length && voc.isFalsified(lits[indSwap]))
343 indSwap++;
344
345 // Mise ? jour de la contrainte
346 if (indSwap == lits.length) {
347 // Si aucun litt?ral n'a ?t? trouv?
348 voc.watch(p, this);
349 // La limite est atteinte
350 watchCumul--;
351 assert watchCumul == degree;
352 voc.undos(p).push(this);
353
354 // On met en queue les litt?raux impliqu?s
355 for (int i = 0; i <= degree; i++)
356 if ((p != (lits[i] ^ 1)) && !s.enqueue(lits[i], this))
357 return false;
358
359 return true;
360 }
361 // Si un litt?ral a ?t? trouv? on les ?change
362 int tmpInt = lits[indSwap];
363 lits[indSwap] = lits[indFalsified];
364 lits[indFalsified] = tmpInt;
365
366 // On observe le nouveau litt?ral
367 voc.watch(tmpInt ^ 1, this);
368
369 return true;
370 }
371
372 /**
373 * Removes a constraint from the solver
374 */
375 public void remove() {
376 for (int i = 0; i <= degree; i++) {
377 voc.watches(lits[i] ^ 1).remove(this);
378 }
379 }
380
381 /**
382 * Rescales the activity value of the constraint
383 *
384 * @param d
385 * rescale factor
386 */
387 public void rescaleBy(double d) {
388 // TODO rescaleBy
389 }
390
391 /**
392 * simplifies the constraint
393 *
394 * @return true if the constraint is satisfied, else false
395 */
396 public boolean simplify() {
397 // Calcul de la valeur actuelle
398 for (int i = 0, count = 0; i < lits.length; i++)
399 if (voc.isSatisfied(lits[i]) && (++count == degree))
400 return true;
401
402 return false;
403 }
404
405 /**
406 * Returns a string representation of the constraint.
407 *
408 * @return representation of the constraint.
409 */
410 @Override
411 public String toString() {
412 StringBuffer stb = new StringBuffer();
413 stb.append("Card (" + lits.length + ") : ");
414 if (lits.length > 0) {
415 // if (voc.isUnassigned(lits[0])) {
416 stb.append(Lits.toString(this.lits[0]));
417 stb.append("[");
418 stb.append(voc.valueToString(lits[0]));
419 stb.append("@");
420 stb.append(voc.getLevel(lits[0]));
421 stb.append("]");
422 stb.append(" "); //$NON-NLS-1$
423 // }
424 for (int i = 1; i < lits.length; i++) {
425 // if (voc.isUnassigned(lits[i])) {
426 stb.append(" + "); //$NON-NLS-1$
427 stb.append(Lits.toString(this.lits[i]));
428 stb.append("[");
429 stb.append(voc.valueToString(lits[i]));
430 stb.append("@");
431 stb.append(voc.getLevel(lits[i]));
432 stb.append("]");
433 stb.append(" "); //$NON-NLS-1$
434 // }
435 }
436 stb.append(">= "); //$NON-NLS-1$
437 stb.append(this.degree);
438 }
439 return stb.toString();
440 }
441
442 /**
443 * Updates information on the constraint in case of a backtrack
444 *
445 * @param p
446 * unassigned literal
447 */
448 public void undo(int p) {
449 // Le litt?ral observ? et falsifi? devient non assign?
450 watchCumul++;
451 }
452
453 public void setLearnt() {
454 throw new UnsupportedOperationException();
455 }
456
457 public void register() {
458 throw new UnsupportedOperationException();
459 }
460
461 public int size() {
462 return lits.length;
463 }
464
465 public int get(int i) {
466 return lits[i];
467 }
468
469 public void assertConstraint(UnitPropagationListener s) {
470 throw new UnsupportedOperationException();
471 }
472
473 protected void computeWatches() {
474 int indSwap = lits.length;
475 int tmpInt;
476 for (int i = 0; i <= degree && i < indSwap; i++) {
477 while (voc.isFalsified(lits[i]) && --indSwap > i) {
478 tmpInt = lits[i];
479 lits[i] = lits[indSwap];
480 lits[indSwap] = tmpInt;
481 }
482
483 // Si le litteral est observable
484 if (!voc.isFalsified(lits[i])) {
485 watchCumul++;
486 voc.watch(lits[i] ^ 1, this);
487 }
488 }
489 if (learnt()) {
490 // chercher tous les litteraux a regarder
491 // par ordre de niveau decroissant
492 int free = 1;
493 while ((watchCumul <= degree) && (free > 0)) {
494 free = 0;
495 // regarder le litteral falsifie au plus bas niveau
496 int maxlevel = -1, maxi = -1;
497 for (int i = watchCumul; i < lits.length; i++) {
498 if (voc.isFalsified(lits[i])) {
499 free++;
500 int level = voc.getLevel(lits[i]);
501 if (level > maxlevel) {
502 maxi = i;
503 maxlevel = level;
504 }
505 }
506 }
507 if (free > 0) {
508 assert maxi >= 0;
509 voc.watch(lits[maxi] ^ 1, this);
510 tmpInt = lits[maxi];
511 lits[maxi] = lits[watchCumul];
512 lits[watchCumul] = tmpInt;
513 watchCumul++;
514 free--;
515 assert free >= 0;
516 }
517 }
518 assert lits.length == 1 || watchCumul > 1;
519 }
520
521 }
522
523 protected MinWatchCard computePropagation(UnitPropagationListener s)
524 throws ContradictionException {
525
526 // Si on a des litteraux impliques
527 if (watchCumul == degree) {
528 for (int i = 0; i < lits.length; i++)
529 if (!s.enqueue(lits[i])) {
530 throw new ContradictionException();
531 }
532 return null;
533 }
534
535 // Si on n'observe pas suffisamment
536 if (watchCumul < degree) {
537 throw new ContradictionException();
538 }
539 return this;
540 }
541
542 public int[] getLits() {
543 int[] tmp = new int[size()];
544 System.arraycopy(lits, 0, tmp, 0, size());
545 return tmp;
546 }
547
548 public ILits getVocabulary() {
549 return voc;
550 }
551 }