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 final 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 for (int i = 0; i < lits.length; i++) {
142 if (voc.isFalsified(lits[i])) {
143 outReason.push(lits[i] ^ 1);
144 }
145 }
146 }
147
148 /**
149 * Obtenir la valeur de l'activit? de la contrainte
150 *
151 * @return la valeur de l'activit? de la contrainte
152 * @see Constr#getActivity()
153 */
154 public double getActivity() {
155 // TODO getActivity
156 return 0;
157 }
158
159 /**
160 * Incr?mente la valeur de l'activit? de la contrainte
161 *
162 * @param claInc
163 * incr?ment de l'activit? de la contrainte
164 * @see Constr#incActivity(double claInc)
165 */
166 public void incActivity(double claInc) {
167 // TODO incActivity
168 }
169
170 /**
171 * D?termine si la contrainte est apprise
172 *
173 * @return true si la contrainte est apprise, false sinon
174 * @see Constr#learnt()
175 */
176 public boolean learnt() {
177 // TODO learnt
178 return false;
179 }
180
181 /**
182 * La contrainte est la cause d'une propagation unitaire
183 *
184 * @return true si c'est le cas, false sinon
185 * @see Constr#locked()
186 */
187 public boolean locked() {
188 // TODO locked
189 return true;
190 }
191
192 /**
193 * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
194 *
195 * @param s
196 * outil pour la propagation des litt?raux
197 * @param voc
198 * vocabulaire utilis? par la contrainte
199 * @param ps
200 * liste des litt?raux de la nouvelle contrainte
201 * @param moreThan
202 * d?termine si c'est une sup?rieure ou ?gal ? l'origine
203 * @param degree
204 * fournit le degr? de la contrainte
205 * @return une nouvelle clause si tout va bien, null sinon
206 * @throws ContradictionException
207 */
208 public static MaxWatchCard maxWatchCardNew(UnitPropagationListener s,
209 ILits voc, IVecInt ps, boolean moreThan, int degree)
210 throws ContradictionException {
211
212 MaxWatchCard outclause = null;
213
214 // La contrainte ne doit pas ?tre vide
215 if (ps.size() == 0) {
216 throw new ContradictionException("Creating empty clause"); //$NON-NLS-1$
217 } else if (ps.size() == degree) {
218 for (int i = 0; i < ps.size(); i++)
219 if (!s.enqueue(ps.get(i))) {
220 throw new ContradictionException(
221 "Contradiction with implied literal"); //$NON-NLS-1$
222 }
223 return null;
224 }
225
226 // On cree la contrainte
227 outclause = new MaxWatchCard(voc, ps, moreThan, degree);
228
229 // Si le degr? est insufisant
230 if (outclause.degree <= 0)
231 return null;
232
233 // Si il n'y a aucune chance de satisfaire la contrainte
234 if (outclause.watchCumul < outclause.degree)
235 throw new ContradictionException();
236
237 // Si les litt?raux observ?s sont impliqu?s
238 if (outclause.watchCumul == outclause.degree) {
239 for (int i = 0; i < outclause.lits.length; i++) {
240 if (!s.enqueue(outclause.lits[i])) {
241 throw new ContradictionException(
242 "Contradiction with implied literal"); //$NON-NLS-1$
243 }
244 }
245 return null;
246 }
247
248 return outclause;
249 }
250
251 /**
252 * On normalise la contrainte au sens de Barth
253 */
254 public final void normalize() {
255 // Gestion du signe
256 if (!moreThan) {
257 // On multiplie le degr? par -1
258 this.degree = 0 - this.degree;
259 // On r?vise chaque litt?ral
260 for (int indLit = 0; indLit < lits.length; indLit++) {
261 lits[indLit] = lits[indLit] ^ 1;
262 this.degree++;
263 }
264 this.moreThan = true;
265 }
266 }
267
268 /**
269 * Propagation de la valeur de v?rit? d'un litt?ral falsifi?
270 *
271 * @param s
272 * objet utilis? pour la propagation
273 * @param p
274 * le litt?ral propag? (il doit etre falsifie)
275 * @return false ssi une inconsistance est d?t?ct?e
276 */
277 public boolean propagate(UnitPropagationListener s, int p) {
278
279 // On observe toujours tous les litt?raux
280 voc.watch(p, this);
281 assert !voc.isFalsified(p);
282
283 // Si le litt?ral p est impliqu?
284 if (this.watchCumul == this.degree)
285 return false;
286
287 // On met en place la mise ? jour du compteur
288 voc.undos(p).push(this);
289 watchCumul--;
290
291 // Si les litt?raux restant sont impliqu?s
292 if (watchCumul == degree) {
293 for (int q : lits) {
294 if (voc.isUnassigned(q) && !s.enqueue(q, this)) {
295 return false;
296 }
297 }
298 }
299 return true;
300 }
301
302 /**
303 * @since 2.1
304 */
305 public void remove(UnitPropagationListener upl) {
306 for (int q : lits) {
307 voc.watches(q ^ 1).remove(this);
308 }
309 }
310
311 /**
312 * Permet le r??chantillonage de l'activit? de la contrainte
313 *
314 * @param d
315 * facteur d'ajustement
316 */
317 public void rescaleBy(double d) {
318 }
319
320 /**
321 * Simplifie la contrainte(l'all?ge)
322 *
323 * @return true si la contrainte est satisfaite, false sinon
324 */
325 public boolean simplify() {
326
327 int i = 0;
328
329 // On esp?re le maximum de la somme
330 int curr = watchCumul;
331
332 // Pour chaque litt?ral
333 while (i < this.lits.length) {
334 // On d?cr?mente si l'espoir n'est pas fond?
335 if (voc.isUnassigned(lits[i++])) {
336 curr--;
337 if (curr < this.degree)
338 return false;
339 }
340 }
341
342 return false;
343 }
344
345 /**
346 * Cha?ne repr?sentant la contrainte
347 *
348 * @return Cha?ne repr?sentant la contrainte
349 */
350 @Override
351 public String toString() {
352 StringBuffer stb = new StringBuffer();
353
354 if (lits.length > 0) {
355 if (voc.isUnassigned(lits[0])) {
356 stb.append(Lits.toString(this.lits[0]));
357 stb.append(" "); //$NON-NLS-1$
358 }
359 for (int i = 1; i < lits.length; i++) {
360 if (voc.isUnassigned(lits[i])) {
361 stb.append(" + "); //$NON-NLS-1$
362 stb.append(Lits.toString(this.lits[i]));
363 stb.append(" "); //$NON-NLS-1$
364 }
365 }
366 stb.append(">= "); //$NON-NLS-1$
367 stb.append(this.degree);
368 }
369 return stb.toString();
370 }
371
372 /**
373 * M?thode appel?e lors du backtrack
374 *
375 * @param p
376 * le litt?ral d?saffect?
377 */
378 public void undo(int p) {
379 watchCumul++;
380 }
381
382 public void setLearnt() {
383 throw new UnsupportedOperationException();
384 }
385
386 public void register() {
387 throw new UnsupportedOperationException();
388 }
389
390 public int size() {
391 return lits.length;
392 }
393
394 public int get(int i) {
395 return lits[i];
396 }
397
398 public void assertConstraint(UnitPropagationListener s) {
399 throw new UnsupportedOperationException();
400 }
401
402 /*
403 * (non-Javadoc)
404 *
405 * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
406 */
407 public BigInteger getCoef(int literal) {
408 return BigInteger.ONE;
409 }
410
411 /*
412 * (non-Javadoc)
413 *
414 * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
415 */
416 public BigInteger getDegree() {
417 return BigInteger.valueOf(degree);
418 }
419
420 public ILits getVocabulary() {
421 return voc;
422 }
423
424 /**
425 * @since 2.1
426 */
427 public void forwardActivity(double claInc) {
428 // TODO Auto-generated method stub
429
430 }
431
432 }