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 MaxWatchPb extends WatchPb {
41
42 private static final long serialVersionUID = 1L;
43
44 /**
45 * Constructeur de base cr?ant des contraintes vides
46 *
47 * @param voc
48 * Informations sur le vocabulaire employ?
49 * @param ps
50 * Liste des litt?raux
51 * @param weightedLits
52 * Liste des coefficients
53 * @param moreThan
54 * Indication sur le comparateur
55 * @param degree
56 * Stockage du degr? de la contrainte
57 */
58 private MaxWatchPb(ILits voc, IDataStructurePB mpb) {
59
60 super(mpb);
61 this.voc = voc;
62
63 activity = 0;
64 watchCumul = BigInteger.ZERO;
65 }
66
67 private MaxWatchPb(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) {
68
69 super(lits, coefs, degree);
70 this.voc = voc;
71
72 activity = 0;
73 watchCumul = BigInteger.ZERO;
74 }
75
76 /**
77 * Permet l'observation de tous les litt???raux
78 *
79 * @see org.sat4j.pb.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 voc.attach(lits[i] ^ 1, this);
89 }
90 } else {
91 // Mise ? jour de la possibilit? initiale
92 voc.attach(lits[i] ^ 1, this);
93 watchCumul = watchCumul.add(coefs[i]);
94 }
95 }
96
97 assert watchCumul.compareTo(recalcLeftSide()) >= 0;
98 if (!learnt && watchCumul.compareTo(degree) < 0) {
99 throw new ContradictionException("non satisfiable constraint");
100 }
101 }
102
103 /*
104 * (non-Javadoc)
105 *
106 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
107 */
108 @Override
109 protected void computePropagation(UnitPropagationListener s)
110 throws ContradictionException {
111 // On propage
112 int ind = 0;
113 while (ind < coefs.length
114 && watchCumul.subtract(coefs[ind]).compareTo(degree) < 0) {
115 if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this))
116 throw new ContradictionException("non satisfiable constraint");
117 ind++;
118 }
119 assert watchCumul.compareTo(recalcLeftSide()) >= 0;
120 }
121
122 /**
123 * @param s
124 * outil pour la propagation des litt?raux
125 * @param ps
126 * liste des litt?raux de la nouvelle contrainte
127 * @param coefs
128 * liste des coefficients des litt?raux de la contrainte
129 * @param moreThan
130 * d?termine si c'est une sup?rieure ou ?gal ? l'origine
131 * @param degree
132 * fournit le degr? de la contrainte
133 * @return une nouvelle clause si tout va bien, ou null si un conflit est
134 * d?tect?
135 */
136 public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
137 ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
138 throws ContradictionException {
139 return maxWatchPbNew(s, voc, ps, Pseudos.toVecBigInt(coefs), moreThan,
140 BigInteger.valueOf(degree));
141 }
142
143 /**
144 * @param s
145 * outil pour la propagation des litt?raux
146 * @param ps
147 * liste des litt?raux de la nouvelle contrainte
148 * @param coefs
149 * liste des coefficients des litt?raux de la contrainte
150 * @param moreThan
151 * d?termine si c'est une sup?rieure ou ?gal ? l'origine
152 * @param degree
153 * fournit le degr? de la contrainte
154 * @return une nouvelle clause si tout va bien, ou null si un conflit est
155 * d?tect?
156 */
157 public static MaxWatchPb maxWatchPbNew(UnitPropagationListener s,
158 ILits voc, IVecInt ps, IVec<BigInteger> coefs, boolean moreThan,
159 BigInteger degree) throws ContradictionException {
160
161 // Il ne faut pas modifier les param?tres
162 VecInt litsVec = new VecInt();
163 IVec<BigInteger> coefsVec = new Vec<BigInteger>();
164 ps.copyTo(litsVec);
165 coefs.copyTo(coefsVec);
166
167 IDataStructurePB mpb = Pseudos.niceParameters(litsVec, coefsVec, moreThan,
168 degree, voc);
169
170 if (mpb == null) {
171 return null;
172 }
173 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
174
175 if (outclause.degree.signum() <= 0)
176 return null;
177 outclause.computeWatches();
178 outclause.computePropagation(s);
179
180 return outclause;
181
182 }
183
184 /**
185 * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
186 *
187 * @param s
188 * un prouveur
189 * @param p
190 * le litt?ral propag? (il doit etre falsifie)
191 * @return false ssi une inconsistance est d?tect?e
192 */
193 public boolean propagate(UnitPropagationListener s, int p) {
194 voc.attach(p, this);
195
196 assert watchCumul.compareTo(recalcLeftSide()) >= 0 : "" + watchCumul
197 + "/" + recalcLeftSide() + ":" + learnt;
198
199 // Si le litt?ral est impliqu? il y a un conflit
200 int indiceP = 0;
201 while ((lits[indiceP] ^ 1) != p)
202 indiceP++;
203
204 BigInteger coefP = coefs[indiceP];
205
206 BigInteger newcumul = watchCumul.subtract(coefP);
207 if (newcumul.compareTo(degree) < 0) {
208 // System.out.println(this.analyse(new ConstrHandle()));
209
210 assert !isSatisfiable();
211 return false;
212 }
213
214 // On met en place la mise ? jour du compteur
215 voc.undos(p).push(this);
216 watchCumul = newcumul;
217
218 // On propage
219 int ind = 0;
220 BigInteger limit = watchCumul.subtract(degree);
221 while (ind < coefs.length && limit.compareTo(coefs[ind]) < 0) {
222 if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
223 assert !isSatisfiable();
224 return false;
225 }
226 ind++;
227 }
228
229 assert learnt || watchCumul.compareTo(recalcLeftSide()) >= 0;
230 assert watchCumul.compareTo(recalcLeftSide()) >= 0;
231 return true;
232 }
233
234 /**
235 * Enl???ve une contrainte du prouveur
236 */
237 public void remove() {
238 for (int i = 0; i < lits.length; i++) {
239 if (!voc.isFalsified(lits[i]))
240 voc.attaches(lits[i] ^ 1).remove(this);
241 }
242 }
243
244 /**
245 * M?thode appel?e lors du backtrack
246 *
247 * @param p
248 * un litt?ral d?saffect?
249 */
250 public void undo(int p) {
251 int indiceP = 0;
252 while ((lits[indiceP] ^ 1) != p)
253 indiceP++;
254
255 assert coefs[indiceP].signum() > 0;
256
257 watchCumul = watchCumul.add(coefs[indiceP]);
258 }
259
260 /**
261 *
262 */
263 public static WatchPb watchPbNew(ILits voc, IVecInt lits, IVecInt coefs,
264 boolean moreThan, int degree) {
265 return watchPbNew(voc, lits, Pseudos.toVecBigInt(coefs), moreThan,
266 BigInteger.valueOf(degree));
267 }
268
269
270 /**
271 *
272 */
273 public static WatchPb watchPbNew(ILits voc, IVecInt lits,
274 IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) {
275 IDataStructurePB mpb = null;
276 mpb = Pseudos.niceCheckedParameters(lits, coefs, moreThan, degree, voc);
277 return new MaxWatchPb(voc, mpb);
278 }
279
280 /**
281 * @param s
282 * a unit propagation listener
283 * @param voc
284 * the vocabulary
285 * @param mpb
286 * the PB constraint to normalize.
287 * @return a new PB contraint or null if a trivial inconsistency is
288 * detected.
289 */
290 public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
291 ILits voc, IDataStructurePB mpb) throws ContradictionException {
292 // Il ne faut pas modifier les param?tres
293 MaxWatchPb outclause = new MaxWatchPb(voc, mpb);
294
295 if (outclause.degree.signum() <= 0) {
296 return null;
297 }
298
299 outclause.computeWatches();
300
301 outclause.computePropagation(s);
302
303 return outclause;
304
305 }
306
307 /**
308 * @param s
309 * a unit propagation listener
310 * @param voc
311 * the vocabulary
312 * @param lits
313 * the literals of the constraint
314 * @param coefs
315 * the coefficients of the constraint
316 * @param degree
317 * the degree of the constraint
318 * @return a new PB constraint or null if a trivial inconsistency is
319 * detected.
320 */
321 public static MaxWatchPb normalizedMaxWatchPbNew(UnitPropagationListener s,
322 ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) throws ContradictionException {
323 // Il ne faut pas modifier les param?tres
324 MaxWatchPb outclause = new MaxWatchPb(voc, lits, coefs, degree);
325
326 if (outclause.degree.signum() <= 0) {
327 return null;
328 }
329
330 outclause.computeWatches();
331
332 outclause.computePropagation(s);
333
334 return outclause;
335
336 }
337
338 /**
339 *
340 */
341 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
342 return new MaxWatchPb(voc, mpb);
343 }
344
345
346 }