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