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