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