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