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  import java.math.BigInteger;
34  
35  import org.sat4j.minisat.constraints.cnf.Lits;
36  import org.sat4j.minisat.constraints.cnf.UnitClauses;
37  import org.sat4j.minisat.core.Constr;
38  import org.sat4j.minisat.core.ILits;
39  import org.sat4j.minisat.core.Propagatable;
40  import org.sat4j.minisat.core.Undoable;
41  import org.sat4j.minisat.core.UnitPropagationListener;
42  import org.sat4j.specs.ContradictionException;
43  import org.sat4j.specs.IVecInt;
44  
45  public final class MaxWatchCard implements Propagatable, Constr, Undoable,
46          Serializable {
47  
48      private static final long serialVersionUID = 1L;
49  
50      /**
51       * Degr? de la contrainte de cardinalit?
52       */
53      private int degree;
54  
55      /**
56       * Liste des litt?raux de la contrainte
57       */
58      private final int[] lits;
59  
60      /**
61       * D?termine si c'est une in?galit? sup?rieure ou ?gale
62       */
63      private boolean moreThan;
64  
65      /**
66       * Somme des coefficients des litt?raux observ?s
67       */
68      private int watchCumul;
69  
70      /**
71       * Vocabulaire de la contrainte
72       */
73      private final ILits voc;
74  
75      /**
76       * Constructeur de base cr?ant des contraintes vides
77       * 
78       * @param size
79       *            nombre de litt?raux de la contrainte
80       * @param learnt
81       *            indique si la contrainte est apprise
82       */
83      private MaxWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
84  
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          }
95          // On repertorie les litt?raux utiles
96          for (int i = 0; i < ps.size(); i++) {
97              if (index[ps.get(i) ^ 1] == 0) {
98                  index[ps.get(i)]++;
99              } else {
100                 index[ps.get(i) ^ 1]--;
101             }
102         }
103         // On supprime les litt?raux inutiles
104         int ind = 0;
105         while (ind < ps.size()) {
106             if (index[ps.get(ind)] > 0) {
107                 index[ps.get(ind)]--;
108                 ind++;
109             } else {
110                 if ((ps.get(ind) & 1) != 0) {
111                     this.degree--;
112                 }
113                 ps.set(ind, ps.last());
114                 ps.pop();
115             }
116         }
117 
118         // On copie les litt?raux de la contrainte
119         this.lits = new int[ps.size()];
120         ps.moveTo(this.lits);
121 
122         // On normalise la contrainte au sens de Barth
123         normalize();
124 
125         // Mise en place de l'observation maximale
126         this.watchCumul = 0;
127 
128         // On observe les litt?raux non falsifi?
129         for (int i = 0; i < this.lits.length; i++) {
130             // Rappel: les ?l?ments falsifi?s ne seront jamais d?pil?s
131             if (!voc.isFalsified(this.lits[i])) {
132                 this.watchCumul++;
133                 voc.watch(this.lits[i] ^ 1, this);
134             }
135         }
136     }
137 
138     /**
139      * Calcule la cause de l'affection d'un litt?ral
140      * 
141      * @param p
142      *            un litt?ral falsifi? (ou Lit.UNDEFINED)
143      * @param outReason
144      *            vecteur de litt?raux ? remplir
145      * @see Constr#calcReason(int p, IVecInt outReason)
146      */
147     public void calcReason(int p, IVecInt outReason) {
148         for (int lit : this.lits) {
149             if (this.voc.isFalsified(lit)) {
150                 outReason.push(lit ^ 1);
151             }
152         }
153     }
154 
155     /**
156      * Obtenir la valeur de l'activit? de la contrainte
157      * 
158      * @return la valeur de l'activit? de la contrainte
159      * @see Constr#getActivity()
160      */
161     public double getActivity() {
162         // TODO getActivity
163         return 0;
164     }
165 
166     /**
167      * Incr?mente la valeur de l'activit? de la contrainte
168      * 
169      * @param claInc
170      *            incr?ment de l'activit? de la contrainte
171      * @see Constr#incActivity(double claInc)
172      */
173     public void incActivity(double claInc) {
174         // TODO incActivity
175     }
176 
177     public void setActivity(double d) {
178     }
179 
180     /**
181      * D?termine si la contrainte est apprise
182      * 
183      * @return true si la contrainte est apprise, false sinon
184      * @see Constr#learnt()
185      */
186     public boolean learnt() {
187         // TODO learnt
188         return false;
189     }
190 
191     /**
192      * La contrainte est la cause d'une propagation unitaire
193      * 
194      * @return true si c'est le cas, false sinon
195      * @see Constr#locked()
196      */
197     public boolean locked() {
198         // TODO locked
199         return true;
200     }
201 
202     /**
203      * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
204      * 
205      * @param s
206      *            outil pour la propagation des litt?raux
207      * @param voc
208      *            vocabulaire utilis? par la contrainte
209      * @param ps
210      *            liste des litt?raux de la nouvelle contrainte
211      * @param moreThan
212      *            d?termine si c'est une sup?rieure ou ?gal ? l'origine
213      * @param degree
214      *            fournit le degr? de la contrainte
215      * @return une nouvelle clause si tout va bien, null sinon
216      * @throws ContradictionException
217      */
218     public static Constr maxWatchCardNew(UnitPropagationListener s, ILits voc,
219             IVecInt ps, boolean moreThan, int degree)
220             throws ContradictionException {
221 
222         MaxWatchCard outclause = null;
223 
224         // La contrainte ne doit pas ?tre vide
225         if (ps.size() < degree) {
226             throw new ContradictionException(
227                     "Creating trivially inconsistent constraint"); //$NON-NLS-1$
228         } else if (ps.size() == degree) {
229             for (int i = 0; i < ps.size(); i++) {
230                 if (!s.enqueue(ps.get(i))) {
231                     throw new ContradictionException(
232                             "Contradiction with implied literal"); //$NON-NLS-1$
233                 }
234             }
235             return new UnitClauses(ps);
236         }
237 
238         // On cree la contrainte
239         outclause = new MaxWatchCard(voc, ps, moreThan, degree);
240 
241         // Si le degr? est insufisant
242         if (outclause.degree <= 0) {
243             return null;
244         }
245 
246         // Si il n'y a aucune chance de satisfaire la contrainte
247         if (outclause.watchCumul < outclause.degree) {
248             throw new ContradictionException();
249         }
250 
251         // Si les litt?raux observ?s sont impliqu?s
252         if (outclause.watchCumul == outclause.degree) {
253             for (int i = 0; i < outclause.lits.length; i++) {
254                 if (!s.enqueue(outclause.lits[i])) {
255                     throw new ContradictionException(
256                             "Contradiction with implied literal"); //$NON-NLS-1$
257                 }
258             }
259             return null;
260         }
261 
262         return outclause;
263     }
264 
265     /**
266      * On normalise la contrainte au sens de Barth
267      */
268     public final void normalize() {
269         // Gestion du signe
270         if (!this.moreThan) {
271             // On multiplie le degr? par -1
272             this.degree = 0 - this.degree;
273             // On r?vise chaque litt?ral
274             for (int indLit = 0; indLit < this.lits.length; indLit++) {
275                 this.lits[indLit] = this.lits[indLit] ^ 1;
276                 this.degree++;
277             }
278             this.moreThan = true;
279         }
280     }
281 
282     /**
283      * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
284      * 
285      * @param s
286      *            objet utilis? pour la propagation
287      * @param p
288      *            le litt?ral propag? (il doit etre falsifie)
289      * @return false ssi une inconsistance est d?t?ct?e
290      */
291     public boolean propagate(UnitPropagationListener s, int p) {
292 
293         // On observe toujours tous les litt?raux
294         this.voc.watch(p, this);
295         assert !this.voc.isFalsified(p);
296 
297         // Si le litt?ral p est impliqu?
298         if (this.watchCumul == this.degree) {
299             return false;
300         }
301 
302         // On met en place la mise ? jour du compteur
303         this.voc.undos(p).push(this);
304         this.watchCumul--;
305 
306         // Si les litt?raux restant sont impliqu?s
307         if (this.watchCumul == this.degree) {
308             for (int q : this.lits) {
309                 if (this.voc.isUnassigned(q) && !s.enqueue(q, this)) {
310                     return false;
311                 }
312             }
313         }
314         return true;
315     }
316 
317     /**
318      * @since 2.1
319      */
320     public void remove(UnitPropagationListener upl) {
321         for (int q : this.lits) {
322             this.voc.watches(q ^ 1).remove(this);
323         }
324     }
325 
326     /**
327      * Permet le r??chantillonage de l'activit? de la contrainte
328      * 
329      * @param d
330      *            facteur d'ajustement
331      */
332     public void rescaleBy(double d) {
333     }
334 
335     /**
336      * Simplifie la contrainte(l'all?ge)
337      * 
338      * @return true si la contrainte est satisfaite, false sinon
339      */
340     public boolean simplify() {
341 
342         int i = 0;
343 
344         // On esp?re le maximum de la somme
345         int curr = this.watchCumul;
346 
347         // Pour chaque litt?ral
348         while (i < this.lits.length) {
349             // On d?cr?mente si l'espoir n'est pas fond?
350             if (this.voc.isUnassigned(this.lits[i++])) {
351                 curr--;
352                 if (curr < this.degree) {
353                     return false;
354                 }
355             }
356         }
357 
358         return false;
359     }
360 
361     /**
362      * Cha?ne repr?sentant la contrainte
363      * 
364      * @return Cha?ne repr?sentant la contrainte
365      */
366     @Override
367     public String toString() {
368         StringBuffer stb = new StringBuffer();
369 
370         if (this.lits.length > 0) {
371             if (this.voc.isUnassigned(this.lits[0])) {
372                 stb.append(Lits.toString(this.lits[0]));
373                 stb.append(" "); //$NON-NLS-1$
374             }
375             for (int i = 1; i < this.lits.length; i++) {
376                 if (this.voc.isUnassigned(this.lits[i])) {
377                     stb.append(" + "); //$NON-NLS-1$
378                     stb.append(Lits.toString(this.lits[i]));
379                     stb.append(" "); //$NON-NLS-1$
380                 }
381             }
382             stb.append(">= "); //$NON-NLS-1$
383             stb.append(this.degree);
384         }
385         return stb.toString();
386     }
387 
388     /**
389      * M?thode appel?e lors du backtrack
390      * 
391      * @param p
392      *            le litt?ral d?saffect?
393      */
394     public void undo(int p) {
395         this.watchCumul++;
396     }
397 
398     public void setLearnt() {
399         throw new UnsupportedOperationException();
400     }
401 
402     public void register() {
403         throw new UnsupportedOperationException();
404     }
405 
406     public int size() {
407         return this.lits.length;
408     }
409 
410     public int get(int i) {
411         return this.lits[i];
412     }
413 
414     public void assertConstraint(UnitPropagationListener s) {
415         throw new UnsupportedOperationException();
416     }
417 
418     /*
419      * (non-Javadoc)
420      * 
421      * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
422      */
423     public BigInteger getCoef(int literal) {
424         return BigInteger.ONE;
425     }
426 
427     /*
428      * (non-Javadoc)
429      * 
430      * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
431      */
432     public BigInteger getDegree() {
433         return BigInteger.valueOf(this.degree);
434     }
435 
436     public ILits getVocabulary() {
437         return this.voc;
438     }
439 
440     /**
441      * @since 2.1
442      */
443     public void forwardActivity(double claInc) {
444         // TODO Auto-generated method stub
445 
446     }
447 
448     public boolean canBePropagatedMultipleTimes() {
449         return true;
450     }
451 
452     public Constr toConstraint() {
453         return this;
454     }
455 }