View Javadoc

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