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 MinWatchPb extends WatchPb {
39  
40      private static final long serialVersionUID = 1L;
41  
42      /**
43       * Liste des indices des litt???raux regardant la contrainte
44       */
45      protected boolean[] watched;
46  
47      /**
48       * Sert ??? d???terminer si la clause est watched par le litt???ral
49       */
50      protected int[] watching;
51  
52      /**
53       * Liste des indices des litt???raux regardant la contrainte
54       */
55      protected int watchingCount = 0;
56  
57      /**
58       * Constructeur de base des contraintes
59       * 
60       * @param voc
61       *            Informations sur le vocabulaire employ???
62       * @param mpb 
63       *            a mutable PB constraint 
64       */
65      protected MinWatchPb(ILits voc, IDataStructurePB mpb) {
66  
67          super(mpb);
68          this.voc = voc;
69  
70          watching = new int[this.coefs.length];
71          watched = new boolean[this.coefs.length];
72          activity = 0;
73          watchCumul = BigInteger.ZERO;
74          locked = false;
75  
76          watchingCount = 0;
77  
78      }
79  
80      protected MinWatchPb(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) {
81  
82          super(lits, coefs, degree);
83          this.voc = voc;
84  
85          watching = new int[this.coefs.length];
86          watched = new boolean[this.coefs.length];
87          activity = 0;
88          watchCumul = BigInteger.ZERO;
89          locked = false;
90  
91          watchingCount = 0;
92  
93      }
94      /*
95       * (non-Javadoc)
96       * 
97       * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
98       */
99      @Override
100     protected void computeWatches() throws ContradictionException {
101         assert watchCumul.signum() == 0;
102         assert watchingCount == 0;
103         for (int i = 0; i < lits.length
104                 && watchCumul.subtract(coefs[0]).compareTo(degree) < 0; i++) {
105             if (!voc.isFalsified(lits[i])) {
106                 voc.watch(lits[i] ^ 1, this);
107                 watching[watchingCount++] = i;
108                 watched[i] = true;
109                 // Mise ??? jour de la possibilit??? initiale
110                 watchCumul = watchCumul.add(coefs[i]);
111             }
112         }
113 
114         if (learnt)
115             watchMoreForLearntConstraint();
116 
117         if (watchCumul.compareTo(degree) < 0) {
118             throw new ContradictionException("non satisfiable constraint");
119         }
120         assert nbOfWatched() == watchingCount;
121     }
122 
123     private void watchMoreForLearntConstraint() {
124         // chercher tous les litteraux a regarder
125         // par ordre de niveau decroissant
126         int free = 1;
127         int maxlevel, maxi, level;
128 
129         while ((watchCumul.subtract(coefs[0]).compareTo(degree) < 0)
130                 && (free > 0)) {
131             free = 0;
132             // regarder le litteral falsifie au plus bas niveau
133             maxlevel = -1;
134             maxi = -1;
135             for (int i = 0; i < lits.length; i++) {
136                 if (voc.isFalsified(lits[i]) && !watched[i]) {
137                     free++;
138                     level = voc.getLevel(lits[i]);
139                     if (level > maxlevel) {
140                         maxi = i;
141                         maxlevel = level;
142                     }
143                 }
144             }
145 
146             if (free > 0) {
147                 assert maxi >= 0;
148                 voc.watch(lits[maxi] ^ 1, this);
149                 watching[watchingCount++] = maxi;
150                 watched[maxi] = true;
151                 // Mise ??? jour de la possibilit??? initiale
152                 watchCumul = watchCumul.add(coefs[maxi]);
153                 free--;
154                 assert free >= 0;
155             }
156         }
157         assert lits.length == 1 || watchingCount > 1;
158     }
159 
160     /*
161      * (non-Javadoc)
162      * 
163      * @see org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat.UnitPropagationListener)
164      */
165     @Override
166     protected void computePropagation(UnitPropagationListener s)
167             throws ContradictionException {
168         // On propage si n???cessaire
169         int ind = 0;
170         while (ind < lits.length
171                 && watchCumul.subtract(coefs[watching[ind]]).compareTo(degree) < 0) {
172             if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) {
173                 throw new ContradictionException("non satisfiable constraint");
174             }
175             ind++;
176         }
177     }
178 
179     /**
180      * @param s
181      *            outil pour la propagation des litt???raux
182      * @param ps
183      *            liste des litt???raux de la nouvelle contrainte
184      * @param coefs
185      *            liste des coefficients des litt???raux de la contrainte
186      * @param moreThan
187      *            d???termine si c'est une sup???rieure ou ???gal ??? l'origine
188      * @param degree
189      *            fournit le degr??? de la contrainte
190      * @return une nouvelle clause si tout va bien, ou null si un conflit est
191      *         d???tect???
192      */
193     public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
194             ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
195             throws ContradictionException {
196         return minWatchPbNew(s, voc, ps, toVecBigInt(coefs), moreThan,
197                 toBigInt(degree));
198     }
199 
200     /**
201      * @param s
202      *            outil pour la propagation des litt???raux
203      * @param ps
204      *            liste des litt???raux de la nouvelle contrainte
205      * @param coefs
206      *            liste des coefficients des litt???raux de la contrainte
207      * @param moreThan
208      *            d???termine si c'est une sup???rieure ou ???gal ??? l'origine
209      * @param degree
210      *            fournit le degr??? de la contrainte
211      * @return une nouvelle clause si tout va bien, ou null si un conflit est
212      *         d???tect???
213      */
214     public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
215             ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
216             BigInteger degree) throws ContradictionException {
217         // Il ne faut pas modifier les param?tres
218         VecInt litsVec = new VecInt(ps.size());
219         IVec<BigInteger> coefsVec = new Vec<BigInteger>(coefs.size());
220         ps.copyTo(litsVec);
221         coefs.copyTo(coefsVec);
222 
223         // Ajouter les simplifications quand la structure sera d???finitive
224         IDataStructurePB mpb = niceParameters(litsVec, coefsVec, moreThan,
225                 degree, voc);
226 
227         if (mpb == null)
228             return null;
229 
230         MinWatchPb outclause = new MinWatchPb(voc, mpb);
231 
232         if (outclause.degree.signum() <= 0) {
233             return null;
234         }
235 
236         outclause.computeWatches();
237 
238         outclause.computePropagation(s);
239 
240         return outclause;
241 
242     }
243 
244     /**
245      * @param s
246      *            a unit propagation listener
247      * @param voc
248      *            the vocabulary
249      * @param mpb
250      *            the PB constraint to normalize.
251      * @return a new PB contraint or null if a trivial inconsistency is
252      *         detected.
253      */
254     public static MinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
255             ILits voc, IDataStructurePB mpb) throws ContradictionException {
256         // Il ne faut pas modifier les param?tres
257         MinWatchPb outclause = new MinWatchPb(voc, mpb);
258 
259         if (outclause.degree.signum() <= 0) {
260             return null;
261         }
262 
263         outclause.computeWatches();
264 
265         outclause.computePropagation(s);
266 
267         return outclause;
268 
269     }
270 
271     /**
272      * @param s
273      *            a unit propagation listener
274      * @param voc
275      *            the vocabulary
276      * @param lits
277      *            the literals
278      * @param coefs
279      *            the coefficients
280      * @param degree
281      *            the degree of the constraint to normalize.
282      * @return a new PB constraint or null if a trivial inconsistency is
283      *         detected.
284      */
285     public static MinWatchPb normalizedMinWatchPbNew(UnitPropagationListener s,
286             ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) throws ContradictionException {
287         // Il ne faut pas modifier les param?tres
288         MinWatchPb outclause = new MinWatchPb(voc, lits, coefs, degree);
289 
290         if (outclause.degree.signum() <= 0) {
291             return null;
292         }
293 
294         outclause.computeWatches();
295 
296         outclause.computePropagation(s);
297 
298         return outclause;
299 
300     }
301 
302     /**
303      * Nombre de litt???raux actuellement observ???
304      * 
305      * @return nombre de litt???raux regard???s
306      */
307     protected int nbOfWatched() {
308         int retour = 0;
309         for (int ind = 0; ind < this.watched.length; ind++) {
310             for (int i = 0; i < watchingCount; i++)
311                 if (watching[i] == ind)
312                     assert watched[ind];
313             retour += (this.watched[ind]) ? 1 : 0;
314         }
315         return retour;
316     }
317 
318     /**
319      * Propagation de la valeur de v???rit??? d'un litt???ral falsifi???
320      * 
321      * @param s
322      *            un prouveur
323      * @param p
324      *            le litt???ral propag??? (il doit etre falsifie)
325      * @return false ssi une inconsistance est d???t???ct???e
326      */
327     public boolean propagate(UnitPropagationListener s, int p) {
328         assert nbOfWatched() == watchingCount;
329         assert watchingCount > 1;
330 
331         // Recherche de l'indice du litt???ral p
332         int pIndiceWatching = 0;
333         while (pIndiceWatching < watchingCount
334                 && (lits[watching[pIndiceWatching]] ^ 1) != p)
335             pIndiceWatching++;
336         int pIndice = watching[pIndiceWatching];
337 
338         assert p == (lits[pIndice] ^ 1);
339         assert watched[pIndice];
340 
341         // Recherche du coefficient maximal parmi ceux des litt???raux
342         // observ???s
343         BigInteger maxCoef = maximalCoefficient(pIndice);
344 
345         // Recherche de la compensation
346         maxCoef = updateWatched(maxCoef, pIndice);
347 
348         BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
349         assert nbOfWatched() == watchingCount;
350 
351         // Effectuer les propagations, return si l'une est impossible
352         if (upWatchCumul.compareTo(degree) < 0) {
353             // conflit
354             voc.watch(p, this);
355             assert watched[pIndice];
356             assert !isSatisfiable();
357             return false;
358         } else if (upWatchCumul.compareTo(degree.add(maxCoef)) < 0) {
359 
360             assert watchingCount != 0;
361             BigInteger limit = upWatchCumul.subtract(degree);
362             for (int i = 0; i < watchingCount; i++) {
363                 if (limit.compareTo(coefs[watching[i]]) < 0
364                         && i != pIndiceWatching
365                         && !voc.isSatisfied(lits[watching[i]])
366                         && !s.enqueue(lits[watching[i]], this)) {
367                     voc.watch(p, this);
368                     assert !isSatisfiable();
369                     return false;
370                 }
371             }
372             // Si propagation ajoute la contrainte aux undos de p, conserver p
373             voc.undos(p).push(this);
374         }
375 
376         // sinon p peut sortir de la liste de watched
377         watched[pIndice] = false;
378         watchCumul = upWatchCumul;
379         watching[pIndiceWatching] = watching[--watchingCount];
380 
381         assert watchingCount != 0;
382         assert nbOfWatched() == watchingCount;
383 
384         return true;
385     }
386 
387     /**
388      * Enl???ve une contrainte du prouveur
389      */
390     public void remove() {
391         for (int i = 0; i < watchingCount; i++) {
392             voc.watches(lits[watching[i]] ^ 1).remove(this);
393             this.watched[this.watching[i]] = false;
394         }
395         watchingCount = 0;
396         assert nbOfWatched() == watchingCount;
397     }
398 
399     /**
400      * M???thode appel???e lors du backtrack
401      * 
402      * @param p
403      *            un litt???ral d???saffect???
404      */
405     public void undo(int p) {
406         voc.watch(p, this);
407         int pIndice = 0;
408         while ((lits[pIndice] ^ 1) != p)
409             pIndice++;
410 
411         assert pIndice < lits.length;
412 
413         watchCumul = watchCumul.add(coefs[pIndice]);
414 
415         assert watchingCount == nbOfWatched();
416 
417         watched[pIndice] = true;
418         watching[watchingCount++] = pIndice;
419 
420         assert watchingCount == nbOfWatched();
421     }
422 
423     /**
424      * 
425      */
426     public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
427             boolean moreThan, int degree) {
428         return watchPbNew(voc, lits, toVecBigInt(coefs), moreThan,
429                 toBigInt(degree));
430     }
431 
432     /**
433      * 
434      */
435     public static WatchPb watchPbNew(ILits voc, IVecInt lits,
436             IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
437         IDataStructurePB mpb = null;
438         mpb = niceCheckedParameters(lits, coefs, moreThan, degree, voc);
439         return new MinWatchPb(voc, mpb);
440     }
441 
442     /**
443      * 
444      */
445     public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
446         return new MinWatchPb(voc, mpb);
447     }
448 
449     /**
450      * 
451      * @param pIndice
452      *            propagated literal : its coefficient is excluded from the
453      *            search of the maximal coefficient
454      * @return the maximal coefficient for the watched literals
455      */
456     protected BigInteger maximalCoefficient(int pIndice) {
457         BigInteger maxCoef = BigInteger.ZERO;
458         for (int i = 0; i < watchingCount; i++)
459             if (coefs[watching[i]].compareTo(maxCoef) > 0
460                     && watching[i] != pIndice) {
461                 maxCoef = coefs[watching[i]];
462             }
463 
464         assert learnt || maxCoef.signum() != 0;
465         // DLB assert maxCoef!=0;
466         return maxCoef;
467     }
468 
469     protected BigInteger updateWatched(BigInteger mc, int pIndice) {
470         BigInteger maxCoef = mc;
471         if (watchingCount < size()) {
472             BigInteger upWatchCumul = watchCumul.subtract(coefs[pIndice]);
473 
474             BigInteger degreePlusMaxCoef = degree.add(maxCoef); // dvh
475             for (int ind = 0; ind < lits.length; ind++) {
476                 if (upWatchCumul.compareTo(degreePlusMaxCoef) >= 0) {
477                     // note: logic negated to old version // dvh
478                     break;
479                 }
480 
481                 if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
482                     upWatchCumul = upWatchCumul.add(coefs[ind]);
483                     watched[ind] = true;
484                     assert watchingCount < size();
485                     watching[watchingCount++] = ind;
486                     voc.watch(lits[ind] ^ 1, this);
487                     // Si on obtient un nouveau coefficient maximum
488                     if (coefs[ind].compareTo(maxCoef) > 0) {
489                         maxCoef = coefs[ind];
490                         degreePlusMaxCoef = degree.add(maxCoef); // update
491                         // that one
492                         // too
493                     }
494                 }
495             }
496             watchCumul = upWatchCumul.add(coefs[pIndice]);
497         }
498         return maxCoef;
499     }
500 
501 }