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.minisat.core.UnitPropagationListener;
41 import org.sat4j.specs.ContradictionException;
42 import org.sat4j.specs.IVecInt;
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 // TODO locked
256 return true;
257 }
258
259 /**
260 * Constructs a cardinality constraint with a minimal set of watched
261 * literals Permet la cr?ation de contrainte de cardinalit? ? observation
262 * minimale
263 *
264 * @param s
265 * tool for propagation
266 * @param voc
267 * vocalulary used by the constraint
268 * @param ps
269 * literals involved in the constraint
270 * @param moreThan
271 * sign of the constraint. Should be ATLEAST or ATMOST.
272 * @param degree
273 * degree of the constraint
274 * @return a new cardinality constraint, null if it is a tautology
275 * @throws ContradictionException
276 */
277 public static Constr minWatchCardNew(UnitPropagationListener s, ILits voc,
278 IVecInt ps, boolean moreThan, int degree)
279 throws ContradictionException {
280
281 int mydegree = degree + linearisation(voc, ps);
282
283 if (ps.size() < mydegree) {
284 throw new ContradictionException();
285 } else if (ps.size() == mydegree) {
286 for (int i = 0; i < ps.size(); i++) {
287 if (!s.enqueue(ps.get(i))) {
288 throw new ContradictionException();
289 }
290 }
291 return new UnitClauses(ps);
292 }
293
294 // La contrainte est maintenant cr??e
295 MinWatchCard retour = new MinWatchCard(voc, ps, moreThan, mydegree);
296
297 if (retour.degree <= 0) {
298 return null;
299 }
300
301 retour.computeWatches();
302
303 retour.computePropagation(s);
304
305 return retour;
306 }
307
308 /**
309 * normalize the constraint (cf. P.Barth normalization)
310 */
311 public final void normalize() {
312 // Gestion du signe
313 if (!this.moreThan) {
314 // On multiplie le degr? par -1
315 this.degree = 0 - this.degree;
316 // On r?vise chaque litt?ral
317 for (int indLit = 0; indLit < this.lits.length; indLit++) {
318 this.lits[indLit] = this.lits[indLit] ^ 1;
319 this.degree++;
320 }
321 this.moreThan = true;
322 }
323 }
324
325 /**
326 * propagates the value of a falsified literal
327 *
328 * @param s
329 * tool for literal propagation
330 * @param p
331 * falsified literal
332 * @return false if an inconistency is detected, else true
333 */
334 public boolean propagate(UnitPropagationListener s, int p) {
335
336 // Si la contrainte est responsable de propagation unitaire
337 if (this.watchCumul == this.degree) {
338 this.voc.watch(p, this);
339 return false;
340 }
341
342 // Recherche du litt?ral falsifi?
343 int indFalsified = 0;
344 while ((this.lits[indFalsified] ^ 1) != p) {
345 indFalsified++;
346 }
347 assert this.watchCumul > this.degree;
348
349 // Recherche du litt?ral swap
350 int indSwap = this.degree + 1;
351 while (indSwap < this.lits.length
352 && this.voc.isFalsified(this.lits[indSwap])) {
353 indSwap++;
354 }
355
356 // Mise ? jour de la contrainte
357 if (indSwap == this.lits.length) {
358 // Si aucun litt?ral n'a ?t? trouv?
359 this.voc.watch(p, this);
360 // La limite est atteinte
361 this.watchCumul--;
362 assert this.watchCumul == this.degree;
363 this.voc.undos(p).push(this);
364
365 // On met en queue les litt?raux impliqu?s
366 for (int i = 0; i <= this.degree; i++) {
367 if (p != (this.lits[i] ^ 1) && !s.enqueue(this.lits[i], this)) {
368 return false;
369 }
370 }
371
372 return true;
373 }
374 // Si un litt?ral a ?t? trouv? on les ?change
375 int tmpInt = this.lits[indSwap];
376 this.lits[indSwap] = this.lits[indFalsified];
377 this.lits[indFalsified] = tmpInt;
378
379 // On observe le nouveau litt?ral
380 this.voc.watch(tmpInt ^ 1, this);
381
382 return true;
383 }
384
385 /**
386 * Removes a constraint from the solver
387 *
388 * @since 2.1
389 */
390 public void remove(UnitPropagationListener upl) {
391 for (int i = 0; i < Math.min(this.degree + 1, this.lits.length); i++) {
392 this.voc.watches(this.lits[i] ^ 1).remove(this);
393 }
394 }
395
396 /**
397 * Rescales the activity value of the constraint
398 *
399 * @param d
400 * rescale factor
401 */
402 public void rescaleBy(double d) {
403 // TODO rescaleBy
404 }
405
406 /**
407 * simplifies the constraint
408 *
409 * @return true if the constraint is satisfied, else false
410 */
411 public boolean simplify() {
412 // Calcul de la valeur actuelle
413 for (int i = 0, count = 0; i < this.lits.length; i++) {
414 if (this.voc.isSatisfied(this.lits[i]) && ++count == this.degree) {
415 return true;
416 }
417 }
418
419 return false;
420 }
421
422 /**
423 * Returns a string representation of the constraint.
424 *
425 * @return representation of the constraint.
426 */
427 @Override
428 public String toString() {
429 StringBuffer stb = new StringBuffer();
430 stb.append("Card (" + this.lits.length + ") : ");
431 if (this.lits.length > 0) {
432 // if (voc.isUnassigned(lits[0])) {
433 stb.append(Lits.toString(this.lits[0]));
434 stb.append("[");
435 stb.append(this.voc.valueToString(this.lits[0]));
436 stb.append("@");
437 stb.append(this.voc.getLevel(this.lits[0]));
438 stb.append("]");
439 stb.append(" "); //$NON-NLS-1$
440 // }
441 for (int i = 1; i < this.lits.length; i++) {
442 // if (voc.isUnassigned(lits[i])) {
443 stb.append(" + "); //$NON-NLS-1$
444 stb.append(Lits.toString(this.lits[i]));
445 stb.append("[");
446 stb.append(this.voc.valueToString(this.lits[i]));
447 stb.append("@");
448 stb.append(this.voc.getLevel(this.lits[i]));
449 stb.append("]");
450 stb.append(" "); //$NON-NLS-1$
451 // }
452 }
453 stb.append(">= "); //$NON-NLS-1$
454 stb.append(this.degree);
455 }
456 return stb.toString();
457 }
458
459 /**
460 * Updates information on the constraint in case of a backtrack
461 *
462 * @param p
463 * unassigned literal
464 */
465 public void undo(int p) {
466 // Le litt?ral observ? et falsifi? devient non assign?
467 this.watchCumul++;
468 }
469
470 public void setLearnt() {
471 throw new UnsupportedOperationException();
472 }
473
474 public void register() {
475 throw new UnsupportedOperationException();
476 }
477
478 public int size() {
479 return this.lits.length;
480 }
481
482 public int get(int i) {
483 return this.lits[i];
484 }
485
486 public void assertConstraint(UnitPropagationListener s) {
487 throw new UnsupportedOperationException();
488 }
489
490 protected void computeWatches() {
491 int indSwap = this.lits.length;
492 int tmpInt;
493 for (int i = 0; i <= this.degree && i < indSwap; i++) {
494 while (this.voc.isFalsified(this.lits[i]) && --indSwap > i) {
495 tmpInt = this.lits[i];
496 this.lits[i] = this.lits[indSwap];
497 this.lits[indSwap] = tmpInt;
498 }
499
500 // Si le litteral est observable
501 if (!this.voc.isFalsified(this.lits[i])) {
502 this.watchCumul++;
503 this.voc.watch(this.lits[i] ^ 1, this);
504 }
505 }
506 if (learnt()) {
507 // chercher tous les litteraux a regarder
508 // par ordre de niveau decroissant
509 int free = 1;
510 while (this.watchCumul <= this.degree && free > 0) {
511 free = 0;
512 // regarder le litteral falsifie au plus bas niveau
513 int maxlevel = -1, maxi = -1;
514 for (int i = this.watchCumul; i < this.lits.length; i++) {
515 if (this.voc.isFalsified(this.lits[i])) {
516 free++;
517 int level = this.voc.getLevel(this.lits[i]);
518 if (level > maxlevel) {
519 maxi = i;
520 maxlevel = level;
521 }
522 }
523 }
524 if (free > 0) {
525 assert maxi >= 0;
526 this.voc.watch(this.lits[maxi] ^ 1, this);
527 tmpInt = this.lits[maxi];
528 this.lits[maxi] = this.lits[this.watchCumul];
529 this.lits[this.watchCumul] = tmpInt;
530 this.watchCumul++;
531 free--;
532 assert free >= 0;
533 }
534 }
535 assert this.lits.length == 1 || this.watchCumul > 1;
536 }
537
538 }
539
540 protected MinWatchCard computePropagation(UnitPropagationListener s)
541 throws ContradictionException {
542
543 // Si on a des litteraux impliques
544 if (this.watchCumul == this.degree) {
545 for (int i = 0; i < this.lits.length; i++) {
546 if (!s.enqueue(this.lits[i])) {
547 throw new ContradictionException();
548 }
549 }
550 return null;
551 }
552
553 // Si on n'observe pas suffisamment
554 if (this.watchCumul < this.degree) {
555 throw new ContradictionException();
556 }
557 return this;
558 }
559
560 public int[] getLits() {
561 int[] tmp = new int[size()];
562 System.arraycopy(this.lits, 0, tmp, 0, size());
563 return tmp;
564 }
565
566 public ILits getVocabulary() {
567 return this.voc;
568 }
569
570 @Override
571 public boolean equals(Object card) {
572 if (card == null) {
573 return false;
574 }
575 try {
576 MinWatchCard mcard = (MinWatchCard) card;
577 if (mcard.degree != this.degree) {
578 return false;
579 }
580 if (this.lits.length != mcard.lits.length) {
581 return false;
582 }
583 boolean ok;
584 for (int lit : this.lits) {
585 ok = false;
586 for (int lit2 : mcard.lits) {
587 if (lit == lit2) {
588 ok = true;
589 break;
590 }
591 }
592 if (!ok) {
593 return false;
594 }
595 }
596 return true;
597 } catch (ClassCastException e) {
598 return false;
599 }
600 }
601
602 @Override
603 public int hashCode() {
604 long sum = 0;
605 for (int p : this.lits) {
606 sum += p;
607 }
608 sum += this.degree;
609 return (int) sum / (this.lits.length + 1);
610 }
611
612 /**
613 * @since 2.1
614 */
615 public void forwardActivity(double claInc) {
616 // do nothing
617 }
618
619 public boolean canBePropagatedMultipleTimes() {
620 return true;
621 }
622
623 public Constr toConstraint() {
624 return this;
625 }
626 }