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