View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  
26  package org.sat4j.minisat.constraints.pb;
27  
28  import java.math.BigInteger;
29  
30  import org.sat4j.core.Vec;
31  import org.sat4j.core.VecInt;
32  import org.sat4j.minisat.core.ILits;
33  import org.sat4j.minisat.core.UnitPropagationListener;
34  import org.sat4j.specs.ContradictionException;
35  import org.sat4j.specs.IVec;
36  import org.sat4j.specs.IVecInt;
37  
38  public class MaxWatchPb extends WatchPb {
39  
40      private static final long serialVersionUID = 1L;
41  
42      /**
43       * Constructeur de base cr?ant des contraintes vides
44       * 
45       * @param voc
46       *            Informations sur le vocabulaire employ?
47       * @param ps
48       *            Liste des litt?raux
49       * @param coefs
50       *            Liste des coefficients
51       * @param moreThan
52       *            Indication sur le comparateur
53       * @param degree
54       *            Stockage du degr? de la contrainte
55       */
56      private MaxWatchPb(ILits voc, IDataStructurePB mpb) {
57  
58          super(mpb);
59          this.voc = voc;
60  
61          activity = 0;
62          watchCumul = BigInteger.ZERO;
63          locked = false;
64      }
65  
66      private MaxWatchPb(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) {
67  
68          super(lits, coefs, degree);
69          this.voc = voc;
70  
71          activity = 0;
72          watchCumul = BigInteger.ZERO;
73          locked = false;
74      }
75  
76      /**
77       * Permet l'observation de tous les litt???raux
78       * 
79       * @see org.sat4j.minisat.constraints.pb.WatchPb#computeWatches()
80       */
81      @Override
82      protected void computeWatches() throws ContradictionException {
83          assert watchCumul.equals(BigInteger.ZERO);
84          for (int i = 0; i < lits.length; i++) {
85              if (voc.isFalsified(lits[i])) {
86                  if (learnt)
87                      voc.undos(lits[i] ^ 1).push(this);
88              } else {
89                  // Mise ? jour de la possibilit? initiale
90                  voc.watch(lits[i] ^ 1, this);
91                  watchCumul = watchCumul.add(coefs[i]);
92              }
93          }
94  
95          assert watchCumul.compareTo(recalcLeftSide()) >= 0;
96          if (!learnt && watchCumul.compareTo(degree) < 0) {
97              throw new ContradictionException("non satisfiable constraint");
98          }
99      }
100 
101     /*
102      * (non-Javadoc)
103      * 
104      * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
105      */
106     @Override
107     protected void computePropagation(UnitPropagationListener s)
108             throws ContradictionException {
109         // On propage
110         int ind = 0;
111         while (ind < coefs.length
112                 && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
113             if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) 
114                 throw new ContradictionException("non satisfiable constraint");
115             ind++;
116         }
117         assert watchCumul.compareTo(recalcLeftSide()) >= 0;
118     }
119 
120     /**
121      * @param s
122      *            outil pour la propagation des litt?raux
123      * @param ps
124      *            liste des litt?raux de la nouvelle contrainte
125      * @param coefs
126      *            liste des coefficients des litt?raux de la contrainte
127      * @param moreThan
128      *            d?termine si c'est une sup?rieure ou ?gal ? l'origine
129      * @param degree
130      *            fournit le degr? de la contrainte
131      * @return une nouvelle clause si tout va bien, ou null si un conflit est
132      *         d?tect?
133      */
134     public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
135             ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
136             throws ContradictionException {
137         return maxWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
138                 toBigInt(degree));
139     }
140 
141     /**
142      * @param s
143      *            outil pour la propagation des litt?raux
144      * @param ps
145      *            liste des litt?raux de la nouvelle contrainte
146      * @param coefs
147      *            liste des coefficients des litt?raux de la contrainte
148      * @param moreThan
149      *            d?termine si c'est une sup?rieure ou ?gal ? l'origine
150      * @param degree
151      *            fournit le degr? de la contrainte
152      * @return une nouvelle clause si tout va bien, ou null si un conflit est
153      *         d?tect?
154      */
155     public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
156             ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
157             BigInteger degree) throws ContradictionException {
158 
159         // Il ne faut pas modifier les param?tres
160         VecInt litsVec = new VecInt();
161         IVec<BigInteger> coefsVec = new Vec<BigInteger>();
162         ps.copyTo(litsVec);
163         coefs.copyTo(coefsVec);
164 
165         IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
166                 degree, voc);
167 
168         if (mpb == null) {
169             return null;
170         }
171         MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
172 
173         if (outclause.degree.signum() <= 0)
174             return null;
175         outclause.computeWatches();
176         outclause.computePropagation(s);
177 
178         return outclause;
179 
180     }
181 
182     /**
183      * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
184      * 
185      * @param s
186      *            un prouveur
187      * @param p
188      *            le litt?ral propag? (il doit etre falsifie)
189      * @return false ssi une inconsistance est d?tect?e
190      */
191     public boolean propagate(UnitPropagationListener s, int p) {
192         voc.watch(p, this);
193 
194         assert watchCumul.compareTo(recalcLeftSide()) >= 0 : "" + watchCumul
195                 + "/" + recalcLeftSide() + ":" + learnt;
196 
197         // Si le litt?ral est impliqu? il y a un conflit
198         int indiceP = 0;
199         while ((lits[indiceP] ^ 1) != p)
200             indiceP++;
201 
202         BigInteger coefP = coefs[indiceP];
203 
204         BigInteger newcumul = watchCumul.subtract(coefP);
205         if (newcumul.compareTo(degree) < 0) {
206             // System.out.println(this.analyse(new ConstrHandle()));
207 
208             assert !isSatisfiable();
209             return false;
210         }
211 
212         // On met en place la mise ? jour du compteur
213         voc.undos(p).push(this);
214         watchCumul = newcumul;
215 
216         // On propage
217         int ind = 0;
218         BigInteger limit = watchCumul.subtract(degree);
219         while (ind < coefs.length && limit.compareTo(coefs[ind]) < 0) {
220             if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
221                 assert !isSatisfiable();
222                 return false;
223             }
224             ind++;
225         }
226 
227         assert learnt || watchCumul.compareTo(recalcLeftSide()) >= 0;
228         assert watchCumul.compareTo(recalcLeftSide()) >= 0;
229         return true;
230     }
231 
232     /**
233      * Enl???ve une contrainte du prouveur
234      */
235     public void remove() {
236         for (int i = 0; i < lits.length; i++) {
237             if (!voc.isFalsified(lits[i]))
238                 voc.watches(lits[i] ^ 1).remove(this);
239         }
240     }
241 
242     /**
243      * M?thode appel?e lors du backtrack
244      * 
245      * @param p
246      *            un litt?ral d?saffect?
247      */
248     public void undo(int p) {
249         int indiceP = 0;
250         while ((lits[indiceP] ^ 1) != p)
251             indiceP++;
252 
253         assert coefs[indiceP].signum() > 0;
254 
255         watchCumul = watchCumul.add(coefs[indiceP]);
256     }
257 
258     /**
259      * 
260      */
261     public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
262             boolean moreThan, int degree) {
263         return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
264                 toBigInt(degree));
265     }
266 
267     /**
268      * 
269      */
270     public static WatchPb watchPbNew(ILits voc, IVecInt lits,
271             IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
272         IDataStructurePB mpb = null;
273         mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
274         return new MaxWatchPb(voc, mpb);
275     }
276 
277     /**
278      * @param s
279      *            a unit propagation listener
280      * @param voc
281      *            the vocabulary
282      * @param mpb
283      *            the PB constraint to normalize.
284      * @return a new PB contraint or null if a trivial inconsistency is
285      *         detected.
286      */
287     public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
288             ILits voc, IDataStructurePB mpb) throws ContradictionException {
289         // Il ne faut pas modifier les param?tres
290         MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
291 
292         if (outclause.degree.signum() <= 0) {
293             return null;
294         }
295 
296         outclause.computeWatches();
297 
298         outclause.computePropagation(s);
299 
300         return outclause;
301 
302     }
303 
304     /**
305      * @param s
306      *            a unit propagation listener
307      * @param voc
308      *            the vocabulary
309      * @param lits
310      *            the literals of the constraint
311      * @param coefs
312      *            the coefficients of the constraint
313      * @param degree 
314      *            the degree of the constraint
315      * @return a new PB constraint or null if a trivial inconsistency is
316      *         detected.
317      */
318     public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
319             ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) throws ContradictionException {
320         // Il ne faut pas modifier les param?tres
321         MaxWatchPb outclause = new MaxWatchPb(voc, lits, coefs, degree);
322 
323         if (outclause.degree.signum() <= 0) {
324             return null;
325         }
326 
327         outclause.computeWatches();
328 
329         outclause.computePropagation(s);
330 
331         return outclause;
332 
333     }
334 
335 }