View Javadoc

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 }